acorrenson
Follow
Starred repositories
109
stars
written in Coq
Clear filter
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
An axiom-free formalization of category theory in Coq for personal study and practical work
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]
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs!
Metaprogramming, verified meta-theory and implementation of Coq in Coq
A work-in-progress language and compiler for verified low-level programming
Language for high-assurance and high-speed cryptography
Randomized Property-Based Testing Plugin for Coq
A Library for Representing Recursive and Impure Programs in Coq
Mathematical Components compliant Analysis Library
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…
A formalization of geometry in Coq based on Tarski's axiom system
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
A Verified Compiler for Gallina, Written in Gallina
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Formal specification and verification of hardware, especially for security and privacy.
A framework for smart contract verification in Coq
A library of mechanised undecidability proofs in the Coq proof assistant.
