Strategic Development Roadmap

[Th0rgal]

Strategic Development Roadmap

This discussion complements Issue 81 with community input on prioritization and implementation strategy.

Current State

The framework provides:

• 9 example contracts with 296 proven theorems
• 3-layer verified compilation (EDSL → IR → Yul → Bytecode)
• 290 tests across 23 test suites
• Comprehensive continuous integration with 15+ validation scripts

Open Technical Challenges

From the 14 open issues, categorized by type:

Soundness and Completeness

1. Issue 65: Complete Ledger sum property proofs (12 remaining sorry statements)
2. Issue 84: Formalize storage layout specification (prevent slot collisions)
3. Issue 76: Formal Yul-to-Bytecode verification (eliminate compiler trust)

Standard Contract Implementations

4. Issue 69: ERC20 token standard (estimated 3 weeks)
5. Issue 73: ERC721 NFT standard
6. Issue 78: Multi-signature wallet with governance

External Dependencies

7. Issue 67: EVMYulLean UInt256 arithmetic library integration
8. Issue 71: EVMYulLean precompiled contracts for verified external calls
9. Issue 75: Ethereum conformance testing against reference vectors

Tooling and Infrastructure

10. Issue 77: VS Code extension for development
11. Issue 79: Proof automation library expansion
12. Issue 80: Gas cost modeling and optimization analysis

Discussion Topics

1. Prioritization Criteria

Which issues provide the most value for:

• Soundness guarantees (eliminate axioms, complete proofs)
• Practical applicability (standard contracts, real-world patterns)
• Developer experience (tooling, automation)
• Trust minimization (formal compilation verification)

2. Automated Implementation Strategy

As automated code generation capabilities improve:

• Should the framework support multiple implementations per specification?
• What validation is required for automatically generated code?
• How should the framework handle optimization vs. verifiability tradeoffs?

3. Community Contribution

What would facilitate external contributions:

• Additional documentation
• Example contracts and proof patterns
• Contribution guidelines
• Mentorship or collaboration opportunities

4. Production Readiness

Define concrete criteria for production readiness:

• All sorry statements eliminated
• Standard contracts (ERC20, ERC721) verified
• Compiler dependency verified or eliminated
• Real-world deployment and audit

Technical Vision

The separation of specification from implementation enables:

Traditional development:
  Implementation → Review → Test → Deploy

Verified development:
  Specification (human-auditable, ~10 lines) →
    Implementation (optimized, ~1000 lines) →
      Proof (mechanized verification) →
        Deploy (guaranteed correctness)

Multiple implementations of a single specification:

One specification → Multiple implementations
- Implementation A: simple (easy to verify)
- Implementation B: gas-optimized
- Implementation C: storage-optimized

All proven correct. Selection based on requirements.

Questions

1. Which technical challenges should be addressed first?
2. What prevents adoption for production use?
3. Which example contracts would provide the most value?
4. How can formal verification be made more accessible?

Related Work

• Issue 81: Strategic roadmap tracker
• Issue 87: Codebase audit findings
• Discussion 127: Verity rename proposal
• Discussion 126: Verified contract explorer

---

Input from the community will help guide development priorities.