SSF-MC was a multi-month applied research project to improve trust in the Ethereum Consensus Layer via Formal Methods, conducted in 2024.
The SSF-MC project verified Accountable Safety, a critical property of the Ethereum 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 Our Work
Apart from the verification of Accountable Safety for certain parameters, our work highlights the following insights:
- Multiple specifications at varying abstraction levels are essential: Using specifications in TLA+, Alloy, and SMT at various levels of abstraction ultimately made the problem tractable for automated tools.
- Combining tools is pivotal: Refining the spec in TLA+ deepened our understanding of the protocol and shaped key abstractions. Generating configurations like justified and finalized checkpoints was significantly easier with TLA+ and Alloy than from the initial Python spec. Ultimately, checking the Alloy model with the Kissat SAT solver enabled verification of the largest state spaces.
More details can be found in our in-depth tech report – and of course, all the specs are open-source:
Tech Report + Source Code
📖 Read our full tech report: https://arxiv.org/abs/2501.07958
💻 Source code and specs: https://github.com/freespek/ssf-mc
Huge thanks to co-authors Igor Konnov, Jure Kukovec, Roberto Saltini, and Thanh-Hai Tran! We are deeply grateful to Luca Zanolini and Francesco D’Amato for the fruitful discussions and the Ethereum Foundation and the EF Ecosystem Support Program (ESP) for supporting our work under the Academic Grants Round 2024!