Step-by-Step Stablecoin Formal Verification: Certora Prover Implementation

# Directory structure I use for all stablecoin verifications
stablecoin-verification/
├── contracts/
│   ├── Stablecoin.sol
│   ├── StablecoinProxy.sol
│   └── interfaces/
├── specs/
│   ├── Stablecoin.spec
│   ├── StablecoinProxy.spec
│   └── helpers/
├── scripts/
│   ├── run_verification.sh
│   └── parse_results.py
└── certora.conf

// certora.conf
{
  "files": [
    "contracts/Stablecoin.sol",
    "contracts/StablecoinProxy.sol"
  ],
  "verify": "Stablecoin:specs/Stablecoin.spec",
  "solc": "solc8.19",
  "optimistic_loop": true,
  "loop_iter": 3,
  "optimistic_hashing": true,
  "smt_timeout": 600,
  "staging": true,
  "msg": "Stablecoin verification run",
  "rule_sanity": "basic",
  "packages": [
    "@openzeppelin/contracts=lib/openzeppelin-contracts"
  ]
}

// specs/Stablecoin.spec
methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function mint(address, uint256) external;
    function burn(address, uint256) external;
    function transfer(address, uint256) external returns (bool);
    function transferFrom(address, address, uint256) external returns (bool);
}

// Critical invariant: total supply equals sum of all balances
invariant totalSupplyEqualsBalances()
    totalSupply() == sumOfBalances()
    filtered { f -> !f.isView }

// Define sumOfBalances as a ghost function
ghost sumOfBalances() returns uint256 {
    init_state axiom sumOfBalances() == 0;
}

// Hook to maintain sumOfBalances accuracy
hook Sload uint256 balance balanceOf[KEY address user] STORAGE {
    // This hook is called whenever a balance is read
    // We use it to track balance changes
}

hook Sstore balanceOf[KEY address user] uint256 new_balance 
    (uint256 old_balance) STORAGE {
    // Update sumOfBalances when any balance changes
    havoc sumOfBalances assuming 
        sumOfBalances() == sumOfBalances()@prev() + new_balance - old_balance;
}

// Verify mint increases both balance and total supply correctly
rule mintIncreasesSupplyAndBalance(address to, uint256 amount) {
    env e;
    
    // Preconditions
    require to != 0;
    require amount > 0;
    require amount <= max_uint256 - totalSupply();
    require amount <= max_uint256 - balanceOf(to);
    
    // Store initial values
    uint256 totalSupplyBefore = totalSupply();
    uint256 balanceBefore = balanceOf(to);
    
    // Execute mint
    mint(e, to, amount);
    
    // Postconditions
    assert totalSupply() == totalSupplyBefore + amount;
    assert balanceOf(to) == balanceBefore + amount;
    
    // Verify other balances unchanged
    address other;
    require other != to;
    assert balanceOf(other) == balanceOf(other)@old;
}

// Verify burn decreases both balance and total supply correctly
rule burnDecreasesSupplyAndBalance(address from, uint256 amount) {
    env e;
    
    // Preconditions
    require from != 0;
    require amount > 0;
    require balanceOf(from) >= amount;
    require totalSupply() >= amount;
    
    // Store initial values
    uint256 totalSupplyBefore = totalSupply();
    uint256 balanceBefore = balanceOf(from);
    
    // Execute burn
    burn(e, from, amount);
    
    // Postconditions
    assert totalSupply() == totalSupplyBefore - amount;
    assert balanceOf(from) == balanceBefore - amount;
}

// Verify transfers maintain total supply invariant
rule transferPreservesTotalSupply(address from, address to, uint256 amount) {
    env e;
    
    uint256 totalSupplyBefore = totalSupply();
    
    // Execute transfer
    transfer(e, to, amount);
    
    // Total supply should remain unchanged
    assert totalSupply() == totalSupplyBefore;
}

// Verify transfer updates balances correctly
rule transferUpdatesBalancesCorrectly(address from, address to, uint256 amount) {
    env e;
    require e.msg.sender == from;
    require from != to;
    require from != 0 && to != 0;
    require balanceOf(from) >= amount;
    
    uint256 fromBalanceBefore = balanceOf(from);
    uint256 toBalanceBefore = balanceOf(to);
    
    // Execute transfer
    bool success = transfer(e, to, amount);
    
    // If transfer succeeded, balances should update correctly
    if (success) {
        assert balanceOf(from) == fromBalanceBefore - amount;
        assert balanceOf(to) == toBalanceBefore + amount;
    }
}

// Verify transferFrom respects allowances
rule transferFromRespectsAllowance(address owner, address spender, address to, uint256 amount) {
    env e;
    require e.msg.sender == spender;
    require owner != spender;
    require owner != 0 && spender != 0 && to != 0;
    
    uint256 allowanceBefore = allowance(owner, spender);
    require allowanceBefore >= amount;
    require balanceOf(owner) >= amount;
    
    // Execute transferFrom
    bool success = transferFrom(e, owner, to, amount);
    
    // If successful, allowance should decrease (unless infinite approval)
    if (success && allowanceBefore != max_uint256) {
        assert allowance(owner, spender) == allowanceBefore - amount;
    }
}

// Verify only minters can mint tokens
rule onlyMinterCanMint(address caller, address to, uint256 amount) {
    env e;
    require e.msg.sender == caller;
    
    // Try to mint
    mint(e, to, amount);
    
    // This should either succeed (if caller is minter) or revert
    // We verify this by checking the minter role
    assert hasRole(MINTER_ROLE(), caller);
}

// Verify role-based access control invariants
invariant minterRoleConsistency(address account)
    hasRole(MINTER_ROLE(), account) => canMint(account)

// Verify admin controls are properly restricted
rule onlyAdminCanGrantRoles(address admin, address account, bytes32 role) {
    env e;
    require e.msg.sender == admin;
    
    // Attempt to grant role
    grantRole(e, role, account);
    
    // Should only succeed if admin has the admin role for this role
    assert hasRole(getRoleAdmin(role), admin);
}

// Verify arithmetic operations never overflow
rule noArithmeticOverflow() {
    method f;
    env e;
    calldataarg args;
    
    // Store initial state
    mathint totalSupplyBefore = totalSupply();
    address user1; address user2;
    mathint balance1Before = balanceOf(user1);
    mathint balance2Before = balanceOf(user2);
    
    // Execute any function
    f(e, args);
    
    // Verify no overflows occurred
    assert totalSupply() <= max_uint256;
    assert balanceOf(user1) <= max_uint256;
    assert balanceOf(user2) <= max_uint256;
    
    // Verify reasonable bounds
    assert totalSupply() >= 0;
    assert balanceOf(user1) >= 0;
    assert balanceOf(user2) >= 0;
}

// Verify safe math operations
rule safeMathOperations(uint256 a, uint256 b) {
    // Test addition
    uint256 sum = safeAdd(a, b);
    assert a <= sum && b <= sum; // No overflow
    assert sum - a == b && sum - b == a; // Correct result
    
    // Test subtraction (when valid)
    if (a >= b) {
        uint256 diff = safeSub(a, b);
        assert diff <= a; // No underflow
        assert diff + b == a; // Correct result
    }
    
    // Test multiplication
    if (a > 0 && b > 0) {
        uint256 product = safeMul(a, b);
        assert product / a == b; // No overflow
        assert product / b == a; // Correct result
    }
}

// specs/StablecoinProxy.spec
using Stablecoin as implementation;

methods {
    function implementation() external returns (address) envfree;
    function admin() external returns (address) envfree;
    function upgrade(address) external;
    function changeAdmin(address) external;
}

// Verify proxy invariants
invariant proxyInvariant()
    implementation() != 0 && admin() != 0

// Verify only admin can upgrade
rule onlyAdminCanUpgrade(address caller, address newImpl) {
    env e;
    require e.msg.sender == caller;
    
    address adminBefore = admin();
    
    // Attempt upgrade
    upgrade@withrevert(e, newImpl);
    
    // Should only succeed if caller is admin
    bool reverted = lastReverted;
    assert !reverted => caller == adminBefore;
}

// Verify upgrade preserves critical state
rule upgradePreservesState(address newImpl) {
    env e;
    require e.msg.sender == admin();
    
    // Store critical state before upgrade
    uint256 totalSupplyBefore = implementation.totalSupply();
    address user;
    uint256 balanceBefore = implementation.balanceOf(user);
    
    // Perform upgrade
    upgrade(e, newImpl);
    
    // Critical state should be preserved
    // Note: This assumes the new implementation has the same interface
    assert implementation.totalSupply() == totalSupplyBefore;
    assert implementation.balanceOf(user) == balanceBefore;
}

// Vulnerable code in interest calculation
function calculateInterest(uint256 principal, uint256 rate, uint256 time) 
    public pure returns (uint256) {
    return (principal * rate * time) / (365 * 24 * 3600 * 10000);
}

// Certora spec that caught this bug
rule interestCalculationSafety(uint256 principal, uint256 rate, uint256 time) {
    require principal > 0 && rate > 0 && time > 0;
    require principal <= 1000000 * 10^18; // 1M tokens max
    require rate <= 10000; // 100% annual rate max
    require time <= 365 * 24 * 3600; // 1 year max
    
    uint256 interest = calculateInterest(principal, rate, time);
    
    // This would fail when (principal * rate * time) overflows
    assert interest <= principal; // Interest shouldn't exceed principal for reasonable rates
}

// Verification rule that caught reentrancy vulnerability
rule noReentrancyInTransfer(address to, uint256 amount) {
    env e;
    
    // Assume receiver might call back into contract
    require isContract(to);
    
    uint256 senderBalanceBefore = balanceOf(e.msg.sender);
    uint256 receiverBalanceBefore = balanceOf(to);
    uint256 totalSupplyBefore = totalSupply();
    
    transfer(e, to, amount);
    
    // Verify state consistency despite potential reentrancy
    assert balanceOf(e.msg.sender) == senderBalanceBefore - amount;
    assert balanceOf(to) == receiverBalanceBefore + amount;
    assert totalSupply() == totalSupplyBefore;
}

// Rule that identified approve front-running vulnerability
rule approveRaceCondition(address owner, address spender, uint256 newAmount) {
    env e1; env e2;
    require e1.msg.sender == owner;
    require e2.msg.sender == spender;
    require e1.block.number == e2.block.number; // Same block
    
    uint256 currentAllowance = allowance(owner, spender);
    require currentAllowance > 0;
    require newAmount != currentAllowance;
    
    // Owner tries to change approval
    approve(e1, spender, newAmount);
    
    // Spender tries to spend old allowance
    transferFrom(e2, owner, spender, currentAllowance);
    
    // This rule helped identify the front-running vulnerability
    // where spender could spend both old and new allowances
}

#!/bin/bash
# scripts/run_verification.sh

set -e

echo "Starting stablecoin formal verification..."

# Clean previous results
rm -rf .certora_build/ certora_out/

# Run base contract verification
echo "Verifying core stablecoin contract..."
certoraRun certora.conf \
    --rule_sanity basic \
    --optimistic_loop \
    --loop_iter 3 \
    --msg "Core stablecoin verification - $(date)"

# Run proxy verification if present
if [ -f "contracts/StablecoinProxy.sol" ]; then
    echo "Verifying proxy contract..."
    certoraRun certora_proxy.conf \
        --msg "Proxy verification - $(date)"
fi

# Run upgrade verification
if [ -f "specs/UpgradeSafety.spec" ]; then
    echo "Verifying upgrade safety..."
    certoraRun certora_upgrade.conf \
        --msg "Upgrade safety verification - $(date)"
fi

# Parse and report results
python3 scripts/parse_results.py

echo "Verification complete!"

#!/usr/bin/env python3
# scripts/parse_results.py

import json
import os
import sys
from datetime import datetime

def parse_certora_results():
    """Parse Certora verification results and generate report"""
    
    results_dir = "certora_out"
    if not os.path.exists(results_dir):
        print("No verification results found")
        return False
    
    # Find latest results file
    result_files = [f for f in os.listdir(results_dir) if f.endswith('.json')]
    if not result_files:
        print("No JSON results found")
        return False
    
    latest_file = max(result_files, key=lambda x: os.path.getctime(os.path.join(results_dir, x)))
    
    with open(os.path.join(results_dir, latest_file), 'r') as f:
        results = json.load(f)
    
    # Generate report
    report = {
        'timestamp': datetime.now().isoformat(),
        'total_rules': 0,
        'passed_rules': 0,
        'failed_rules': 0,
        'timeout_rules': 0,
        'critical_failures': [],
        'warnings': []
    }
    
    for rule_name, rule_result in results.get('rules', {}).items():
        report['total_rules'] += 1
        
        if rule_result['status'] == 'PASS':
            report['passed_rules'] += 1
        elif rule_result['status'] == 'FAIL':
            report['failed_rules'] += 1
            
            # Check if this is a critical failure
            if is_critical_rule(rule_name):
                report['critical_failures'].append({
                    'rule': rule_name,
                    'counterexample': rule_result.get('counterexample', 'No counterexample')
                })
        elif rule_result['status'] == 'TIMEOUT':
            report['timeout_rules'] += 1
            report['warnings'].append(f"Rule {rule_name} timed out - consider simplifying")
    
    # Print report
    print(f"\n{'='*50}")
    print(f"STABLECOIN VERIFICATION REPORT")
    print(f"{'='*50}")
    print(f"Timestamp: {report['timestamp']}")
    print(f"Total Rules: {report['total_rules']}")
    print(f"Passed: {report['passed_rules']}")
    print(f"Failed: {report['failed_rules']}")
    print(f"Timeouts: {report['timeout_rules']}")
    
    if report['critical_failures']:
        print(f"\n🚨 CRITICAL FAILURES ({len(report['critical_failures'])}):")
        for failure in report['critical_failures']:
            print(f"  - {failure['rule']}")
            print(f"    Counterexample: {failure['counterexample'][:100]}...")
    
    if report['warnings']:
        print(f"\n⚠️  WARNINGS ({len(report['warnings'])}):")
        for warning in report['warnings']:
            print(f"  - {warning}")
    
    # Determine if verification passed
    success = report['failed_rules'] == 0 and len(report['critical_failures']) == 0
    
    if success:
        print(f"\n✅ VERIFICATION PASSED")
    else:
        print(f"\n❌ VERIFICATION FAILED")
        sys.exit(1)
    
    return success

def is_critical_rule(rule_name):
    """Determine if a rule failure is critical"""
    critical_patterns = [
        'totalSupply',
        'balance',
        'mint',
        'burn',
        'overflow',
        'underflow',
        'onlyAdmin',
        'onlyMinter',
        'reentrancy'
    ]
    
    return any(pattern.lower() in rule_name.lower() for pattern in critical_patterns)

if __name__ == "__main__":
    parse_certora_results()

// Track historical maximum supply
ghost maxSupplyEver() returns uint256 {
    init_state axiom maxSupplyEver() == 0;
}

hook Sstore totalSupply uint256 new_supply (uint256 old_supply) {
    havoc maxSupplyEver assuming maxSupplyEver() >= old_supply && 
                                 maxSupplyEver() >= new_supply &&
                                 (maxSupplyEver() == old_supply || maxSupplyEver() == new_supply);
}

// Verify supply never exceeds configured maximum
rule supplyCap() {
    assert totalSupply() <= MAX_SUPPLY();
    assert maxSupplyEver() <= MAX_SUPPLY();
}

// Track pause state changes
ghost wasPausedEver() returns bool {
    init_state axiom wasPausedEver() == false;
}

hook Sstore paused bool new_paused (bool old_paused) {
    havoc wasPausedEver assuming wasPausedEver()@prev() || new_paused;
}

// Verify pause functionality
rule pauseStopsTransfers(address from, address to, uint256 amount) {
    require paused();
    
    transfer@withrevert(e, to, amount);
    
    // Transfer should revert when paused
    assert lastReverted;
}

// specs/StablecoinEcosystem.spec
using Stablecoin as stablecoin;
using StablecoinController as controller;
using PriceOracle as oracle;

methods {
    // Stablecoin methods
    function stablecoin.totalSupply() external returns (uint256) envfree;
    function stablecoin.mint(address, uint256) external;
    
    // Controller methods
    function controller.mintingAllowed() external returns (bool) envfree;
    function controller.pause() external;
    
    // Oracle methods
    function oracle.getPrice() external returns (uint256) envfree;
}

// Verify ecosystem-wide invariants
invariant ecosystemConsistency()
    controller.mintingAllowed() => !stablecoin.paused()

// Verify cross-contract interactions
rule controllerCanPauseStablecoin() {
    env e;
    
    require !stablecoin.paused();
    
    controller.pause(e);
    
    assert stablecoin.paused();
}

// Verify oracle-dependent operations
rule mintingRequiresValidPrice(address to, uint256 amount) {
    env e;
    
    uint256 price = oracle.getPrice();
    require price > 0; // Valid price required
    
    stablecoin.mint(e, to, amount);
    
    // Should succeed with valid price
    assert !lastReverted;
}

// Instead of one complex rule, split into focused rules
rule transferBasicCorrectness(address to, uint256 amount) {
    env e;
    require amount <= balanceOf(e.msg.sender);
    require to != 0;
    
    uint256 senderBefore = balanceOf(e.msg.sender);
    uint256 receiverBefore = balanceOf(to);
    
    transfer(e, to, amount);
    
    assert balanceOf(e.msg.sender) == senderBefore - amount;
    assert balanceOf(to) == receiverBefore + amount;
}

rule transferPreservesSupply(address to, uint256 amount) {
    env e;
    
    uint256 supplyBefore = totalSupply();
    
    transfer(e, to, amount);
    
    assert totalSupply() == supplyBefore;
}

rule transferRevertsOnInsufficientBalance(address to, uint256 amount) {
    env e;
    require amount > balanceOf(e.msg.sender);
    
    transfer@withrevert(e, to, amount);
    
    assert lastReverted;
}

// Group related invariants
invariant balanceConsistency(address user)
    balanceOf(user) <= totalSupply() &&
    balanceOf(user) >= 0
    filtered { f -> !f.isView }

invariant systemIntegrity()
    totalSupply() >= 0 &&
    totalSupply() <= MAX_SUPPLY()
    filtered { f -> !f.isView }

// Use preserved blocks for expensive checks
rule expensivePropertyCheck(method f) {
    env e; calldataarg args;
    
    bool propertyBefore = expensivePropertyHolds();
    
    f(e, args);
    
    bool propertyAfter = expensivePropertyHolds();
    
    // Only check expensive property if it held before
    assert propertyBefore => propertyAfter;
}

#!/bin/bash
# scripts/pre_deploy_verification.sh

echo "Pre-deployment verification checklist..."

# 1. Run full verification suite
./scripts/run_verification.sh || exit 1

# 2. Check for critical property violations
python3 scripts/check_critical_properties.py || exit 1

# 3. Verify upgrade compatibility (if applicable)
if [ "$UPGRADE_MODE" = "true" ]; then
    ./scripts/verify_upgrade_safety.sh || exit 1
fi

# 4. Generate verification report
python3 scripts/generate_audit_report.py

echo "✅ All verifications passed - ready for deployment"

# scripts/generate_audit_report.py
def generate_audit_report():
    """Generate comprehensive verification audit report"""
    
    report = {
        'contract_info': get_contract_info(),
        'verification_results': parse_verification_results(),
        'properties_verified': get_verified_properties(),
        'bug_classes_covered': get_coverage_analysis(),
        'recommendations': get_recommendations()
    }
    
    # Generate HTML report
    html_report = f"""
    <html>
    <head><title>Stablecoin Formal Verification Report</title></head>
    <body>
        <h1>Formal Verification Report</h1>
        <h2>Contract: {report['contract_info']['name']}</h2>
        <p>Version: {report['contract_info']['version']}</p>
        <p>Verification Date: {datetime.now().strftime('%Y-%m-%d %H:%M:%S')}</p>
        
        <h2>Verification Summary</h2>
        <ul>
            <li>Total Properties: {report['verification_results']['total']}</li>
            <li>Verified: {report['verification_results']['passed']}</li>
            <li>Failed: {report['verification_results']['failed']}</li>
        </ul>
        
        <h2>Properties Verified</h2>
        <ul>
        {''.join(f'<li>{prop}</li>' for prop in report['properties_verified'])}
        </ul>
        
        <h2>Security Coverage</h2>
        <ul>
        {''.join(f'<li>{bug_class}</li>' for bug_class in report['bug_classes_covered'])}
        </ul>
    </body>
    </html>
    """
    
    with open('verification_report.html', 'w') as f:
        f.write(html_report)
    
    print("Audit report generated: verification_report.html")