Certora <> Compound Formal Verification
01Summary
Proposal to enhance Compound protocol security through a 12-week annual engagement with Certora for formal verification services, including: (1) access to Certora Prover for code reviewers, (2) allocation of 3 security engineers to review code changes and propose correctness rules, and (3) establishment of a community of security researchers. All code changes and governance proposals will be reviewed using formal verification tools. On-chain action: Stream 16,722,407.99 COMP tokens to 0x0F11640BF66e2D9352d9c41434A5C6E597c5e4c8 over ~16 weeks starting March 26, 2023.
- Type
- treasury allocation
Key changes
- Grant access to Certora Prover source code to code reviewers under NDA(high)
- Allocate team of 3 Certora security engineers for 12 weeks per annum to review code changes and propose correctness rules(high)
- Establish community of security researchers to review code changes and propose new correctness rules(medium)
- Implement continuous formal verification for all code changes and governance proposals(high)
- Stream 16,722,407.99 COMP tokens to Certora for services over approximately 16 weeks(high)
Generated by Kvorum
02Description
Certora <> Compound Formal Verification
We propose to improve the security and agility of the Compound protocol via continuous formal verification in three ways: (1) By granting access to the Certora Prover to anybody checking the Compound code. This includes accessing the Certora Prover’s source code under NDA. (2) By allocating a team of 3 Certora security engineers for 12 weeks per annum to review code changes and propose new correctness rules. (3) By creating a community of security researchers to review code changes and propose new correctness rules. Every code change and governance proposal will be reviewed by both internal and external teams using the Certora prover to prevent bugs when the code is upgraded.
See the full forum discussion here: https://www.comp.xyz/t/security-and-agility-of-compound-smart-contracts-via-continuous-formal-verification/4007
03Mismatch analysis
The description is a high-level narrative about a formal-verification partnership with Certora (Prover access, a dedicated engineering team, and a security researcher community) but gives no numeric or address-level details. The calldata reveals the concrete mechanism: an ERC20 approve of ~16,722.4 COMP followed by a createStream call funneling that same amount to a specific address over roughly 183 days (about 26 weeks). Two issues stand out: (1) the actual payment amount and recipient are never disclosed in the prose, which is material given the transfer represents Compound treasury funds; and (2) the stated cadence of 'and 12 weeks per annum' doesn't clearly correspond to the ~26-week continuous stream duration, creating a moderate mismatch in the described time commitment vs. the on-chain vesting period. Neither the target contract addresses nor the amounts are contradicted outright — there's no evidence of fund redirection to an unrelated party or a wildly different magnitude — so this doesn't rise to severe. But the lack of any quantifiable disclosure plus the duration ambiguity is enough that a careful delegate should be alerted before voting, making this a material discrepancy rather than merely minor or cosmetic. Confidence is medium because the description is intentionally high-level, making some judgment calls necessary when mapping vague prose to precise calldata parameters.
Discrepancies
- mediumomitted in description
The proposal executes a concrete on-chain payment of ~16,722 COMP tokens (worth a substantial sum) to a specific address via approve+createStream, but the description never states the compensation amount, the token/stream mechanism, or the recipient address. Voters approving this text have no way to verify the size or destination of the transfer from the prose alone.
“allocating a team of 3 Certora security engineers for 12 weeks per annum”
- mediumvalue mismatch
The description frames the engagement as '12 weeks per annum' of security engineer time, implying a roughly quarter-year cadence, but the on-chain stream actually vests continuously over ~183 days (~26 weeks, roughly double the stated period). This creates ambiguity about whether the payment reflects 12 weeks of work stretched over 6 months, or a longer engagement than described.
“for 12 weeks per annum”
Generated by Kvorum
04Actions
- Target
- 0xc00e…6888
- Value
- 0 wei
- Function
- approve(address,uint256)
- Arguments
{ "0": "0xCD18eAa163733Da39c232722cBC4E8940b1D8888", "1": "16722407999999999750400" }- Calldata
- Target
- 0xcd18…8888
- Value
- 0 wei
- Function
- createStream(address,uint256,address,uint256,uint256)
- Arguments
{ "0": "0x0F11640BF66e2D9352d9c41434A5C6E597c5e4c8", "1": "16722407999999999750400", "2": "0xc00e94Cb662C3520282E6f5717214004A7f26888", "3": "1680673189", "4": "1696484389" }- Calldata
05Tally
Summed from votes
06Voters
No votes recorded yet.
07Forum
- Security and Agility of Compound Smart Contracts via Continuous Formal Verification ↗discourse · high confidence
Arguments for
- Formal verification with Certora complements audits and testing by finding a different class of hard-to-detect critical bugs, as demonstrated in past work with Compound and Aave.— sofiviss, msagiv, dvf, pennblockchain
- The price is justified given Compound's large TVL and the potentially far greater cost of a hack, and Certora is showing alignment by accepting part payment in vested COMP and offering a steep discount.— sofiviss, pennblockchain
- Continuous integration of the Certora Prover into the CI/CD pipeline allows every code change to be checked before and after audits, similar to a compiler check.— sofiviss, msagiv
- The proposal builds community security capacity through free Prover access, courses, office hours, and grant-funded rule-writing competitions open to the whole ecosystem.— sofiviss, pennblockchain
- Prior real-world engagements (Aave, OUSD) show formal verification adds a valuable, complementary security layer and produced concrete bug-catching results.— dvf, sofiviss
- Reducing the proposal to a 6-month trial period at lower cost allows Certora to demonstrate value before a longer commitment, following the same successful pattern used with Aave.— sofiviss
Arguments against
- The proposed cost is very high and may be unsustainable given Compound's relatively low revenue compared to its existing fixed security/operations costs.— RapidsCapital, VonNeumann2022, ClairvoyantLabs
- A pay-per-service model (paying Certora only when it finds issues, alongside other security vendors) would be a more appropriate and cost-effective arrangement than a large annual retainer.— ClairvoyantLabs, RapidsCapital
- Formal verification does not guarantee safety, as shown by protocols like Euler that were hacked despite having been formally verified or extensively audited, casting doubt on the value proposition.— ClairvoyantLabs
- Compound III (Comet) is already formally verified and architecturally 'complete' via its factory model, reducing the need for extensive new verification work going forward.— rleshner
- The proposal lacks a clear plan for how community developers would actually adopt and use the Certora tools, risking low uptake despite the investment.— rleshner
- Security-related funding of this kind should go through the existing grants program (which has a dedicated security section) and be part of a holistic, needs-based security strategy rather than a standalone proposal.— rleshner
- Aave's positive experience and vote outcome with Certora does not automatically justify a similar arrangement or expenditure for Compound.— ClairvoyantLabs
Unresolved concerns
- Whether the overall cost (even at the reduced 6-month/$750k level) is sustainable relative to Compound's actual protocol revenue.— RapidsCapital, VonNeumann2022, ClairvoyantLabs
- Whether a pay-per-service or multi-vendor security purchasing model would be preferable to a fixed retainer arrangement with Certora.— ClairvoyantLabs, RapidsCapital
- Whether formal verification meaningfully reduces real-world hack risk given examples (e.g., Euler) where verified or audited code was still later exploited.— ClairvoyantLabs
- Whether continuous, large-scale formal verification is even necessary given Comet's 'complete' factory-based architecture and lack of anticipated major code changes.— rleshner
- How community developer adoption of the Certora tools would actually be driven and measured, beyond just making them available.— rleshner
Notable participants
- sofivissCertora representative and proposer who authored the proposal, responded to nearly all objections, and later revised it to a 6-month trial.
- ClairvoyantLabsPersistent critic who repeatedly questioned cost, referenced prior threads, and cited hacks (Euler) to challenge formal verification's value.
- RapidsCapitalRaised sustainability and revenue concerns and echoed calls for an alternative pay-per-service model.
- VonNeumann2022Questioned whether the proposal's cost was sustainable and could be reduced.
- pennblockchainSupportive voice arguing the pricing was competitive given market conditions and asked for clarity on the community grant allocation.
- dvfShared positive prior experience using Certora on OUSD and clarified the timeline of the Euler bug relative to Certora's audit.
- msagivCertora team member who reinforced that continuous verification aims to prevent Euler-like gaps from unreviewed code changes.
- rleshnerPosted a detailed, influential rejection near the end of the thread citing Comet's completeness, lack of adoption plan, and preference for grants-based funding.
- ClementBarbierUnrelated audit firm representative promoting an alternative service (Omniscia), not substantively engaging with the proposal's merits.