Skip to content
@mit-plv

Programming Languages and Verification Group at MIT CSAIL

Popular repositories Loading

  1. fiat-crypto fiat-crypto Public

    Cryptographic Primitive Code Generation by Fiat

    Rocq Prover 799 163

  2. bedrock2 bedrock2 Public

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

    Rocq Prover 323 53

  3. riscv-semantics riscv-semantics Public

    A formal semantics of the RISC-V ISA in Haskell

    Haskell 172 19

  4. koika koika Public

    A core language for rule-based hardware design 🦑

    Rocq Prover 167 17

  5. kami kami Public

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

    Rocq Prover 164 30

  6. fiat fiat Public

    Mostly Automated Synthesis of Correct-by-Construction Programs

    Rocq Prover 157 35

Repositories

Showing 10 of 30 repositories
  • fiat-crypto Public

    Cryptographic Primitive Code Generation by Fiat

    mit-plv/fiat-crypto’s past year of commit activity
    Rocq Prover 799 163 137 (13 issues need help) 42 Updated Jan 12, 2026
  • rupicola Public

    Gallina to Bedrock2 compilation toolkit

    mit-plv/rupicola’s past year of commit activity
    Rocq Prover 65 MIT 15 4 1 Updated Jan 6, 2026
  • rewriter Public

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

    mit-plv/rewriter’s past year of commit activity
    Rocq Prover 26 23 5 (1 issue needs help) 0 Updated Jan 5, 2026
  • bedrock2 Public

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

    mit-plv/bedrock2’s past year of commit activity
    Rocq Prover 323 MIT 53 36 7 Updated Jan 5, 2026
  • riscv-coq Public

    RISC-V Specification in Coq

    mit-plv/riscv-coq’s past year of commit activity
    Rocq Prover 116 BSD-3-Clause 19 4 3 Updated Jan 5, 2026
  • lean4-itree Public

    Coinductive Interaction Trees in Lean4 using QPFs

    mit-plv/lean4-itree’s past year of commit activity
    Lean 10 MIT 1 0 0 Updated Dec 26, 2025
  • fiat2 Public

    A high level language for data-intensive applications, with formally verified database-style optimizations

    mit-plv/fiat2’s past year of commit activity
    Rocq Prover 6 MIT 6 0 0 Updated Dec 15, 2025
  • coqutil Public

    Coq library for tactics, basic definitions, sets, maps

    mit-plv/coqutil’s past year of commit activity
    Rocq Prover 51 MIT 28 7 2 Updated Dec 14, 2025
  • koika Public

    A core language for rule-based hardware design 🦑

    mit-plv/koika’s past year of commit activity
    Rocq Prover 167 LGPL-2.1 17 9 0 Updated Dec 10, 2025
  • quartz Public
    mit-plv/quartz’s past year of commit activity
    0 MIT 0 0 0 Updated Nov 26, 2025
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.