2026-08-06T10:10:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23038 2025-10-02T12:30:34Z ddc:004 open_access

Formally Specifying Contract Optimizations with Bisimulations in Coq Sorensen, Derek smart contract verification formal methods interactive theorem prover smart contract upgradeability The efficacy of formal verification of smart contracts depends on being able to correctly specify and carry out the verification of optimized code. However, code optimized for performance is rarely optimized for intelligibility, which can make formally verifying optimized code difficult and costly. To address this issue, we present a formal tool for reasoning about an optimized contract in terms of its reference implementation. This tool reduces the work of formally verifying an optimized contract to proving behavioral equivalence to the reference implementation. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Derek Sorensen 2025 Is Part Of OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2025.11 urn:nbn:de:0030-drops-230382 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.11 eng https://creativecommons.org/licenses/by/4.0/legalcode