12 open source projects by mit-plv

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

Mostly Automated Synthesis of Correct-by-Construction Programs

RISC-V Specification in Coq

Cryptographic Primitive Code Generation by Fiat

Coq library for verified low-level programming

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

Bedrock Bit Vector Library

Gallina to Bedrock2 compilation toolkit

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Coq library for tactics, basic definitions, sets, maps

A core language for rule-based hardware design 🦑

A formal semantics of the RISC-V ISA in Haskell