docs(certora): formal-verification follow-up plan#34
Merged
Conversation
Inventory current proof coverage (Phases 1-3 + no-double-claim) and lay out prioritized follow-up phases ordered by economic blast radius: - Phase 3b: deepen RoundVotingEngine/Distributor to aggregate-claimed<=pool, lifecycle monotonicity, single-use refunds (highest value/effort ratio) - Phase 4: QuestionRewardPoolEscrow claim/refund slice - Phase 5-7: LaunchDistributionPool, FrontendRegistry, FeedbackBonusEscrow conservation (reuse ghost-summed pattern) - Cross-cutting: pin certora-cli, revisit via_ir workaround, path-filtered CI gate, mutation testing Includes CVL methodology notes for invariant/ghost/single-use patterns. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ed48c2e289
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| `solc_via_ir = false`. Drop the workaround once upstream covers 0.8.35. | ||
| 3. **Promote CI toward a gate — carefully.** Today it's `workflow_dispatch` + | ||
| weekly cron, non-gating. The next step is **path-filtered, non-required** PR | ||
| runs (trigger only when `contracts/**` or `certora/**` changes), watch runtimes |
There was a problem hiding this comment.
If the future PR trigger is implemented with these literal filters, it will not run for the files this workflow verifies: the repository has no top-level contracts/ or certora/ directories, and the existing Certora job runs from packages/foundry with proofs under packages/foundry/certora and contracts under packages/foundry/contracts. In that context, Solidity or CVL changes would bypass the intended non-required PR lane; the filters should use repo-root globs such as packages/foundry/contracts/** and packages/foundry/certora/**.
Useful? React with 👍 / 👎.
Verified (certora-cli 8.13.1 / solc 0.8.35): per-pool remainingAmount never exceeds fundedAmount (bounds total payouts by funded), and a feedback hash is awarded at most once per pool. Harness exposes the funded/remaining scalars. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Verified: bonded stake never exceeds STAKE_AMOUNT (no overstaking), a second completeDeregister by the same operator reverts (single-use stake return), and slashFrontend reduces stake by exactly amount and only when amount <= bonded stake (bounded slash). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…se proof Verified: the launch verified-bonus is single-use per account (second claim reverts) and a successful claim records the account flag. The per-rater paid<=cap conservation invariant is deferred (true but not self-inductive; needs auxiliary invariants) - documented in the follow-up plan. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Verified: claimCancelledRoundRefund reverts on an Open round (no draining a live round) and on a Settled round (settled rounds pay rewards, not refunds) - refunds are gated to terminal-but-not-settled states. Harness gains round-state and commit-stake getters. Lifecycle monotonicity and single-use refund stay deferred: the engine needs via_ir, under which certora-cli 8.13.1 cannot instrument the internal-function summaries those proofs require, and its auto-finder mis-models settleRound. Documented in docs/testing/certora-security-findings.md. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…roof deferred) Spec + harness for the property 'a refunded reward pool rejects claims' (the require(!refunded) guard runs before any external call, so it is resolution-free). Compiles and type-checks under solc 0.8.35 + via_ir, but the solver run exceeds certora-cli's 15-minute no-output window on this 1,490-line + 11-library contract, so the lane is excluded from the CI matrix and marked proof-deferred. Run manually with a longer prover budget. Harness reads the private rewardPools via the inherited internal _getExistingRewardPool. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…PR trigger - Pin CERTORA_CLI_VERSION to ==8.13.1 (the version the specs were verified against). - Add the four verified Phase 3b/5/6/7 confs to the CI matrix (QRPE excluded: it exceeds the prover output window). - Add a path-filtered pull_request trigger (contracts/** + certora/**) so the lane runs on relevant PRs; still non-required (informational). - Update certora/README.md layout + per-phase status and the follow-up plan doc. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Records what was proved (Phases 3b-7 slices), what could not be proved and the concrete tooling reasons (via_ir blocks internal-function summaries; the cap invariant is true but not self-inductive; QRPE exceeds the prover output window), and a low-confidence manual-review note on LaunchDistributionPool cap accounting. No exploitable vulnerabilities were found. Co-Authored-By: Claude Opus 4.8 <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.
Summary
Adds
docs/testing/certora-followup.md— the continuation plan for the Certora formal-verification effort, picking up where the landed Phases 1–3 + cross-contract no-double-claim proof left off.The plan inventories what is actually proven today vs. deferred, then lays out follow-up phases ordered by economic blast radius first, modeling effort second. Key observation: every existing spec is a single-transition safety slice — none yet proves a property that holds across a round's or pool's full lifecycle, which is where the remaining solvency risk lives.
Proposed phases
RoundVotingEngine/RoundRewardDistributorto proveaggregate claimed ≤ pool(ghost-summed), lifecycle monotonicity, and single-use refunds. Highest value/effort ratio; produces the conservation idiom later phases reuse.QuestionRewardPoolEscrowclaim/refund/recovery slice (the originally-planned-but-unstarted Phase 4), scoped as 2–3 incremental specs.LaunchDistributionPool,FrontendRegistry,FeedbackBonusEscrowconservation, parallelizable.via_ir/solc-0.8.35 workaround viasolc_via_ir_map, promote CI toward a path-filtered (then partly-required) PR gate, add Gambit mutation testing.Includes CVL methodology notes for the deferred property classes (ghost accumulators, explicit
invariant+preservedover parametric rules, single-use patterns) and a soundness watch-list, with sources linked.Docs-only change.
🤖 Generated with Claude Code