ABSTRACT
This paper introduces a novel approach to verify safety properties of legacy smart contracts without complete specifications, leveraging coinductive proof synthesis to handle infinite behaviors and complex control flows.
PAPER · PDF
Loading PDF…
Key findings
Proposes CoindSC, a framework for synthesizing coinductive safety proofs for legacy smart contracts.
Develops a coinductive program logic for EVM bytecode to express safety properties.
Introduces an automated algorithm for synthesizing coinductive proof certificates using constrained Horn clause solving.
Outlines a practical toolchain for analyzing deployed contracts and automatic property inference.
Limitations & open questions
The paper does not discuss the limitations of the proposed approach or any open research questions.