Skip to content
Formal Analysis of the CBC Casper Consensus Algorithm with TLA+
blog.trailofbits.com | blog | #blockchain | #formal-verification | #ethereum | #consensus | #tla-plus | #byzantine-fault-tolerance
Summary
A Trail of Bits intern formalized Ethereum's CBC Casper binary consensus protocol in TLA+/PlusCal, confirming finality requires a Byzantine fault threshold under one-third of validator weight.
- Published
- Collected