Skip to content

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

Change the repository type filter

All

    Repositories list

    29 repositories

    • fiat-crypto

      Public
      Cryptographic Primitive Code Generation by Fiat
      Rocq Prover
      •
      Other
      •155•771•126•36•Updated Aug 13, 2025Aug 13, 2025

    • rupicola

      Public
      Gallina to Bedrock2 compilation toolkit
      coq
      Rocq Prover
      •
      MIT License
      •14•59•4•1•Updated Aug 13, 2025Aug 13, 2025

    • fiat

      Public
      Mostly Automated Synthesis of Correct-by-Construction Programs
      Rocq Prover
      •
      Other
      •35•154•1•0•Updated Aug 13, 2025Aug 13, 2025

    • bedrock2

      Public
      A work-in-progress language and compiler for verified low-level programming
      Rocq Prover
      •
      MIT License
      •51•311•33•7•Updated Aug 12, 2025Aug 12, 2025

    • rewriter

      Public
      Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
      Rocq Prover
      •
      Other
      •23•25•5•1•Updated Aug 12, 2025Aug 12, 2025

    • engine-bench

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

    • coqutil

      Public
      Coq library for tactics, basic definitions, sets, maps
      Rocq Prover
      •
      MIT License
      •25•49•7•2•Updated Jul 15, 2025Jul 15, 2025

    • riscv-coq

      Public
      RISC-V Specification in Coq
      Rocq Prover
      •
      BSD 3-Clause "New" or "Revised" License
      •18•116•4•4•Updated Jul 14, 2025Jul 14, 2025

    • kami

      Public
      A Platform for High-Level Parametric Hardware Specification and its Modular Verification
      proof-assistanthardware-description-languagehardware-verificationcoqbluespec
      Rocq Prover
      •
      MIT License
      •28•158•3•0•Updated Jul 14, 2025Jul 14, 2025

    • lean4-choice-tree

      Public
      Coinductive Choice Tree in Lean4 using QPFs
      Lean
      •
      MIT License
      •1•8•0•0•Updated Jul 8, 2025Jul 8, 2025

    • bbv

      Public
      Bedrock Bit Vector Library
      Rocq Prover
      •
      MIT License
      •24•28•4•3•Updated Jun 20, 2025Jun 20, 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
      •14•159•8•1•Updated Jun 11, 2025Jun 11, 2025

    • cross-crypto

      Public
      Connecting computational and symbolic crypto models
      Coq
      •
      MIT License
      •22•8•3•0•Updated Jun 3, 2025Jun 3, 2025

    • fiat2

      Public
      A high level language for data-intensive applications, with formally verified database-style optimizations
      Coq
      •
      MIT License
      •5•6•0•0•Updated May 14, 2025May 14, 2025

    • isolation

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

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

      Public
      http://adam.chlipala.net/papers/GarageDoorPLDI24/
      1•1•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•3•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
      •18•170•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
      •1•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-programmingtime-complexitystandard-mlsmlmlton
      Standard ML
      •6•80•2•0•Updated Aug 28, 2017Aug 28, 2017

    • bedrock

      Public
      Coq library for verified low-level programming
      Coq
      •
      Other
      •6•60•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