Stars
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications!
Cryptographic Primitive Code Generation by Fiat
A framework for formally verifying distributed systems implementations in Coq
Tricks you wish the Coq manual told you [maintainer=@tchajed]
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
FSCQ is a certified file system written and proven in Coq
A Library for Representing Recursive and Impure Programs in Coq
A formalization of geometry in Coq based on Tarski's axiom system
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
A Verified Compiler for Gallina, Written in Gallina
A minimalistic blockchain consensus implemented and verified in Coq
Correctness proofs of Ethereum token contracts
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Formal verification of the Algorand consensus protocol
Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2018