Programming Languages and Verification Group at MIT CSAIL

MIT CSAIL, Building 32–G8

Pinned Repositories

bedrock
Coq library for verified low-level programming
Language:Coq57 10 06
bedrock2
A work-in-progress language and compiler for verified low-level programming
Language:Coq289 17 10343
fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Language:Coq145 9 1030
fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Language:Coq703 54 405144
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Language:Coq141 14 924
koika
A core language for rule-based hardware design 🦑
Language:Coq136 24 209
riscv-coq
RISC-V Specification in Coq
Language:Coq100 15 1116
riscv-semantics
A formal semantics of the RISC-V ISA in Haskell
Language:Haskell147 24 1615
rupicola
Gallina to Bedrock2 compilation toolkit
Language:Coq51 16 911
timl
TiML: A Functional Programming Language with Time Complexity
Language:Standard ML75 12 26

Programming Languages and Verification Group at MIT CSAIL's Repositories

mit-plv/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Language:Coq703 54 405144
mit-plv/bedrock2
A work-in-progress language and compiler for verified low-level programming
Language:Coq289 17 10343
mit-plv/riscv-semantics
A formal semantics of the RISC-V ISA in Haskell
Language:Haskell147 24 1615
mit-plv/fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Language:Coq145 9 1030
mit-plv/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Language:Coq141 14 924
mit-plv/koika
A core language for rule-based hardware design 🦑
Language:Coq136 24 209
mit-plv/riscv-coq
RISC-V Specification in Coq
Language:Coq100 15 1116
mit-plv/timl
TiML: A Functional Programming Language with Time Complexity
Language:Standard ML75 12 26
mit-plv/bedrock
Coq library for verified low-level programming
Language:Coq57 10 06
mit-plv/rupicola
Gallina to Bedrock2 compilation toolkit
Language:Coq51 16 911
mit-plv/coqutil
Coq library for tactics, basic definitions, sets, maps
Language:Coq41 12 2424
mit-plv/bbv
Bedrock Bit Vector Library
Language:Coq27 16 1123
mit-plv/rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Language:Coq23 11 1219
mit-plv/hemiola
A Coq framework to support structural design and proof of hardware cache-coherence protocols
Language:Coq11 10 00
mit-plv/reification-by-parametricity
Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Language:Mathematica11 12 02
mit-plv/cross-crypto
Connecting computational and symbolic crypto models
Language:Coq8 13 719
mit-plv/engine-bench
Benchmarks for various proof engines
Language:Coq5 11 34
mit-plv/network-configurations
Using Coq to derive network configurations from declarative policies
Language:Coq4 13 0
mit-plv/stencils
A Coq library for verifying dependencies of stencil implementations
Language:Coq4 8 0
mit-plv/blog
A blog for PLV and friends of PLV
Language:CSS3 12 1
mit-plv/certifying-derivation-of-state-machines-from-coroutines
Language:Haskell3 10 02
mit-plv/fiat2
A high level language that will compile to bedrock2 using database-style techniques
Language:Coq23
mit-plv/softmul
Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware
Language:Coq2
mit-plv/Fiat_matrix
Language:Coq1 13 01
mit-plv/bedrock2-ci
Continuous Integration for bedrock2
Language:Makefile10 02
mit-plv/coq-ident-to-string
Ltac2 wizardy to convert a gallina identifier to a coq string.
12 1
mit-plv/foundational-integration-verification-of-a-cryptographic-server
http://adam.chlipala.net/papers/GarageDoorPLDI24/
mit-plv/spacetalk
Language:Lean3 0