[ARFC] Strengthening Upgrade Safety: Concord Equivalence Checker by Certora
Author
Certora
Date
April 2026
We would like to share this proposal with the Aave community to gather early feedback on a new security initiative being developed in collaboration with leading protocols and the Ethereum Foundation.
Note: We are aware of the ongoing efforts around recent ecosystem events and do not expect immediate feedback. This ARFC is shared now for early visibility and initial thoughts, and we are happy to engage in deeper discussion once things stabilize.
Summary
We propose that the Aave DAO participate as a founding sponsor in the development of Certora Concord, an open-source equivalence-checking framework designed to formally verify that smart contract upgrades — including compiler upgrades, optimizations, and refactors — preserve protocol behavior.
Aave would contribute $50,000 USD as part of a co-funded ecosystem initiative, alongside other leading protocols, unlocking matching funding from the Ethereum Foundation.
This initiative introduces a new security primitive for Aave:
Formal, machine-checked guarantees that upgrades do not introduce unintended behavioral changes.
Motivation
Aave is a long-lived, continuously evolving protocol with:
- Frequent upgrades and governance proposals
- Increasing complexity (v4 and multi-chain deployments)
- Strong reliance on safe execution of changes
However, today:
- Even small changes (compiler upgrades, optimizations, refactors) can introduce subtle bugs
- These issues are difficult or impossible to detect via testing alone
- Post-audit changes often require expensive re-audits
This creates:
- Upgrade risk
- Operational overhead
- Slower innovation cycles
Proposed Solution: Certora Concord
Certora Concord is an equivalence-checking framework that:
- Compares two smart contracts at the bytecode level
- Proves whether they are behaviorally equivalent across all possible executions
- Produces counterexamples when differences exist
Unlike testing or fuzzing:
- Concord is exhaustive, not probabilistic
- Covers all inputs and execution paths
- Verifies externally observable behavior (state, calls, events)
In practice
- Compile the same contract with two compiler versions → prove equivalence
- Compare pre/post upgrade contracts → ensure no unintended behavior changes
This directly addresses core risks in Aave’s lifecycle.
Why This Matters for Aave
1. Safer Upgrades
Guarantee that:
- Compiler upgrades
- Gas optimizations
- Refactors
Do not change protocol behavior
2. Reduced Audit Overhead
- Avoid full re-audits for non-functional changes
- Focus audits only where behavior actually changes
3. Governance Confidence
- Provide stronger guarantees for AIPs
- Reduce the risk of introducing bugs through governance
4. Ecosystem Leadership
Aave becomes:
- A founding sponsor of a new verification primitive
- A leader in advancing formal security standards in DeFi
Scope of Work
Certora will:
- Develop Concord, integrated with the Certora Prover
- Provide:
- CLI tooling
- GUI interface for equivalence analysis
- Open-source the tool and documentation
- Maintain and extend Concord for at least 18 months
- Deliver:
- Real-world equivalence analyses
- Documentation and best practices
- Ecosystem-facing education and content
Funding Structure
This is a co-funded ecosystem initiative:
- 4 sponsors (including Aave): $50,000 each
- Total ecosystem funding: $200,000
- Ethereum Foundation match: $200,000
- Total project funding: $400,000
Aave’s contribution unlocks:
- Additional funding from the Ethereum Foundation
- Shared development costs across leading protocols
Timeline
- Initial production-ready version: 3 months
- Ongoing development & maintenance: 15+ months
Deliverables include:
- Tooling
- Documentation
- Case studies
- Continuous improvements
Benefits to Aave
Technical Benefits
- Early access to Concord tooling
- Ability to apply it directly to Aave upgrades
- Reduced upgrade risk and audit overhead
Strategic Benefits
- Recognition as a Concord Ecosystem Sponsor
- Visibility in:
- Technical publications
- Case studies
- Ecosystem initiatives
Financial Efficiency
- Leverages Ethereum Foundation matching → amplified impact per dollar
Specification
The proposal requests:
- A one-time payment of $50,000 USD
- Paid to Certora for Concord development
- Subject to standard DAO execution process
Next Steps
- Gather community feedback on this ARFC
- If consensus is reached:
- Move to Snapshot vote
- If Snapshot passes:
- Submit AIP for execution
Disclaimer
Certora is presenting this proposal independently and is not compensated by any third party for creating this ARFC.
Copyright
Copyright and related rights waived via CC0.