About me

I'm a senior formal methods engineer at Positive Web3 team. I specialize in blockchain security and the formal verification of software systems. I employ mathematical models, theorem provers, and model checking to rigorously prove that programs adhere to specifications and are free of vulnerabilities. By bridging the gap between theoretical correctness and real-world security, I help ensure that decentralized applications remain safe and reliable.

Publications and Reports

From Paradigm Shift to Audit Rift: Exploring Vulnerabilities and Audit Tips for TON Smart Contracts [Preprint submitted]

with Yury Yanovich, Sergey Sobolev, Yash Madhwal, Vladimir Gorgadze, Victoria Kovalevskaya, Elizaveta Smirnova, Matvey Mishuris, Subodh Sharma

VeHa-2024 Formal Verification Contest: Two Years of Experience and Prospects (in Russian) [pdf]

with Dmitry Kondratyev, Sergey Staroletov, Irina Shoshmina, Anastasia Krasnenkova, Nikolay Shilov, Natalia Garanina, Timofey Cherganov

Research and Application of Formal Verification Approaches for Ethereum Smart Contracts - PSSV 2024

Formal Verification of Smart Contracts in the ConCert Framework [medium]

Verification of HotStuff BFT Consensus Protocol With TLA+/TLC in an Industrial Setting - CSOC 2021 [pdf]

with Vladimir Kukharenko, Rafael Sadykov, Ruslan Rezin

Research & Background

I graduated from Lomonosov Moscow State University in 2023 with a combined B.S. & M.S. in Mathematics. In my third year, I joined the InnoChain project, where we built a formally verified enterprise blockchain. It was at this time that I became interested in blockchain technology and formal verification.

At ISP RAS I contributed to the development of an Isabelle-based framework for verifying C code, gaining hands-on experience with proof assistants.

Currently, as a Ph.D. candidate, I focus on the model checking of consensus protocols. Also I conduct security audits of smart contracts across multiple blockchain platforms using formal methods.