Stars
The CompCert formally-verified C compiler
Cryptographic Primitive Code Generation by Fiat
A framework for formally verifying distributed systems implementations in Coq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
A work-in-progress language and compiler for verified low-level programming
A Library for Representing Recursive and Impure Programs in Coq
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
A Verified Compiler for Gallina, Written in Gallina
A framework for smart contract verification in Coq
A minimalistic blockchain consensus implemented and verified in Coq
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
A framework for implementing and certifying impure computations in Coq
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
This is a Coq formalization of Damas-Milner type system and its algorithm W.
Formal verification of the Algorand consensus protocol
Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
An implementation of the Chord lookup protocol verified in Coq using the Verdi framework
Coq tactics for certification of the results of SSL-based program synthesis via Hoare Type Theory.
Formal Verification of Merckle Proof algorithm in Coq
A toolkit to reason with programs raising exceptions