Top 32 proof open source projects

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Coq formalizations of functional languages.

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

The Definitive Guide to Dark Mode and Bootstrap 4 - A proof of concept

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)

Tierion Hash API client library for Node.js

Emofishes is a collection of proof of concepts that help improve, bypass or detect virtualized execution environments (focusing on the ones setup for malware analysis).

Formalisation of the linear lambda calculus in Coq

Provably correct implementation of insertion sort in Idris.

An advanced SAT solver

A framework for formally verifying distributed systems implementations in Coq

Public append-only ledger microservice built with Slim Framework

The Agda standard library

⚠️ KADENCE HAS MOVED TO GITLAB ⚠️

seL4 specification and proofs

Project is in active development and has been moved to the EthereumJS VM monorepo.

📚Solutions to Language, Proof and Logic (2nd Edition)

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

🎞️💓🍿 Love streaming - It's always best to watch a movie together ! 🤗

Examples of NuID's zero knowledge authentication and key management facilities in various languages and frameworks. Open an Issue or PR if you'd like to see your favorite tool here.

A JavaScript propositional logic and resolution library

Fitch style proof constructor

Project Planeverb is a CPU based real-time wave-based acoustics engine for games. It comes with an integration with the Unity Engine.

Basic Analysis, undergraduate real analysis textbook

Batch verification proposal for the zkSNARK verification with the same(!) circuit

GAPT: General Architecture for Proof Theory

Intermediate Memory Model (IMM) and compilation correctness proofs for it

Build trust into your image by creating a blockchain certificate for it

Hääl - Anonymous Electronic Voting System on Public Blockchains

Solutions for the book "Language Proof and Logic".

Proof of concept to generate safe and fast JavaScript