Model Checking Accountability in Ethereum

SSF-MC is a research project supported by the Ethereum Foundation’s Ecosystem Support Program. The goal is to investigate how model checking, especially the model checker Apalache, can help the researchers in verifying consensus algorithms such as Single-Slot Finality.

We have started the project in Q3 of 2024. Stay tuned for more details.