Petar Maksimović is a Senior Verification Engineer at Nethermind and a Research Fellow at Imperial College London. He holds a PhD in theoretical computer science from the University of Nice Sophia Antipolis (France) and a PhD in applied mathematics from the University of Novi Sad (Serbia). The focus of his work is the development of program analysis tools and their application to real-world codebases, and his research has been published in top-tier conferences such as CAV, ECOOP, PLDI, and POPL. At Nethermind, he is working on the development of verification infrastructures for proving correctness and security of real-world zero-knowledge technologies in the Lean proof assistant. In particular, he has led and primarily executed the formal verification of Succinct’s SP1 HyperCube and Axiom’s OpenVM RISC-V extension against the official Lean RISC-V specification.