Software, Specifications, Proofs, etc.

Are specifications and proofs software?

TLA+ specifications

Various TLA+ specifications are available in the TLA+ examples repository. If you like consensus algorithms, two interesting ones are Streamlet and DAG-based consensus.

CPP-DPOR

A model-checking library for distributed protocols, inspired by Must. Uses dynamic partial-order reduction; parallel search never explores the same execution graph class twice, yet workers don’t have to synchronize! Successfully used to debug new features in stellar-core. Sources are on github at https://github.com/nano-o/CPP-DPOR.

python-fbas

A prototype tool to reason about Federated Byzantine Agreement Systems using SAT solvers. Sources are on github at https://github.com/nano-o/python-fbas.

Formalization and proof of a classical distributed algorithm

https://github.com/nano-o/Distributed-termination-detection

The algorithm is the “channel-counting” termination-detection algorithm of Kumar (1985). The proof I propose is a great example of inductive reasoning about distributed algorithms. The exercise branch of the repository sets things up as an exercise in finding inductive invariants.

Accountable safety of Tendermint

An IVy model and proof of accountable safety for Tendermint. Developed with help from Benoit Razet while I was at Galois. Sources are in the CometBFT repository at https://github.com/cometbft/cometbft/tree/main/spec/ivy-proofs.