SSF-MC is an applied research project to improve trust in the Ethereum Consensus Layer via Formal Methods.
In particular, we verify the 3-slot finality consensus protocol (3SF) by D’Amato, Saltini, Tran and Zanolini, a potential step on the path to Single-Slot Finality in Ethereum. Our key contributions are:
- We use model-checking in TLA+/Apalache, Alloy, and CVC5 to show that the protocol is accountably safe.
- We investigate the translation of Executable Python Specifications to the TLA+ specification language, to automate part of the specification effort.
ยป The project started in Q3 of 2024, and is in the process of wrapping up. Contact me for an early copy of the tech report.
SSF-MC is a joint project by Roberto Saltini and Thanh-Hai Tran (Consensys) and independent researchers Igor Konnov, Jure Kukovec, and Thomas Pani. The project is funded through a grant from the Ethereum Foundation‘s Ethereum Support Program Academic Grants Round 2024.