Bythos is a framework embedded in the Coq proof assistant for users to implement, compose and verify Byzantine distributed protocols. By including a simple shim layer, Bythos also enables running the OCaml protocol implementation generated using the extraction mechanism of Coq.
Check INSTALL.md for installation details, and a sample guide for exploring this project.