# \[ARFC\] Strengthening Upgrade Safety: Concord Equivalence Checker by Certora **URL:** \ **Category:** Service Provider engagements\ **Created:** [April 23, 2026, 12:57pm UTC](https://governance.aave.com/t/arfc-strengthening-upgrade-safety-concord-equivalence-checker-by-certora/24713 "2026-04-23T12:57:05Z")\ **Posts on this page:** 4\ **Page:** 1
**Author:** ![Certora](https://dub1.discourse-cdn.com/flex013/user_avatar/governance.aave.com/certora/32/6230_2.png) [@Certora](https://governance.aave.com/u/Certora)\ **Post date:** [April 23, 2026, 12:57pm UTC](https://governance.aave.com/t/arfc-strengthening-upgrade-safety-concord-equivalence-checker-by-certora/24713/1 "2026-04-23T12:57:05Z")
# **[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: 1. Develop **Concord** , integrated with the Certora Prover 2. Provide: - CLI tooling - GUI interface for equivalence analysis 3. Open-source the tool and documentation 4. Maintain and extend Concord for **at least 18 months** 5. 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** 1. Gather community feedback on this ARFC 2. If consensus is reached: - Move to Snapshot vote 3. 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. ---
**Author:** ![Abel189](https://avatars.discourse-cdn.com/v4/letter/a/c67d28/32.png) [@Abel189](https://governance.aave.com/u/Abel189)\ **Post date:** [June 20, 2026, 6:21pm UTC](https://governance.aave.com/t/arfc-strengthening-upgrade-safety-concord-equivalence-checker-by-certora/24713/2 "2026-06-20T18:21:07Z")
I support this proposal. Aave is one of the most actively maintained and continuously evolving protocols in DeFi. As the protocol grows across multiple chains and moves toward increasingly sophisticated architectures, the ability to verify that upgrades preserve intended behavior becomes more valuable. The proposed Concord framework addresses a real challenge. Many upgrade-related risks do not come from new functionality but from compiler changes, optimizations, refactoring, or implementation details that are difficult to fully validate through testing alone. A formal equivalence-checking framework could provide an additional layer of assurance before governance-approved upgrades reach production. The requested contribution is modest relative to the potential benefits. In addition, the Ethereum Foundation matching structure effectively doubles the impact of the ecosystem funding and helps create a shared security resource that can benefit multiple protocols. While the practical effectiveness of the framework will ultimately be demonstrated through adoption and real-world use cases, the cost-to-benefit ratio appears attractive and aligns well with Aave’s long-standing commitment to security leadership and rigorous engineering standards. For these reasons, I support moving this initiative forward. ---
**Author:** ![pdiomede-certora](https://dub1.discourse-cdn.com/flex013/user_avatar/governance.aave.com/pdiomede-certora/32/15089_2.png) [@pdiomede-certora](https://governance.aave.com/u/pdiomede-certora)\ **Post date:** [June 23, 2026, 1:35pm UTC](https://governance.aave.com/t/arfc-strengthening-upgrade-safety-concord-equivalence-checker-by-certora/24713/3 "2026-06-23T13:35:02Z")
The **[Snapshot vote](https://snapshot.org/#/s:aavedao.eth/proposal/0xcf9ca2d7a9b1ee819b6b76f8dae1cdc7fb507e027f044e90d7937b4b264a42c1/discussion)** for this ARFC has concluded and passed with 100% suppor. Final result: - For: 357.6k, 100% - Against: 0 - Abstain: 0 Thank you to the Aave community for the support and feedback throughout the ARFC process. Certora will now coordinate the next step in the standard Aave DAO execution process and work with the relevant governance contributors to move this proposal to the AIP stage, including finalizing the execution payload and payment details for the approved $50,000 USD funding request for Concord development. ---
**Author:** ![AaveLabs](https://dub1.discourse-cdn.com/flex013/user_avatar/governance.aave.com/aavelabs/32/6388_2.png) [@AaveLabs](https://governance.aave.com/u/AaveLabs)\ **Post date:** [June 24, 2026, 3:30pm UTC](https://governance.aave.com/t/arfc-strengthening-upgrade-safety-concord-equivalence-checker-by-certora/24713/4 "2026-06-24T15:30:28Z")
The AIP for this proposal was successfully created, [proposal#500](https://app.aave.com/governance/v3/proposal/?proposalId=500), voting will start in less than 24hs.