Construct a formal proof that Sumeragi is BFT

[e-ivkov]

The proof can be either purely mathematical or in TLA+ (Coq, etc.).

TLA+ should be convertible to math expressions in LaTeX.

[s8sato]

Alternatives:

• Isabelle/HOL

Papers:

• Formal Verification of Blockchain Byzantine Fault Tolerance

[appetrosyan]

I have some experience with Isabelle. My university CompSci lecturer, Larry Paulson is the author of that system, and we did a small amount of theorem proving as part of the courses.