Conversation
CVL syntax spike (certora-cli 8.18.0 local; CI pin 8.6.1 untested): - Q1 tuple-return summary: syntax OK, binding not load-bearing (ledger A3) - Q2 Math.Rounding as CVL param + assert_uint8: works - Q3 wildcard summary on library internal fn: works Q3 was proved by sentinel rather than by typecheck: a summary naming a function that exists nowhere typechecks with exit 0 and no warning, so only a rule that fails when the binding is absent actually answers it. Prover: https://prover.certora.com/output/1392759/75136955b8c64624beeedc3c439083c7 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ghost-backed asset model and mulDiv closed form, activated in a leaf base spec. Harness adds donate() to model unbacked asset inflows; deliberately exposes no share mint/burn, since an unbacked share mint is what the solvency and rate-monotonicity properties forbid. Prover: https://prover.certora.com/output/1392759/06cda2c815be46cda4f0e7daaa8c3e25 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
previewRedeem(totalSupply()) <= totalAssets(), stated as a rule rather than an invariant. The property needs no induction: it holds in every state with no relation between totalSupply and totalAssets, since floor(x) <= A iff x < A+1 reduces the obligation to 0 < (A+1)K. Quantifying over all sane states is both stronger than quantifying over reachable ones and far cheaper - as an invariant it returned UNKNOWN on every method. Also adds the shared sum-of-balances ghost. Note that importing a spec makes its invariants assumable but not proved; `use invariant` is what proves them. Verified: https://prover.certora.com/output/1392759/aa28b0f58dd74d49a4bfe3e5138f703a Mutation (_convertToAssets forced to Ceil) correctly VIOLATED: https://prover.certora.com/output/1392759/400c3aee9dad44289661bb075a8a28d4 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
No round trip creates value, and per-operation leakage is bounded at one unit in both directions. The bounds are paired with reachability witnesses, without which `gap <= 1` would be satisfied by a gap that is always zero. Prover run: https://prover.certora.com/output/1392759/1e8a438118444bd7aff1755d2589b57d?anonymousKey=b2b0e29a4f1e586b4eecaa73d5fd247f1c96c407
The max functions agree with the previews, and the limits they advertise are actually reachable: redeem(maxRedeem(o)) and withdraw(maxWithdraw(o)) never revert. Both liveness rules fix owner == msg.sender, so the claim covers self-withdrawals only; the allowance path is left to the conservation rules. Adds a noVirtualOverflow scope definition. The virtual-asset design computes totalAssets() + 1, which reverts when the vault holds the whole uint256 range. Stated on both liveness rules rather than only the one that needs it, so neither relies on a preview call reverting to prune the state for it. Prover run: https://prover.certora.com/output/1392759/46832ab7c6954ba1a471aa24de45b09f?anonymousKey=efa79148b605bc5e1b24e6f092a3f3cb23f65747
One rule per state-changer: share and asset deltas, allowance spend on the third-party path, and isolation against a free `other` parameter the prover quantifies over universally. Supporting machinery for the value properties, which all assume the operations move the right amounts between the right parties. Previews are read before the operation, since afterwards the operation has moved both sides of the conversion. The allowance assertions treat infinite approval separately, which ERC20 leaves untouched by design. Prover run: https://prover.certora.com/output/1392759/6e66a0d667e945f4b5f5962aa71ac6de?anonymousKey=b5a8cc0780bb79eb02256ee7fed7a386ad74c5bd
A positive rule list is a coverage claim that decays: a newly added rule is silently unverified and the suite still goes green. The complement shard carries the same list under exclude_rule, so the two tile the rule space and anything not named lands in the complement rather than going unrun. Both confs are identical apart from the selector and the message, so a pass in one and a timeout in the other says something about the rules rather than the configs. The builtin sanity rule lives in the complement: it is a property of the scene rather than of the vault, and it keeps that shard non-empty, which the prover requires. Prover runs: https://prover.certora.com/output/1392759/749da38c0d8f4cf0812116f9c3e12070?anonymousKey=2894d8e2c220b53101eccee6a90ed95ef4033bbd https://prover.certora.com/output/1392759/ac9ea159bfa14eea968d10ef4fe3c082?anonymousKey=675379c58c214b9cd3a882ec08ffea4aadba0e73
Snapshot replay for deposit and withdraw plus a donation-interleaved variant, with the inequality directions derived from the rounding mode and assert_uint256 on the combined amount so an overflowing sum fails rather than being assumed away. Adds a third shard for these rules. An isolation probe showed the replay machinery is nearly free and the whole cost is the nested-floor share math, so the shard forces nonlinear arithmetic, turns splitting off, and races ten solver seeds. That takes the closed-form obligation from a timeout to a second. depositIsNotSplittable is discharged. The withdraw mirror and the donation variant still exceed the solver budget: both hold under exhaustive and random sampling, so this is cost rather than a defect. Both are annotated in the spec and excluded from every shard, so their absence is not readable as a pass. Prover runs: https://prover.certora.com/output/1392759/8ed8cb59ae59465fbc77462232f52710?anonymousKey=6076baa48f1f53a2de5816970454097a6f57d527 https://prover.certora.com/output/1392759/ac6bd6eb4d204b1e93a4c3768a91a61a?anonymousKey=7843c2de77fbc66261c3113df100673536ec4ec1 https://prover.certora.com/output/1392759/3a96491c44644ff7a907289cf4aa0f0d?anonymousKey=f0d7646fe86dd27462f7e79f2d082a9bdc9bea77
Parametric over every non-view harness method, donate() included, so the raw asset-inflow vector is inside the claim rather than outside it. Deposits round shares minted down and withdrawals round shares burned up, so the rounding residue stays with the vault and the price per share can only rise or hold. Verified RED under a temporary unbacked share mint on the harness, which is the hazard the contract documents. Prover run: https://prover.certora.com/output/1392759/99fd77b65bee4a0bb02d55fcab99af64?anonymousKey=3ef3ce7831c2fea1f8a72abd7e8ce9fc1e7a86e8
Donations never reduce what an existing holder can redeem, and neither do asset inflows arriving by any other means. The second rule writes the asset ghost directly, so it covers inflows no transaction on this contract can produce: yield accrual, a rebase up, a raw transfer from an address that never calls the vault. Verified RED under a transposed mulDiv in _convertToAssets. Note that inflating the denominator or ignoring totalAssets entirely both leave these rules green: a mutation that weakens a quantity uniformly does not test a monotonicity property, only one that reverses the direction does. Prover run: https://prover.certora.com/output/1392759/eb81dc3dd3374756afd34a4d2a1ea03a?anonymousKey=eaf15defb0c27dc27735c935b348f717fa0046aa
The inflation-attack non-profitability claim, in its own tuned config: enter, inflate the rate with a donation, let a victim deposit, exit, and assert the attacker's asset balance never rises. Scoped to a vault that starts empty. That is what the virtual-shares mitigation claims and the only scope in which the claim holds: from an arbitrary state the sequence is profitable, but only because a vault holding assets against no shares is already manipulated, so the attacker profits on a price someone else paid to inflate. Requiring an empty vault makes them pay for the manipulation themselves. The contract is explicit that the mitigation does not fully prevent the attack and that empty vaults are the hazard, so this records the narrower claim rather than the general one. Verified RED under a mutation restoring pre-v4.9 behaviour without virtual assets and shares. Prover run: https://prover.certora.com/output/1392759/3646df758a544c35aaa4124b06f3b513?anonymousKey=cd942582582f46d66424c98761caf8023ea3b861
The timeout ledger goes in the workflow, next to the job that would have run the rules it lists, so it is re-read whenever that job changes. The soundness ledger goes in the spec files: what a rule narrows on the rule, what a file assumes at its top. Both halves then travel with the code. Fixes a CI break this suite would otherwise introduce. The workflow selected specs by changed basename and mapped each to a same-named config, but ERC4626Base.spec has no config of its own, so a labelled PR touching it invoked a missing config and failed the job. A changed helper spec had the opposite problem and selected nothing at all. Selection now maps a changed spec to every config whose verify target names it, falling back to a full run when no config does, since such a spec is a shared import. That also lets a change to ERC4626.spec reach all three of its shards rather than only the one sharing its name. The verify job no longer installs Foundry. certoraRun reads `forge remappings` when forge is present, which emits a `hardhat` key that package.json also provides, and rejects the duplicate. The job has no use for forge. Prover runs: https://prover.certora.com/output/1392759/cee60a07375e4f128c3ef351730cab16?anonymousKey=32ec067a5c77139114935c728ee00dc1838af2dc https://prover.certora.com/output/1392759/47a8d21b7b8b495f9ad560a7e6221a71?anonymousKey=1e53632b61bb42e651eafb11afcdaa64945d92bd
Every other spec in the suite runs at _decimalsOffset() == 0, where the offset is the identity, so nothing proved there says the offset does anything. This tier leaves the offset symbolic and re-proves solvency and the donation sandwich over offsets 0 through 77. It also adds inflationCostScalesWithOffset, the claim only a symbolic offset can state: a deposit rounds to zero shares only when the vault already holds at least 10**offset times that deposit, so the offset is the multiplier between what a victim loses and what robbing them costs. That is the "orders of magnitude more expensive than it is profitable" claim in ERC4626's own documentation, which no zero-offset rule can express. The symbolic exponent needed no ghost abstraction and no bound on the offset, so the tier adds nothing to the suite's assumptions. Prover runs: https://prover.certora.com/output/1392759/9afe1d75a84d4fdb81e362adfca9eb9c?anonymousKey=b9b5fd2f43c56b3309c36eb0b0c34dfdac52a156 https://prover.certora.com/output/1392759/0fe2b8f4b74e473293625695201e1a7b?anonymousKey=c1359ac05eba0704a61961551c864cf982506cb9 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Drop the vacuity guards rule_sanity already provides, the donate()-only inflow rule subsumed by the ghost-write one, and the zero-offset solvency rule subsumed by the symbolic-offset proof. Merge ERC4626_rest.conf into ERC4626.conf via exclude_rule so the shards tile by construction. Dedupe and trim the spec prose. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
EperezOk
force-pushed
the
fv/erc4626-certora
branch
from
August 29, 2026 05:35
377c6eb to
3500ada
Compare
A base or helper spec is verified by no config of its own. Rather than escalate to --all implicitly, fail with a pointer to the formal-verification-force-all label so the author opts into the full run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
EperezOk
changed the title
A changed base, helper or methods spec is verified through the specs that import it, transitively, so touching one runs exactly the configs it can affect instead of failing or running everything. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a Certora suite for
ERC4626, verifying the vault against a symbolic asset token and a closed-formmulDivmodel.Properties (rule names in parentheses):
vaultNeverOvercommitted).roundTripNeverCreatesValue,roundingGapIsAtMostOne,*GapCanBeOne).maxRedeem/maxWithdraware consistent with the previews, and redeeming or withdrawing the advertised max never reverts (maxBoundaryIsConsistent,*MaxNeverReverts).depositIsNotSplittable).rateNeverDecreases).assetInflowNeverHarmsHolders).donationAttackNeverProfits).aassets to mint zero shares, the vault must already hold at leasta · 10^offsetassets, so the attack costs the attacker10^offsettimes what it takes from the victim (inflationCostScalesWithOffset).*Conserves).Layout:
ERC4626Base.specholds the summary layer and states everything the suite assumes rather than proves;ERC4626.spec(tiers 1–2),ERC4626Donation.spec(tier 3) andERC4626Offset.spec(tier 4, symbolic_decimalsOffset()) hold the rules. Two anti-splitting rules time out and are recorded in the ledger infv-certora.yml.Also fixes the workflow's changed-spec → config mapping, which assumed one config per spec and did not follow imports.
PR Checklist
npx changeset add)