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

    Coq 707 147

  2. bedrock2 bedrock2 Public

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

    Coq 292 43

  3. riscv-semantics riscv-semantics Public

    A formal semantics of the RISC-V ISA in Haskell

    Haskell 155 16

  4. fiat fiat Public

    Mostly Automated Synthesis of Correct-by-Construction Programs

    Coq 147 31

  5. kami kami Public

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

    Coq 141 24

  6. koika koika Public

    A core language for rule-based hardware design 🦑

    Coq 138 9

Repositories

Showing 10 of 28 repositories
  • fiat-crypto Public

    Cryptographic Primitive Code Generation by Fiat

    mit-plv/fiat-crypto’s past year of commit activity
    Coq 707 147 119 (13 issues need help) 37 Updated Sep 20, 2024
  • fiat2 Public

    A high level language that will compile to bedrock2 using database-style techniques

    mit-plv/fiat2’s past year of commit activity
    Coq 2 MIT 3 0 0 Updated Sep 19, 2024
  • 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
    Coq 22 20 5 (1 issue needs help) 0 Updated Sep 19, 2024
  • spacetalk Public
    mit-plv/spacetalk’s past year of commit activity
    Lean 0 0 0 0 Updated Sep 19, 2024
  • cross-crypto Public Forked from asya-bergal/cross-crypto

    Connecting computational and symbolic crypto models

    mit-plv/cross-crypto’s past year of commit activity
    Coq 8 MIT 22 3 0 Updated Sep 18, 2024
  • engine-bench Public

    Benchmarks for various proof engines

    mit-plv/engine-bench’s past year of commit activity
    Coq 5 MIT 5 2 0 Updated Sep 18, 2024
  • fiat Public

    Mostly Automated Synthesis of Correct-by-Construction Programs

    mit-plv/fiat’s past year of commit activity
    Coq 147 31 1 0 Updated Sep 17, 2024
  • koika Public

    A core language for rule-based hardware design 🦑

    mit-plv/koika’s past year of commit activity
    Coq 138 GPL-3.0 9 8 1 Updated Sep 14, 2024
  • rupicola Public

    Gallina to Bedrock2 compilation toolkit

    mit-plv/rupicola’s past year of commit activity
    Coq 49 MIT 11 4 2 Updated Aug 19, 2024
  • bedrock2 Public

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

    mit-plv/bedrock2’s past year of commit activity
    Coq 292 MIT 43 36 12 Updated Aug 16, 2024
View all repositories

People

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

Top languages

Loading…

Most used topics

Loading…