Ivy Proofs

Copy Copyright (c) 2020 Galois, Inc. SPDX-License-Identifier: Apache-2.0

Contents

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 shim object 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).

1. Install Docker (opens new window) and Docker Compose (opens new window).
2. Build a Docker image: docker-compose build
3. Run the proofs inside the Docker container: docker-compose run tendermint-proof. This will check all the proofs with the ivy_check command and write the output of ivy_check to a subdirectory of `./output/'