This is a simplified formal analysis and verification of Tendermint blockchain which uses a byzantine fault tolerant consensus algorithm.
Process Analysis Toolkit (PAT).
You would need to first compile and load /pat/PAT.Lib.Tendermint.cs into PAT. Please refer to section 2.5 of PAT user manual Using C# (C/C++/Java) Code as Libraries.
Verification results and the white paper can be found in /docs.