May 19
Loading video player...
In the tenth episode of Honest Majority, we speak with Zoe Paraskevopoulou, Assistant Professor at the National Technical University of Athens and former member of the Ethereum Foundation's formal verification team, about the importance of formal verification for smart contract security. The conversation begins with Zoe's path from programming languages and formal methods research into the blockchain space, before diving into what formal verification actually is and why it goes beyond testing and code review. We discuss how mathematical proofs can guarantee smart contract correctness for all possible inputs and states, and explore ACT v0.2.0, a formal specification and verification framework for EVM smart contracts developed at Argot Collective. The episode covers how ACT models contracts as state transition systems, how it automatically proves equivalence between bytecode and formal specifications, and the open challenges ahead including unknown code and re-entrancy vulnerabilities. The conversation closes with Zoe's vision for the future, where LLMs could make formal verification more accessible and software increasingly comes with machine-checked proofs of correctness.