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.
@InProceedings{sorensen:OASIcs.FMBC.2025.11, author = {Sorensen, Derek}, title = {{Formally Specifying Contract Optimizations with Bisimulations in Coq}}, booktitle = {6th International Workshop on Formal Methods for Blockchains (FMBC 2025)}, pages = {11:1--11:13}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-371-3}, ISSN = {2190-6807}, year = {2025}, volume = {129}, editor = {Marmsoler, Diego and Xu, Meng}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.11}, URN = {urn:nbn:de:0030-drops-230382}, doi = {10.4230/OASIcs.FMBC.2025.11}, annote = {Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgradeability} }
Feedback for Dagstuhl Publishing