Popular repositories Loading

1. fiat-crypto fiat-crypto Public

   Forked from mit-plv/fiat-crypto

   Cryptographic Primitive Code Generation by Fiat

   Rocq Prover

2. bedrock2 bedrock2 Public

   Forked from mit-plv/bedrock2

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

   Rocq Prover

3. rocq rocq Public

   Forked from rocq-prover/rocq

   The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

   OCaml

4. rupicola rupicola Public

   Forked from mit-plv/rupicola

   Gallina to Bedrock2 compilation toolkit

   Rocq Prover

5. coqutil coqutil Public

   Forked from mit-plv/coqutil

   Coq library for tactics, basic definitions, sets, maps

   Rocq Prover

6. stdlib stdlib Public

   Forked from rocq-prover/stdlib

   Stdlib for the Rocq Prover

   Rocq Prover