Blockchain Formal Specifications

This is a project of formal specifications built to gain intuition into various blockchain protocols. It uses Quint, a modern wrapper around TLA+.

Why Formal Specs?

• Exhaustive verification - Model checkers explore all possible states, not just test cases you thought of
• Find edge cases - Discover bugs in rare interleavings before they hit production
• Precise documentation - Specs are unambiguous, executable documentation
• Design validation - Verify protocol properties before writing code

Setup

npm install -g @informalsystems/quint

Specs

Spec	Description	Status
engine-api	Ethereum Engine API (CL/EL interaction)
bft-voting	BFT quorum voting
bft-proposal	BFT with leader proposal phase
bft-locking	BFT with multi-round locking
pbft	Practical BFT (3-phase protocol)

Quick Start

make help                  # see all commands
make test                  # test all specs
make test SPEC=bft-voting  # test one spec
make verify SPEC=pbft      # verify safety properties
make run SPEC=bft-locking  # random simulation

BFT Learning Path

The BFT specs form a progression, each building on the previous:

1. bft-voting - Why 2f+1 quorums guarantee agreement
2. bft-proposal - Why BFT needs a leader to coordinate
3. bft-locking - Why nodes must remember across rounds
4. pbft - How the 3-phase protocol ties it together

Contributing

1. Create a new directory for your spec
2. Include a README.md explaining the protocol
3. Document safety properties and what they mean

Resources

• Quint README - How to write Quint specs
• Quint Documentation
• Quint GitHub