# Ivy Proofs
This folder contains:
tendermint.ivy, a specification of Tendermint algorithm as described in The latest gossip on BFT consensus by E. Buchman, J. Kwon, Z. Milosevic.
abstract_tendermint.ivy, a more abstract specification of Tendermint that is more verification-friendly.
classic_safety.ivy, a proof that Tendermint satisfies the classic safety property of BFT consensus: if every two quorums have a well-behaved node in common, then no two well-behaved nodes ever disagree.
accountable_safety_1.ivy, a proof that, assuming every quorum contains at least one well-behaved node, if two well-behaved nodes disagree, then there is evidence demonstrating at least f+1 nodes misbehaved.
accountable_safety_2.ivy, a proof that, regardless of any assumption about quorums, well-behaved nodes cannot be framed by malicious nodes. In other words, malicious nodes can never construct evidence that incriminates a well-behaved node.
network_shim.ivy, the network model and a convenience
shimobject to interface with the Tendermint specification.
domain_model.ivy, a specification of the domain model underlying the Tendermint specification, i.e. rounds, value, quorums, etc.
All specifications and proofs are written in Ivy (opens new window).
The license above applies to all files in this folder.
# Building and running
The easiest way to check the proofs is to use Docker (opens new window).
- Install Docker (opens new window) and Docker Compose (opens new window).
- Build a Docker image:
- Run the proofs inside the Docker container:
docker-compose run tendermint-proof. This will check all the proofs with the
ivy_checkcommand and write the output of
ivy_checkto a subdirectory of `./output/'