mit-plv Goto Github PK

bbv

Bedrock Bit Vector Library

bedrock

Coq library for verified low-level programming

bedrock2

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

bedrock2-ci

Continuous Integration for bedrock2

blog

A blog for PLV and friends of PLV

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

coq-ident-to-string

Ltac2 wizardy to convert a gallina identifier to a coq string.

coqutil

Coq library for tactics, basic definitions, sets, maps

cross-crypto

Connecting computational and symbolic crypto models

engine-bench

Benchmarks for various proof engines

fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

fiat-crypto

Cryptographic Primitive Code Generation by Fiat

fiat2

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

fiat_matrix

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

http://adam.chlipala.net/papers/GarageDoorPLDI24/

hemiola

A Coq framework to support structural design and proof of hardware cache-coherence protocols

kami

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

koika

A core language for rule-based hardware design 🦑

network-configurations

Using Coq to derive network configurations from declarative policies

reification-by-parametricity

Fast Setup for Proof by Reflection, in Two Lines of Ltac.

rewriter

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

riscv-coq

RISC-V Specification in Coq

riscv-semantics

A formal semantics of the RISC-V ISA in Haskell

rupicola

Gallina to Bedrock2 compilation toolkit

softmul

Proving that a system with software trap handlers for unimplemented instructions behaves as if they were implemented in hardware

spacetalk

stencils

A Coq library for verifying dependencies of stencil implementations

timl

TiML: A Functional Programming Language with Time Complexity