Verified Contract Explorer

[Th0rgal]

Verified Contract Explorer

Motivation

As formally verified smart contracts become more prevalent, there is a need for infrastructure to discover, understand, and verify the guarantees they provide. This proposal outlines a system for exploring verified contracts and their proofs.

Core Concept

A web-based interface for examining verified smart contracts:

Domain: verified-contracts.org/ethereum/0xA0b86...

Displays:
- Contract specification (Lean formalization)
- Proven properties (theorems with proofs)
- Interactive property verification
- Implementation details

Technical Requirements

1. Contract Registry

Maintain a database of verified contracts with:

• Formal specifications
• Proven theorems
• Proof artifacts
• Contract metadata

2. Property Verification Interface

Enable queries about contract behavior:

• "Is owner able to drain user funds?" → Provably no (theorem reference)
• "What occurs when amount = 0?" → Contract reverts (proven behavior)
• "Does reentrancy exist?" → Provably no (theorem reference)

3. Property-Based Search

Query contracts by proven guarantees:

• All exchange contracts with proven fund safety
• All token contracts with proven arithmetic safety
• Contracts satisfying specific invariants

4. Integration Points

• API for wallet software (verification status before transactions)
• Integration with existing block explorers
• Machine-readable proof artifacts

Formal Model

Current state:

Implementation → Testing → Deployment → Hope for correctness

Proposed state:

Specification (human-auditable) → 
  Implementation (potentially automated) → 
    Proof (machine-verified) → 
      Public verification (this system)

Discussion Points

1. Which features constitute a minimal viable system?
2. How should proof explanations be presented to non-experts?
3. Should the system support multiple verification frameworks beyond Lean?
4. What formal guarantees must the system itself provide?

Related Work

This complements the potential rebrand discussion (Issue 121) by providing the discovery and verification layer for formally verified contracts.