🚀 DumbContracts Strategic Roadmap: Path to Production Excellence

[Th0rgal]

Vision

Transform DumbContracts from research prototype to the leading production-ready formal verification platform for smart contracts.

Current State

✅ Solid Foundation:

• 3-layer verification (EDSL → IR → Yul)
• 70% property coverage
• 7 example contracts
• Differential testing framework
• 203 theorems proven

⚠️ Gaps:

• Incomplete Ledger proofs (7 theorems)
• Limited documentation for contributors
• Trust boundary at solc compiler
• No real-world standard contracts (ERC20, ERC721)

Strategic Analysis

Report: See /STRATEGIC_IMPROVEMENTS_REPORT.md for comprehensive 20-point analysis

Key Insight: Three strategic thrusts drive impact:

1. Close Known Gaps → Credibility
2. Production Readiness → Adoption
3. Ecosystem Growth → Sustainability

Implementation Roadmap

🎯 Phase 1: Foundation (Months 1-2)

Goal: Solid foundation, onboarding ready

Critical Path

• [Proofs] Complete Ledger sum property helper lemmas #65: Complete Ledger sum proofs ⚡ HIGHEST PRIORITY
• [Documentation] Document trust assumptions and verification boundaries #68: Document trust assumptions
• [Documentation] Create 'Adding Your First Contract' tutorial #66: "Adding Your First Contract" tutorial
• [Integration] Integrate EVMYulLean UInt256 arithmetic library #67: Integrate EVMYulLean UInt256

Outcome:

• ✅ 100% Ledger verification
• ✅ Clear trust boundaries
• ✅ Contributors can onboard in hours

---

🏗️ Phase 2: Production Examples (Months 3-4)

Goal: Real-world contracts verified

High-Value Additions

• [Example Contract] Implement ERC20 standard token with full verification #69: ERC20 implementation
• [Documentation] Create proof debugging handbook #70: Proof debugging handbook
• [Automation] Auto-generate property manifest from Lean files #72: Automated property extraction
• [Integration] Add EVMYulLean precompiled contracts for verified external calls #71: EVMYulLean precompiled contracts

Outcome:

• ✅ Industry-standard contracts proven
• ✅ Reduced developer friction
• ✅ Automated maintenance

---

🚀 Phase 3: Advanced Features (Months 5-8)

Goal: Production-ready platform

Advanced Capabilities

• [Example Contract] Implement ERC721 NFT contract with advanced state modeling #73: ERC721 NFT contract
• [Example Contract] Multi-signature wallet with governance patterns #78: Multi-sig wallet
• [Tooling] Create VS Code extension for DumbContracts development #77: VS Code extension
• [Infrastructure] Add conformance testing against Ethereum test vectors #75: Conformance testing
• [Infrastructure] Proof automation library expansion and optimization #79: Proof automation expansion

Outcome:

• ✅ Complex state models verified
• ✅ Professional developer tooling
• ✅ Cross-validation with Ethereum tests

---

🌱 Phase 4: Ecosystem Growth (Months 9-12)

Goal: Thriving ecosystem, minimal trust

Strategic Enhancements

• [Infrastructure] Formal Yul-to-Bytecode verification (eliminate solc trust) #76: Formal Yul→Bytecode verification
• [Infrastructure] Gas cost modeling and optimization analysis #80: Gas cost modeling
• Community bounty program
• Partnership with auditing firms

Outcome:

• ✅ Zero trust assumptions
• ✅ Production-optimized contracts
• ✅ External contributor growth

---

Issue Dependency Graph

Foundation (Phase 1)
├── #65 Ledger sum proofs ⟹ #69, #73
├── #67 EVMYulLean UInt256 ⟹ #69, #71, #73, #76, #80
├── #68 Trust assumptions
└── #66 First contract tutorial ⟹ #70

Production Examples (Phase 2)
├── #69 ERC20 ⟹ #73
├── #70 Debugging handbook
├── #71 Precompiled contracts
└── #72 Auto property extraction ⟹ #77

Advanced Features (Phase 3)
├── #73 ERC721 (depends: #65, #69)
├── #75 Conformance testing (depends: #67)
├── #77 VS Code extension (depends: #72)
├── #78 Multi-sig wallet (depends: #65)
└── #79 Proof automation (accelerates all)

Ecosystem Growth (Phase 4)
├── #76 Bytecode verification (depends: #67, #71)
└── #80 Gas modeling (depends: #67, #76)

---

Success Metrics

Technical Excellence

• 100% property coverage for all contracts
• Zero trust assumptions in verification stack (phase 4)
• <1 hour build time for all proofs
• Gas costs competitive with hand-written Solidity

Adoption

• 10+ external contributors
• 3+ production contract audits completed
• 100+ GitHub stars
• Featured in formal methods conferences

Documentation

• Complete guides for all workflows
• 90%+ satisfaction in developer surveys
• <1 day time-to-first-contribution
• Video tutorials and demos

Community

• Active Discord/Discussions
• Monthly community calls
• Bounty program active
• Academic collaborations

---

Quick Wins (Start Immediately)

Week 1-2:

1. [Proofs] Complete Ledger sum property helper lemmas #65: Complete Ledger sum proofs (2 weeks)
2. [Documentation] Document trust assumptions and verification boundaries #68: Document trust assumptions (2 days)

Week 3-4:
3. #67: Integrate EVMYulLean UInt256 (3 days)
4. #66: Write first contract tutorial (1 week)

Impact: Foundation solid, contributors can onboard

---

Resource Allocation

By Phase

• Phase 1: 2 person-months
• Phase 2: 3 person-months
• Phase 3: 6 person-months
• Phase 4: 6 person-months

Total: ~17 person-months over 12 months

By Category

• Proofs/Verification: 40% ([Proofs] Complete Ledger sum property helper lemmas #65, [Example Contract] Implement ERC20 standard token with full verification #69, [Example Contract] Implement ERC721 NFT contract with advanced state modeling #73, [Infrastructure] Formal Yul-to-Bytecode verification (eliminate solc trust) #76, [Example Contract] Multi-signature wallet with governance patterns #78)
• Documentation: 15% ([Documentation] Create 'Adding Your First Contract' tutorial #66, [Documentation] Document trust assumptions and verification boundaries #68, [Documentation] Create proof debugging handbook #70)
• Infrastructure: 25% ([Automation] Auto-generate property manifest from Lean files #72, [Infrastructure] Add conformance testing against Ethereum test vectors #75, [Infrastructure] Proof automation library expansion and optimization #79, [Infrastructure] Gas cost modeling and optimization analysis #80)
• Tooling: 10% ([Tooling] Create VS Code extension for DumbContracts development #77)
• Integration: 10% ([Integration] Integrate EVMYulLean UInt256 arithmetic library #67, [Integration] Add EVMYulLean precompiled contracts for verified external calls #71)

---

Risk Mitigation

Technical Risks

Risk	Mitigation	Issues
Proof complexity too high	Invest in automation first	#79
EVMYulLean integration fails	Isolate integration, vendor code	#67, #71
Bytecode verification too hard	Phase 4 (can defer)	#76

Adoption Risks

Risk	Mitigation	Issues
Poor developer experience	Prioritize DX (tooling, docs)	#66, #70, #77
Perceived as academic	Focus on production examples	#69, #73, #78
Competition from Certora/K	Differentiate on usability	All docs

Community Risks

Risk	Mitigation	Issues
Low contributor growth	Tutorial + bounties	#66
Maintainer burnout	Automation + delegation	#72, #79
Lack of adoption	Marketing + real audits	#69, #73

---

Key Decision Points

Month 3: After Phase 1

Decision: Continue to Phase 2 or pivot?
Criteria:

• Ledger proofs complete? ([Proofs] Complete Ledger sum property helper lemmas #65)
• Tutorial working? ([Documentation] Create 'Adding Your First Contract' tutorial #66)
• First external contribution?

Month 6: After Phase 2

Decision: Invest in tooling (Phase 3) or double down on contracts?
Criteria:

• ERC20 complete? ([Example Contract] Implement ERC20 standard token with full verification #69)
• Community size growing?
• Audit opportunities?

Month 9: After Phase 3

Decision: Pursue bytecode verification (Phase 4) or ecosystem growth?
Criteria:

• Production deployments happening?
• Trust assumptions acceptable to users?
• Technical feasibility of [Infrastructure] Formal Yul-to-Bytecode verification (eliminate solc trust) #76 proven?

---

Communication Plan

Monthly Updates

• GitHub Discussions post
• Twitter/X thread
• Progress metrics

Quarterly Reviews

• Retrospective on completed issues
• Adjust roadmap based on feedback
• Community survey

Milestone Celebrations

• Blog post for each phase completion
• Demo videos
• Conference talks

---

Next Steps

1. Review this roadmap with stakeholders
2. Assign [Proofs] Complete Ledger sum property helper lemmas #65 (highest priority) immediately
3. Set up project board with phases
4. Create contributor guide referencing this roadmap
5. Schedule monthly sync for coordination

---

Related Resources

• Full Analysis: /STRATEGIC_IMPROVEMENTS_REPORT.md
• EVMYulLean Repo: https://github.com/NethermindEth/EVMYulLean
• Trust Assumptions: See [Documentation] Document trust assumptions and verification boundaries #68 (to be created)
• First Contract Tutorial: See [Documentation] Create 'Adding Your First Contract' tutorial #66 (to be created)

---

Status: 📋 Planning
Last Updated: 2026-02-14
Next Review: 2026-03-14

---

This roadmap is a living document. Issues and priorities may adjust based on community feedback, technical discoveries, and ecosystem evolution.

[Th0rgal]

🔍 Roadmap Update: Codebase Audit Results

A comprehensive audit has been completed (see #87 for full report). 6 additional critical issues identified that require roadmap adjustments.

Critical Findings

New Critical Issues:

• [Critical] Add CI validation for axiom usage in proof files #82: Axiom validation in CI (CRITICAL - blocks production)
• [Architecture] Formalize storage layout specification to prevent slot collisions #84: Storage layout formalization (HIGH - prevents collisions)
• [Testing] Add multi-seed differential testing to detect flakiness #83: Multi-seed differential testing
• [Testing] Add property tests for reentrancy examples #85: Reentrancy property tests
• [Documentation] Clean up TODO comments and update completion status #86: Documentation cleanup

Revised Phase 1 (Extended to 7 weeks)

Original Phase 1 (2 months):

• [Proofs] Complete Ledger sum property helper lemmas #65, [Documentation] Create 'Adding Your First Contract' tutorial #66, [Integration] Integrate EVMYulLean UInt256 arithmetic library #67, [Documentation] Document trust assumptions and verification boundaries #68

Updated Phase 1 (7 weeks):

1. Week 1-2: [Proofs] Complete Ledger sum property helper lemmas #65 Complete Ledger sum proofs ⚡ HIGHEST
2. Week 2: [Critical] Add CI validation for axiom usage in proof files #82 Add axiom validation ⚡ CRITICAL (NEW)
3. Week 3: [Documentation] Document trust assumptions and verification boundaries #68 Document trust assumptions (must include axioms)
4. Week 3-7: [Architecture] Formalize storage layout specification to prevent slot collisions #84 Storage layout formalization (NEW)
5. Week 6: [Integration] Integrate EVMYulLean UInt256 arithmetic library #67 EVMYulLean UInt256 integration
6. Week 7: [Documentation] Create 'Adding Your First Contract' tutorial #66 First contract tutorial

Rationale: #82 and #84 are production blockers discovered in audit.

Updated Phase 2 (Months 3-4)

Add to existing:

• [Testing] Add multi-seed differential testing to detect flakiness #83 Multi-seed testing (improves all property tests)
• [Documentation] Clean up TODO comments and update completion status #86 Documentation cleanup (enables clearer onboarding)

Updated Phase 3 (Months 5-8)

Add:

• [Testing] Add property tests for reentrancy examples #85 Reentrancy property tests (security demonstration)

Impact on Timeline

Before Audit:

• Total: 17 person-months
• Phase 1: 2 months

After Audit:

• Total: 19 person-months (+2)
• Phase 1: 7 weeks (+3 weeks)

The additional time is essential for production safety.

New Dependency Graph

Phase 1 (CRITICAL PATH)
├── #65 Ledger sum proofs ⟹ #69, #73
├── #82 Axiom validation ⟹ #68, Production ⚡ NEW
├── #84 Storage layout ⟹ #69, #73, #78, Composition ⚡ NEW
├── #68 Trust assumptions (depends: #82)
├── #67 EVMYulLean UInt256
└── #66 First contract tutorial

Phase 2
├── #69 ERC20 (depends: #65, #84)
├── #83 Multi-seed testing ⚡ NEW
├── #86 Doc cleanup ⚡ NEW
├── #70 Debugging handbook
├── #71 Precompiled contracts
└── #72 Auto property extraction

Phase 3
├── #73 ERC721 (depends: #65, #69, #84)
├── #85 Reentrancy tests ⚡ NEW
├── #75 Conformance testing
├── #77 VS Code extension
├── #78 Multi-sig (depends: #65, #84)
└── #79 Proof automation

Updated Success Criteria

Phase 1 Exit Criteria (REVISED):

• Ledger sum proofs complete ([Proofs] Complete Ledger sum property helper lemmas #65)
• Axioms documented and CI-validated ([Critical] Add CI validation for axiom usage in proof files #82) ⚡ NEW
• Storage layout type system working ([Architecture] Formalize storage layout specification to prevent slot collisions #84) ⚡ NEW
• Trust assumptions documented ([Documentation] Document trust assumptions and verification boundaries #68)
• EVMYulLean UInt256 integrated ([Integration] Integrate EVMYulLean UInt256 arithmetic library #67)
• First contract tutorial complete ([Documentation] Create 'Adding Your First Contract' tutorial #66)

Risk Mitigation

Risk: Phase 1 extended by 3 weeks
Mitigation: Critical for production safety, prevents future bugs

Risk: Storage layout (#84) is 5-week effort
Mitigation: Parallelize with other work, start early

Risk: Axiom validation (#82) might find issues
Mitigation: Document soundness arguments first, prove later

Next Steps

1. This week: Assign [Critical] Add CI validation for axiom usage in proof files #82 (axiom validation)
2. Week 2: Begin [Architecture] Formalize storage layout specification to prevent slot collisions #84 (storage layout)
3. Month 2: Reassess timeline after critical issues resolved

See #87 for complete audit report and detailed findings.

[Th0rgal]

Roadmap Progress Update (Feb 2026)

Phase 1 Status — 7/9 items completed

Issue	Description	Status
#82	Axiom validation CI	✅ Completed (PR #88)
#68	Trust assumptions documentation	✅ Completed (PR #89)
#66	First contract tutorial	✅ Completed (PR #90)
#86	Code comment conventions	✅ Completed (PR #91)
#83	Multi-seed testing	✅ Completed (PR #92)
#70	Proof debugging handbook	✅ Completed (PR #94)
#72	Auto-generate property manifest	✅ Closed (already solved)
#65	Complete Ledger sum proofs	📋 Open (requires Lean expertise)
#67	EVMYulLean UInt256 integration	📋 Open (requires Lean expertise)
#84	Storage layout formalization	🔄 Started (PR #98: validation tooling)

Phase 2 Status — infrastructure improvements done

Issue	Description	Status
#96	Multi-seed gas fix	✅ Completed (PR #97)
#93	SumProofs refactoring	✅ Completed (PR #93)

Remaining Open Issues (by category)

Lean proof work (requires Lean 4 expertise):

• [Proofs] Complete Ledger sum property helper lemmas #65 Ledger sum proofs (12 sorry placeholders)
• [Integration] Integrate EVMYulLean UInt256 arithmetic library #67 EVMYulLean UInt256 integration
• [Infrastructure] Proof automation library expansion and optimization #79 Proof automation library expansion

New contracts (large implementation):

• [Example Contract] Implement ERC20 standard token with full verification #69 ERC20 standard token
• [Example Contract] Implement ERC721 NFT contract with advanced state modeling #73 ERC721 NFT contract
• [Example Contract] Multi-signature wallet with governance patterns #78 Multi-sig wallet

Infrastructure (significant engineering):

• [Infrastructure] Add conformance testing against Ethereum test vectors #75 Ethereum conformance testing
• [Infrastructure] Formal Yul-to-Bytecode verification (eliminate solc trust) #76 Yul-to-Bytecode verification
• [Tooling] Create VS Code extension for DumbContracts development #77 VS Code extension
• [Infrastructure] Gas cost modeling and optimization analysis #80 Gas cost modeling
• [Architecture] Formalize storage layout specification to prevent slot collisions #84 Storage layout formalization (started)
• [Testing] Add property tests for reentrancy examples #85 Reentrancy property tests
• [Integration] Add EVMYulLean precompiled contracts for verified external calls #71 EVMYulLean precompiled contracts

Summary

The documentation, testing infrastructure, and CI validation improvements are largely complete. The remaining open issues are primarily deep Lean 4 proof work (#65, #67, #79) and large implementation efforts requiring specialized expertise.

[Th0rgal]

Review Finding: Roadmap Uses Stale "DumbContracts" Naming

This roadmap issue (and all sub-issues #65-#80) reference file paths using DumbContracts/ naming (e.g., DumbContracts/Examples/SimpleToken/, DumbContracts/EVM/Uint256.lean, DumbContracts/Proofs/Stdlib/Automation.lean).

The codebase has been renamed to Verity and all paths now use Verity/ (e.g., Verity/Examples/SimpleToken.lean, Verity/EVM/Uint256.lean, Verity/Proofs/Stdlib/Automation.lean).

This affects every single sub-issue in the roadmap (#65, #67, #69, #71, #73, #75-#80, #84). All file path references in those issues are wrong.

Additional Observations

• Phase 1 progress update (comment Wip/edsl maxstore stdlib #2) is accurate and up-to-date
• The dependency graph is still valid conceptually, just all paths need DumbContracts/ → Verity/ replacement
• Several referenced issues are already closed ([Documentation] Create 'Adding Your First Contract' tutorial #66, [Documentation] Document trust assumptions and verification boundaries #68, [Documentation] Create proof debugging handbook #70, [Automation] Auto-generate property manifest from Lean files #72, [Critical] Add CI validation for axiom usage in proof files #82, [Testing] Add multi-seed differential testing to detect flakiness #83, [Testing] Add property tests for reentrancy examples #85, [Documentation] Clean up TODO comments and update completion status #86)

[Th0rgal]

This roadmap references the old DumbContracts naming and is superseded by docs/ROADMAP.md, TRUST_ASSUMPTIONS.md, and the current issue tracker. Recommend closing in favor of the updated documentation.