Tendermint consensus powers many proof-of-stake blockchains securing billions of dollars. As such, it is a core component of the Cosmos network of blockchains. In Tendermint, n participants have to reach consensus in presence of f Byzantine faults. Thus, it is crucial to show that it satisfies (among others) two safety properties: Agreement and fork accountability. We present a TLA+ specification of Tendermint consensus that focuses on these properties. By running the Apalache model checker for n=4..6, we show two properties. First, Tendermint satisfies agreement when f < n/3, that is, it cannot produce a fork. Second, Tendermint satisfies fork accountability for f >= n/3, that is, in case of disagreement, the correct processes collectively hold a piece of evidence that allows us to identify at least n/3 misbehaving participants.

Our specification presents a challenging case study for the CPP community: Extending our results beyond the small parameters and proving agreement and fork accountability for arbitrary values of n and f.

https://github.com/tendermint/spec/tree/master/rust-spec/tendermint-accountability