proof

An advanced SAT solver

deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

A framework for formally verifying distributed systems implementations in Coq

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

The Agda standard library

Public append-only ledger microservice built with Slim Framework

seL4 specification and proofs

Verified Software Toolchain

The Ancillary Guide to Dark Mode and Bootstrap 5 - A continuation of the v4 Dark Mode POC. >>> Bootstrap 5.2 is in the `dev/v1.2.0` branch <<<

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

Reference implementation of the OpenRarity protocol with Python.

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

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

Coq formalizations of functional languages.

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

Zero-Knowledge Proofs "for (not too much 😉 ) dummies"

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

Correctness proofs of Ethereum token contracts

GAPT: General Architecture for Proof Theory

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