zhouxt1
Follow
Lists (1)
Stars
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
Total Parser Combinators in Coq [maintainer=@womeier]
Tricks you wish the Coq manual told you [maintainer=@tchajed]
A Library for Representing Recursive and Impure Programs in Coq
A Python library to ease the development of encoders and decoders for various protocols and file formats, especially telecom ones. Provides an ASN.1 compiler and a CSN.1 runtime.
ASN1SCC: An open source ASN.1 compiler for embedded systems
Various signed and unsigned integer types for OCaml
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
Various signed and unsigned integers for OCaml
A work-in-progress language and compiler for verified low-level programming
Cryptographic Primitive Code Generation by Fiat
Creusot helps you prove your code is correct in an automated fashion.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
Mostly Automated Synthesis of Correct-by-Construction Programs
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Lean 3's obsolete mathematical components library: please use mathlib4
Automated generation of provably secure, zero-copy parsers from format specifications
KaRaMeL is a tool for extracting low-level F* programs to readable C code