SSF-MC was a multi-month applied research project conducted in 2024 to improve trust in the Ethereum Consensus Layer via formal methods.
The project verified Accountable Safety, a critical property of Ethereum's 3SF consensus protocol, using formal methods tools. 3SF (3-Slot Finality) is a recently designed consensus protocol by Francesco D'Amato, Roberto Saltini, Thanh-Hai Tran, and Luca Zanolini. It builds on Casper FFG to achieve faster finality while maintaining safety and liveness, a potential step on the path to Single-Slot Finality in Ethereum (details, paper).
In SSF-MC, formal specification in TLA+, Alloy, and SMT at various abstraction levels allowed us to exhaustively check Accountable Safety for parameters reasonably large for verification. Extensive experiments, lasting up to 16 days, found no counterexamples, further boosting confidence in the protocol's safety.
Insights from the work
Apart from the verification of Accountable Safety for certain parameters, the work highlighted two broader points:
- Multiple specifications at varying abstraction levels are essential. Using specifications in TLA+, Alloy, and SMT at different levels of abstraction ultimately made the problem tractable for automated tools.
- Combining tools is pivotal. Refining the specification in TLA+ deepened our understanding of the protocol and shaped key abstractions. Generating configurations such as justified and finalized checkpoints was significantly easier with TLA+ and Alloy than from the initial Python specification. Ultimately, checking the Alloy model with the Kissat SAT solver enabled verification of the largest state spaces.
Tech report and source code
More details are available in the technical report, and all specifications are open source:
- Tech report: arxiv.org/abs/2501.07958
- Source code and specifications: github.com/freespek/ssf-mc
Thanks to co-authors Igor Konnov, Jure Kukovec, Roberto Saltini, and Thanh-Hai Tran. We are grateful to Luca Zanolini and Francesco D'Amato for fruitful discussions, and to the Ethereum Foundation and the EF Ecosystem Support Program for supporting the work under the Academic Grants Round 2024.
