Specification and Model-checking of the ZKsync Governance Protocol
A detailed blogpost that summarizes our work on formal specification of ZKsync Governance and model checking of its properties...
After our success in specification and model checking of the ChonkyBFT consensus in Quint, Denis Kolegov at Matter Labs offered me to apply Quint and its tools to a slightly different domain: ZKsync governance contracts in Solidity. We used the Quint simulator and the model checker Apalache. Check our technical blogpost that summarizes our experience and highlights the important modeling decisions we made.
Also, check the talk at DeFi Security Summit 2024 on this work, which I gave later.
This post is licensed under CC BY 4.0 by the author.