2026-05-08 –, Masaryk Stage
This workshop provides practical training in act, a high-level specification language for EVM programs with built-in formal verification capabilities to increase smart contract security. Targeted at security experts and auditors, we will develop an act specification for a smart contract, automatically verify its equivalence to Solidity implementation, and prove correctness in a proof assistant.
Smart contracts are a prominent domain for formal verification as they often manage large amounts of assets and are immutable once deployed. Their vulnerabilities have led to significant financial losses, which is why strong formal guarantees are necesary. Smart contract security is multi-faceted (as outlined by 1TS initiative from Ethereum Foundation) - formal verification plays a part in a holisitc security approach. act, developed at Argot, sits at the core of these efforts, providing a way to reason about security in the highest level of formality.
Coming from a formal training in mathematics and computer science, I value applying complex mathematical ideas to make a functioning tool that abstacts away the heavy lifting and is directly usable by developers. As a scientist I am also very passionate about bringing knowledge to the broader public - for years I was participating on a science show on Slovenian national television, making mathematical concepts accessible to an average Joe.
I am a formal verification researcher at Argot Collective, specializing in automated theorem proving, type theory, and its applications to blockchain security. I co-built CheckMate tool for automated game-theoretic security analysis of blochckain protocols. I completed my PhD on proof assistants and type systems. I'm passionate about science communication, presenting math riddles on Slovenian TV.