2026-07-21T01:00:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25698 2026-06-23T12:49:04Z ddc:004 open_access

Scaling Formal Verification Across DeFi Ecosystems (Invited Talk) Georgiev, Pamina Formal Verification Smart Contracts Formal verification is essential for ensuring the safety of smart contracts in decentralized finance (DeFi), but scaling these techniques across diverse blockchain ecosystems remains a challenge. In this talk, we present our experience making formal verification practical across multiple platforms, including the EVM, Solana, Stellar, and Sui. We discuss how automated reasoning techniques can be adapted to different execution models and programming paradigms while still providing strong correctness guarantees. We focus on what it takes to apply verification in real-world settings: handling complex DeFi primitives, integrating with development workflows, and maintaining usability for engineers. Drawing from verification projects with production protocols, we highlight key challenges and lessons learned in bringing formal methods from theory into practice. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pamina Georgiev 2026 Is Part Of OASIcs, Volume 142, 7th International Workshop on Formal Methods for Blockchains (FMBC 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2026.1 urn:nbn:de:0030-drops-256986 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.1 eng https://creativecommons.org/licenses/by/4.0/legalcode