-
OpenTT:
A family of effectful type
theories formalized in Agda.
-
Damysus:
A protocol implemented in
C++ that improves
the efficiency and
reliability of HotStuff
thanks to trusted components.
-
Pistis:
A real-time Byzantine
reliable broadcast
protocol implemented in C++.
-
Asphalion:
A framework implemented in Coq and OCaml, to implement, execute, and reason about the safety of
hybrid fault-tolerant systems.
-
Velisarios:
A framework implemented in Coq and OCaml, to implement, execute, and reason about the safety of
Byzantine fault-tolerant systems.
-
Coq-dL:
A verified implementation
of KeYmaera X's core in
Coq (KeYmaera X is a proof assistant for
cyber-physical systems).
-
NuprlInCoq:
A verified
implementation of Nuprl in Coq. It includes a Nuprl proof translator
written in OCaml.
-
EventML:
A framework to implement, execute and reason about crash
fault-tolerante systems, implemented in Nuprl, SML,
OCaml, Lisp, and Scala.
-
Aneris:
A fault-tolerant ordered broadcast service similar to Paxos, implemented in EventML.
-
Skalpel:
A static analysis tool implemented in SML that
reports type error for the SML language.