act: From EVM Bytecode to Machine-Checked Reasoning

Abstract: This talk introduces act, a high-level specification language designed for formal verification of Ethereum smart contracts. act bridges the gap between human-readable specifications and machine-verifiable proofs, enabling developers to rigorously ensure their smart contracts behave as intended. We will demonstrate act’s key features through a live demo, showing how to write specifications that capture contract behavior in a clear, mathematically precise way; automatically proving the equivalence between act specifications and the EVM byte code of Solidity/Vyper implementations; export specifications to proof assistants (Rocq and Lean) for proving higher-level properties; and show an example of such a proof. The demo will walk through a real-world example, illustrating the verification workflow with act.

Bio: Sophie Rain is a formal verification researcher at the Argot Collective. With a background in mathematics and a PhD in computer science, she specializes in formal methods that combine mathematical logic with automated reasoning. Her research focuses on security of blockchain protocols. She developed CheckMate, an open-source tool for automatically verifying the game-theoretic security of protocols. Her current work involves Act, a specification language for Ethereum smart contracts, with the goal of creating an integrated verification pipeline for smart contract incentives. Her research interests include logic, blockchain security, game theory, and automated reasoning.