Minimal Formal Verification System for Ethereum

A lightweight, educational formal verification system that demonstrates mathematical proof generation for Ethereum smart contract safety properties using Z3 SMT solver.

What This Is

This is a minimal implementation of the core concepts behind formal verification systems like those used in:

• Solidity's built-in SMTChecker
• Dafny verification language
• CBMC bounded model checker
• Certora verification platform

Key Insight: All formal verification systems fundamentally do the same thing - convert program logic into mathematical constraints and use SMT solvers to prove or disprove properties.

What It Demonstrates

Mathematical Proofs

• Overflow Detection: Proves when a + b exceeds uint256 bounds
• Underflow Detection: Proves when a - b would be negative
• Multiplication Safety: Proves when a * b stays within bounds

Real Formal Verification

• SMT-LIB2 Integration: Direct communication with Z3 theorem prover
• Mathematical Guarantees: Results are proofs, not heuristics
• Ethereum-Specific: Native uint256 support with correct bounds

Quick Start

Prerequisites

# macOS
brew install z3 ghc

# Ubuntu/Debian  
sudo apt-get install z3 ghc

# Verify installation
z3 --version
ghc --version

Run

# Clone or extract the project
cd minimal-verify

# Run the verification system
runhaskell MinimalVerify.hs

Expected Output

Minimal Formal Verification System for Ethereum uint256
==========================================================

Safe addition:
PROVEN: 100 + 200 = 300 (no overflow)

Overflow addition:
OVERFLOW: 115792089237316195423570985008687907853269984665640564039457584007913129639935 + 1 would exceed uint256_max

Safe subtraction:
PROVEN: 200 - 100 = 100 (no underflow)

Underflow subtraction:
UNDERFLOW: 100 - 200 would be negative

Safe multiplication:
PROVEN: 100 * 200 = 20000 (no overflow)

Overflow multiplication:
OVERFLOW: 340282366920938463463374607431768211456 * 340282366920938463463374607431768211456 would exceed uint256_max

Architecture

Core Components

-- SMT Solver Interface
data SMTSolver = SMTSolver ProcessHandle Handle Handle

-- Ethereum Types
newtype UInt256 = UInt256 Integer

-- Verification Results  
data VerifyResult = Verified Text | CounterExample Text | VerifyError Text

Verification Process

1. Model the Problem: Convert arithmetic operation to SMT constraints
2. Generate Constraints: Create SMT-LIB2 assertions about bounds and operations
3. Query Solver: Ask Z3 if overflow/underflow is possible
4. Interpret Results:
   • unsat = PROVEN safe (no counterexample exists)
   • sat = Unsafe (counterexample found)

SMT-LIB2 Example

(set-logic QF_NIA)                    ; Nonlinear Integer Arithmetic
(declare-const a Int)                 ; Declare variables
(declare-const b Int)
(declare-const result Int)
(assert (= a 100))                    ; Set specific values
(assert (= b 200))
(assert (= result (+ a b)))           ; Define operation
(assert (> result 115792089...))      ; Check if exceeds uint256_max
(check-sat)                           ; Query: is overflow possible?

Code Structure

Key Functions

initSolver :: IO (Either Text SMTSolver)
-- Initialize Z3 process with SMT-LIB2 interface

verifyAdditionNoOverflow :: SMTSolver -> UInt256 -> UInt256 -> IO VerifyResult  
-- Prove addition safety using mathematical constraints

sendCommand :: SMTSolver -> Text -> IO ()
-- Send SMT-LIB2 commands to Z3 solver

getResponse :: SMTSolver -> IO Text
-- Receive and parse Z3 responses

Educational Value

Learn Formal Verification Concepts

• SMT Solvers: How theorem provers work
• Constraint Generation: Converting programs to logic
• Satisfiability: Understanding SAT/UNSAT results
• Bounded Verification: Working within type constraints

Understand Real Tools

This minimal system demonstrates the same core concepts used in:

• Solidity SMTChecker: Built into the Solidity compiler
• Dafny: Microsoft's verification-aware programming language
• CBMC: Bounded model checker for C/C++
• SMACK: LLVM bitcode verifier

Technical Details

SMT Logic Used

• QF_NIA: Quantifier-Free Nonlinear Integer Arithmetic
• Supports: +, -, *, <, >, =, and, or, not
• No division (would require real arithmetic)

Verification Approach

• Bounded Model Checking: Verify within uint256 bounds
• Concrete Values: Check specific arithmetic operations
• Proof by Contradiction: Assert unsafe condition, check if satisfiable

Context Management

sendCommand solver "(push)"    -- Save solver state
-- ... add constraints and check ...
sendCommand solver "(pop)"     -- Restore solver state

Limitations

Current Scope

• ✅ Arithmetic overflow/underflow: Addition, subtraction, multiplication
• ❌ Division by zero: Not implemented (easy to add)
• ❌ Complex contracts: Only basic arithmetic operations
• ❌ Loops: No loop invariant generation
• ❌ Function calls: No inter-procedural analysis

Design Choices

• Educational over Performance: Clarity prioritized over optimization
• Concrete over Symbolic: Specific values rather than symbolic execution
• Simple over Complete: Core concepts without full language support

Comparison with Other Tools

Tool	Approach	Guarantees	Scope
This System	SMT-based proofs	Mathematical certainty	Arithmetic operations
Slither	Static analysis	Heuristic warnings	Full Solidity language
Mythril	Symbolic execution	Path-based analysis	EVM bytecode
Solidity SMTChecker	SMT-based proofs	Mathematical certainty	Full Solidity language
Certora	SMT-based proofs	Mathematical certainty	Production contracts

When to Use This

Learning Formal Verification

• Understand how SMT solvers work
• Learn constraint generation techniques
• Explore verification result interpretation

Prototyping Verification Ideas

• Test new verification approaches
• Experiment with different SMT logics
• Validate verification algorithms

Educational Demonstrations

• Teaching formal methods concepts
• Showing mathematical proof generation
• Explaining SMT solver integration

Development Setup

WebStorm Integration

1. Run Configuration:

   • Script: /path/to/runhaskell
   • Arguments: MinimalVerify.hs
   • Working Directory: minimal-verify/

2. File Association:

   • Associate .hs files with Haskell syntax highlighting

Command Line

# Compile (optional)
ghc -o MinimalVerify MinimalVerify.hs

# Run compiled version
./MinimalVerify

# Or run directly
runhaskell MinimalVerify.hs

Further Reading

SMT Solvers

• Z3 Tutorial
• SMT-LIB Standard
• Satisfiability Modulo Theories

Formal Verification

• Software Foundations
• Concrete Semantics
• Program Verification

Ethereum Verification

• Solidity SMTChecker
• Certora Documentation
• Runtime Verification

Contributing

This is an educational project. Contributions that improve clarity, add educational value, or demonstrate new verification concepts are welcome.

Areas for Enhancement

• Additional arithmetic operations (division, modulo)
• Better error messages and explanations
• Interactive mode for custom inputs
• Visualization of SMT constraints

License

MIT License - Feel free to use for educational purposes, research, or as a foundation for more complex verification systems.

---

Remember: This is the core of formal verification. Everything else - parsing, user interfaces, reporting - is built around this fundamental capability to generate mathematical proofs about program properties.