Closed
Conversation
Add detailed documentation of the verification architecture, current status, and roadmap to help contributors understand the project state and next steps. New Documentation: - `docs/VERIFICATION_STATUS.md` - Complete verification status guide - Layer 1 (EDSL ≡ ContractSpec): 100% complete, all 7 contracts verified - Layer 2 (ContractSpec → IR): 100% complete, all IR generation proven - Layer 3 (IR → Yul): Semantics complete, statement equivalence pending - Property test coverage: 63% after pending PRs, 89 remaining all proof-only - Trust assumptions and verified components breakdown - Concrete next steps for completing Layer 3 Updated README.md: - Added link to verification status documentation - Shows current verification progress prominently Key Insights Documented: - Layer 3 blocker: Statement-level equivalence proofs needed - Requires proving each IR/Yul statement type matches - Fuel-parametric approach needs statement-level lemmas - Alternative approaches documented if current method is too complex - Property extraction essentially complete (all addressable properties covered) - Differential testing production-ready (10k+ tests, 8-shard CI) Benefits: - New contributors can understand verification architecture - Clear roadmap for completing Layer 3 - Documents what's complete vs. what's blocked - Helps stakeholders understand trust assumptions - Provides concrete next steps for each verification layer Target Audience: - Researchers evaluating formal verification approaches - Contributors wanting to help complete Layer 3 - Users understanding what's proven vs. trusted - Maintainers tracking verification progress Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Th0rgal
added a commit
that referenced
this pull request
Feb 14, 2026
Member
Author
|
Superseded by consolidated PR #24 which includes all changes |
This was referenced Feb 15, 2026
Th0rgal
pushed a commit
that referenced
this pull request
Apr 15, 2026
…ge writes The CEI (Checks-Effects-Interactions) validator previously used `stmtIsPersistentWrite` which returned false for internal calls, so a pattern like `externalCallBind(...); internalCall(helper, [...])` where the helper writes storage would silently pass CEI validation. Add `stmtMayPersistentlyWrite` — a conservative variant that treats `internalCall` and `internalCallAssign` as potential persistent writes (since their callee bodies are not visible at single-function scope). Use it in the CEI write-after-call check. Note: internal calls do NOT set `seenCall` for CEI purposes — each callee function has its own CEI validation, so treating internal calls as both interactions and writes would produce false positives on contracts like DirectHelperCallSmoke. Also fix a guard_pending state leak in generate_macro_property_tests.py where `#guard_msgs in` / `#check_contract Foo` would incorrectly skip the next `verity_contract` declaration (affected RolesCEISmoke, ModifiesRolesSmoke, UnsafeCEICompliant property test generation). Addresses P1 review threads #23 and #5 on PR #1731. Co-Authored-By: Claude Opus 4.6 <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
Add comprehensive verification status documentation that provides visibility into the verification architecture, current progress, and roadmap.
What This PR Does
Introduces detailed documentation to help contributors, researchers, and users understand:
New Documentation
docs/VERIFICATION_STATUS.mdComprehensive guide covering:
Verification Layers:
Layer 3 Blocker Analysis:
stmt_equivhypothesisProperty Test Coverage:
Trust Assumptions:
Roadmap:
README.md Updates
Added prominent link to verification status documentation showing current progress.
Why This Is High-Leverage
For Contributors:
For Researchers:
For Users:
For Maintainers:
Key Insights
Testing
Documentation reviewed for:
Benefits
🤖 Generated with Claude Code
Note
Low Risk
Documentation-only changes (new markdown + README edit) with no impact on code, proofs, or build/test behavior.
Overview
Adds a new
docs/VERIFICATION_STATUS.mddocument that consolidates the verification architecture (Layers 1–3), current completion status, trust assumptions, property/differential testing coverage, and a roadmap/next steps for finishing Layer 3.Updates
README.mdto fix a heading typo and add a prominent link to the new verification status page.Written by Cursor Bugbot for commit 9ca686d. This will update automatically on new commits. Configure here.