We are working to finalize an updated Tendermint specification with formal
proofs of safety and liveness.

In the meantime, see the [description in the
docs](http://tendermint.readthedocs.io/en/master/specification/byzantine-consensus-algorithm.html).

There are also relevant but somewhat outdated descriptions in Jae Kwon's [original
whitepaper](https://tendermint.com/static/docs/tendermint.pdf) and Ethan Buchman's [master's
thesis](https://atrium.lib.uoguelph.ca/xmlui/handle/10214/9769).