SSF-MC is a research project applying Formal Methods to improve trust in the Ethereum Consensus Layer.
In particular, we investigate the feasibility of translating Executable Python Specifications to the TLA+ specification language for proposed protocol upgrades to Single-Slot Finality. We then verify Accountable Safety using the Apalache model-checker.
ยป The project started in Q3 of 2024. Stay tuned for more details.
SSF-MC 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.