[ARFC] Strengthening Upgrade Safety: Concord Equivalence Checker by Certora

Service Provider engagements
1

[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.

1 Like