Anja Petković Komel
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.
Session
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.