Skip to content

@mit-plv Programming Languages and Verification Group at MIT CSAIL

Change the repository type filter

All

    Repositories list

    30 repositories

    • fiat-crypto

      Public
      Cryptographic Primitive Code Generation by Fiat
      Rocq Prover
      •
      Other
      •164•806•137•38•Updated Feb 20, 2026Feb 20, 2026

    • rupicola

      Public
      Gallina to Bedrock2 compilation toolkit
      coq
      Rocq Prover
      •
      MIT License
      •15•65•4•1•Updated Feb 19, 2026Feb 19, 2026

    • bedrock2

      Public
      A work-in-progress language and compiler for verified low-level programming
      Rocq Prover
      •
      MIT License
      •53•323•37•8•Updated Feb 19, 2026Feb 19, 2026

    • rewriter

      Public
      Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
      Rocq Prover
      •
      Other
      •24•26•5•0•Updated Feb 17, 2026Feb 17, 2026

    • coqutil

      Public
      Coq library for tactics, basic definitions, sets, maps
      Rocq Prover
      •
      MIT License
      •28•51•7•3•Updated Feb 13, 2026Feb 13, 2026

    • quartz

      Public
      MIT License
      •0•0•0•0•Updated Jan 29, 2026Jan 29, 2026

    • fiat

      Public
      Mostly Automated Synthesis of Correct-by-Construction Programs
      Rocq Prover
      •
      Other
      •35•157•1•1•Updated Jan 27, 2026Jan 27, 2026

    • riscv-coq

      Public
      RISC-V Specification in Coq
      Rocq Prover
      •
      BSD 3-Clause "New" or "Revised" License
      •19•116•4•3•Updated Jan 5, 2026Jan 5, 2026

    • lean4-itree

      Public
      Coinductive Interaction Trees in Lean4 using QPFs
      Lean
      •
      MIT License
      •1•10•0•0•Updated Dec 26, 2025Dec 26, 2025

    • fiat2

      Public
      A high level language for data-intensive applications, with formally verified database-style optimizations
      Rocq Prover
      •
      MIT License
      •6•6•0•0•Updated Dec 15, 2025Dec 15, 2025

    • koika

      Public
      A core language for rule-based hardware design 🦑
      semanticscoqprogramming-languagesformal-methodscompilationhardware-description-language
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •20•172•9•0•Updated Dec 10, 2025Dec 10, 2025

    • engine-bench

      Public
      Benchmarks for various proof engines
      Coq
      •
      MIT License
      •6•6•2•1•Updated Nov 21, 2025Nov 21, 2025

    • kami

      Public
      A Platform for High-Level Parametric Hardware Specification and its Modular Verification
      coqproof-assistantbluespechardware-description-languagehardware-verification
      Rocq Prover
      •
      MIT License
      •30•164•3•1•Updated Nov 20, 2025Nov 20, 2025

    • bbv

      Public
      Bedrock Bit Vector Library
      Rocq Prover
      •
      MIT License
      •25•28•5•2•Updated Oct 28, 2025Oct 28, 2025

    • cross-crypto

      Public
      Connecting computational and symbolic crypto models
      Rocq Prover
      •
      MIT License
      •22•8•4•0•Updated Oct 8, 2025Oct 8, 2025

    • isolation

      Public
      Coq
      •
      GNU General Public License v3.0
      •2•4•0•0•Updated Oct 15, 2024Oct 15, 2024

    • foundational-integration-verification-of-a-cryptographic-server

      Public
      http://adam.chlipala.net/papers/GarageDoorPLDI24/
      1•2•0•0•Updated Apr 6, 2024Apr 6, 2024

    • softmul

      Public
      Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware
      Coq
      •1•4•0•0•Updated Mar 19, 2024Mar 19, 2024

    • riscv-semantics

      Public
      A formal semantics of the RISC-V ISA in Haskell
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •19•173•11•0•Updated Aug 13, 2023Aug 13, 2023

    • hemiola

      Public
      A Coq framework to support structural design and proof of hardware cache-coherence protocols
      coqproof-assistantdomain-specific-languagecache-coherencehardware-verification
      Coq
      •
      MIT License
      •2•14•0•0•Updated May 7, 2022May 7, 2022

    • certifying-derivation-of-state-machines-from-coroutines

      Public
      Haskell
      •
      MIT License
      •3•5•0•0•Updated Oct 30, 2021Oct 30, 2021

    • coq-ident-to-string

      Public
      Ltac2 wizardy to convert a gallina identifier to a coq string.
      MIT License
      •1•1•1•0•Updated Jan 15, 2021Jan 15, 2021

    • reification-by-parametricity

      Public
      Fast Setup for Proof by Reflection, in Two Lines of Ltac.
      Mathematica
      •
      MIT License
      •3•14•0•0•Updated Jan 12, 2021Jan 12, 2021

    • blog

      Public
      A blog for PLV and friends of PLV
      CSS
      •2•4•0•0•Updated Nov 15, 2020Nov 15, 2020

    • network-configurations

      Public
      Using Coq to derive network configurations from declarative policies
      Coq
      •
      MIT License
      •2•6•0•0•Updated Apr 30, 2019Apr 30, 2019

    • bedrock2-ci

      Public
      Continuous Integration for bedrock2
      Makefile
      •1•1•0•0•Updated Jun 27, 2018Jun 27, 2018

    • Fiat_matrix

      Public
      Coq
      •
      Other
      •2•2•0•0•Updated Apr 26, 2018Apr 26, 2018

    • timl

      Public
      TiML: A Functional Programming Language with Time Complexity
      functional-programmingsmltime-complexitystandard-mlmlton
      Standard ML
      •6•80•2•0•Updated Aug 28, 2017Aug 28, 2017

    • bedrock

      Public
      Coq library for verified low-level programming
      Coq
      •
      Other
      •6•62•0•0•Updated Jun 15, 2017Jun 15, 2017

    • stencils

      Public
      A Coq library for verifying dependencies of stencil implementations
      Coq
      •
      Other
      •1•5•0•0•Updated May 29, 2016May 29, 2016