Summary
Solidity compiler upgrades are one of the most underappreciated sources of silent risk in smart contract systems. Even with unchanged source code, a new compiler can produce materially different bytecode — in ways that testing and manual review routinely miss.
For Lido, where protocol correctness underpins billions in staked assets, this demands formal proof. This proposal requests LEGO funding to deploy Certora Concord as a machine-checked equivalence guardrail for Lido’s compiler upgrade process.
Deliverables include formal equivalence results for selected Lido contracts, a reusable Concord configuration for future upgrades, and a technical report establishing ecosystem best practices.
Motivation and Background
Solidity compiler upgrades are unavoidable for long-lived protocols. New compiler versions introduce security fixes, optimizer changes, code generation improvements, and support for new language features.
However, compiler upgrades also carry non-trivial risk. Changes in optimization strategies, code layout, or edge-case semantics can introduce behavioral differences even when the Solidity source code is unchanged or minimally modified. These differences are often extremely difficult to detect via testing or manual review.
For a protocol like Lido, where correctness and upgrade safety are critical, there is currently no systematic way to prove that recompiling contracts with a newer Solidity compiler preserves protocol semantics.
Certora Concord Overview
Concord is Certora’s equivalence-checking framework, built on top of the battle-tested Certora Prover. Rather than testing sampled inputs, Concord reasons symbolically across all possible executions — providing exhaustive guarantees that two contract implementations behave identically with respect to state transitions, emitted events, and external calls.
For Lido’s use case specifically, this means compiling the same protocol contract under two different Solidity versions and formally proving the outputs are behaviorally identical. Where divergence exists, Concord produces concrete counterexamples pinpointing exactly how and where behavior differs — enabling targeted investigation rather than broad re-auditing.
Compiler-Version Equivalence with Concord
In the proposed workflow, the same Solidity contract is compiled using two different compiler versions. The resulting bytecode artifacts are then compared using Certora Concord.
Concord checks that the two compiled implementations are equivalent with respect to externally observable behavior, including state transitions, emitted events, and external calls. Internal differences in control flow, instruction selection, or optimization strategy are abstracted away.
If Concord identifies non-equivalence, it produces concrete counterexamples demonstrating how behavior can diverge between compiler versions, enabling targeted investigation and mitigation.
Proposed Work and Milestones
Phase 1 - Scope Definition and Pilot Selection. Collaborate with the LEGO Council and Lido contributors to select a representative set of Lido contracts and relevant compiler version upgrades to serve as pilot cases.
Phase 2 - Concord Configuration and Specification. Define the equivalence boundaries and observable behaviors relevant for compiler-version equivalence, and configure Concord accordingly.
Phase 3 - Equivalence Verification. Run Concord proofs comparing bytecode produced by different compiler versions. Analyze any counterexamples and iterate on specifications as needed.
Phase 4 - Documentation and Ecosystem Deliverables. Package the resulting methodology, tooling configuration, and findings into reusable documentation for future Lido compiler upgrades.
Deliverables
The project will deliver formal equivalence results for selected compiler upgrades, a reusable Concord setup for compiler-version equivalence checking, and a final technical report documenting methodology, findings, and recommended best practices.
Expected Impact on the Lido Ecosystem
This work provides Lido with strong, formal guarantees that compiler upgrades do not introduce unintended behavioral changes. It significantly reduces upgrade risk and increases confidence in adopting newer Solidity compiler versions.
More broadly, it establishes a principled, reusable approach to managing compiler risk for long-lived smart contract systems, benefiting the entire Lido ecosystem.
Timeline and Budget
To support the development, deployment, and long-term maintenance of Concord, Certora proposes a co-funded model involving leading Web3 organizations (the “Sponsors”), including Lido, alongside the Ethereum Foundation.
Certora is seeking a contribution of $50,000 USD from each Sponsor. These funds will directly support the development, open-sourcing, documentation, and community adoption of Concord, as outlined in this proposal.
The Ethereum Foundation has expressed preliminary support for the initiative, and Certora will be applying for a matching grant through its formal review process.
An initial production-ready version supporting Vyper and Solidity, accompanied by comprehensive documentation and a coordinated marketing campaign featuring examples from participating teams, will be delivered within three (3) months.
Over the subsequent fifteen (15) months, Certora will focus on ongoing enhancements, feature expansion, and maintenance of Concord to ensure continued reliability, ecosystem alignment, and long-term sustainability.