Programming Languages and Verification Group at MIT CSAIL

bedrock2 Public
A work-in-progress language and compiler for verified low-level programming

Coq 155 MIT 40 37 16 Updated Dec 7, 2021
coqutil Public
Coq library for tactics, basic definitions, sets, maps

Coq 21 MIT 13 7 0 Updated Dec 7, 2021
fiat-crypto Public
Cryptographic Primitive Code Generation by Fiat

Coq 432 116 84 (8 issues need help) 12 Updated Dec 6, 2021
rupicola Public
Extracting imperative code from Gallina

Coq 17 MIT 5 4 1 Updated Dec 7, 2021
fiat Public
Mostly Automated Synthesis of Correct-by-Construction Programs

Coq 125 24 1 2 Updated Dec 3, 2021
rewriter Public
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

Coq 17 12 2 1 Updated Dec 3, 2021
cross-crypto Public
Connecting computational and symbolic crypto models

Coq 7 MIT 15 3 0 Updated Nov 25, 2021
certifying-derivation-of-state-machines-from-coroutines Public

Haskell 1 MIT 1 0 0 Updated Oct 30, 2021
koika Public
A core language for rule-based hardware design 🦑

Coq 69 GPL-3.0 2 8 0 Updated Oct 28, 2021
bbv Public
Bedrock Bit Vector Library

Coq 25 MIT 17 4 1 Updated Oct 6, 2021

Popular repositories Loading