Skip to content

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

Change the repository type filter

All

    Repositories list

    31 repositories

    • fiat-crypto

      Public
      Cryptographic Primitive Code Generation by Fiat
      Rocq Prover
      •
      Other
      •175•839•139•46•Updated Aug 7, 2026Aug 7, 2026

    • coqutil

      Public
      Coq library for tactics, basic definitions, sets, maps
      Rocq Prover
      •
      MIT License
      •32•54•7•4•Updated Aug 6, 2026Aug 6, 2026

    • riscv-coq

      Public
      RISC-V Specification in Coq
      Rocq Prover
      •
      BSD 3-Clause "New" or "Revised" License
      •20•118•5•4•Updated Aug 6, 2026Aug 6, 2026

    • bedrock2

      Public
      A work-in-progress language and compiler for verified low-level programming
      Rocq Prover
      •
      MIT License
      •56•335•38•9•Updated Aug 6, 2026Aug 6, 2026

    • rupicola

      Public
      Gallina to Bedrock2 compilation toolkit
      coq
      coq
      Rocq Prover
      •
      MIT License
      •15•71•4•0•Updated Aug 4, 2026Aug 4, 2026

    • bbv

      Public
      Bedrock Bit Vector Library
      Rocq Prover
      •
      MIT License
      •25•30•5•2•Updated Aug 2, 2026Aug 2, 2026

    • granite

      Public
      Coming soon!
      0•0•0•0•Updated Aug 2, 2026Aug 2, 2026

    • rewriter

      Public
      Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
      Rocq Prover
      •
      Other
      •24•28•5•2•Updated Jul 29, 2026Jul 29, 2026

    • fiat2

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

    • quartz

      Public
      MIT License
      •0•0•0•0•Updated Jun 28, 2026Jun 28, 2026

    • fiat

      Public
      Mostly Automated Synthesis of Correct-by-Construction Programs
      Rocq Prover
      •
      Other
      •34•160•1•1•Updated Jun 19, 2026Jun 19, 2026

    • kami

      Public
      A Platform for High-Level Parametric Hardware Specification and its Modular Verification
      coqproof-assistantbluespec
      coqproof-assistantbluespechardware-description-languagehardware-verification
      Rocq Prover
      •
      MIT License
      •30•170•3•1•Updated May 26, 2026May 26, 2026

    • lean4-itree

      Public
      Coinductive Interaction Trees in Lean4 using QPFs
      Lean
      •
      MIT License
      •1•17•0•0•Updated May 7, 2026May 7, 2026

    • cross-crypto

      Public
      Connecting computational and symbolic crypto models
      Rocq Prover
      •
      MIT License
      •19•8•4•0•Updated Apr 3, 2026Apr 3, 2026

    • koika

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

    • engine-bench

      Public
      Benchmarks for various proof engines
      Coq
      •
      MIT License
      •5•6•2•1•Updated Nov 21, 2025Nov 21, 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•5•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
      •23•176•11•1•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-language
      coqproof-assistantdomain-specific-languagecache-coherencehardware-verification
      Coq
      •
      MIT License
      •3•15•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-complexity
      functional-programmingsmltime-complexitystandard-mlmlton
      Standard ML
      •7•85•2•0•Updated Aug 28, 2017Aug 28, 2017

    • bedrock

      Public
      Coq library for verified low-level programming
      Coq
      •
      Other
      •7•65•0•0•Updated Jun 15, 2017Jun 15, 2017
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.