sifive/Kami - Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
uwplse/verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
amintimany/Categories - A formalization of category theory in the Coq proof assistant.
DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
coq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [[email protected]]
pa-ba/calc-comp - Coq proofs for the paper "Calculating Correct Compilers"
tchajed/iris-simp-lang - We define a simple programming language, simplang, then instantiate Iris to verify simple simplang programs with concurrent separation logic.
snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
coq-community/semantics - A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [[email protected]]
We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.