smom-dbis-138/docs/bridge/trustless/FORMAL_VERIFICATION.md

# Formal Verification - Trustless Bridge

## Overview

This document describes the formal verification approach for the trustless bridge system using Certora Prover. Formal verification provides mathematical proofs that the contracts satisfy critical security properties.

## Verification Tool

**Tool**: Certora Prover  
**License**: Commercial (requires Certora license)  
**Configuration**: `verification/certora/certora.conf`

## Verified Contracts

### 1. BondManager

**Specification**: `verification/certora/specs/BondManager.spec`

**Properties Verified**:
- **Bond Calculation**: Bond amount always >= max(depositAmount * multiplier / 10000, minBond)
- **State Exclusivity**: Bond cannot be both slashed and released
- **Slashing Split**: Slashing correctly splits 50% to challenger, 50% burned
- **Total Bonds Tracking**: `totalBonds[relayer]` correctly updated on all operations
- **No Duplicate Bonds**: Cannot post bond twice for same depositId
- **Reentrancy Protection**: All state-changing functions protected

**Critical Invariants**:
```solidity
invariant bondStateExclusive(uint256 depositId)
    bonds[depositId].slashed == false || bonds[depositId].released == false;
```

### 2. ChallengeManager

**Specification**: `verification/certora/specs/ChallengeManager.spec`

**Properties Verified**:
- **Challenge Window**: Cannot finalize before window expires
- **Challenge Timing**: Cannot challenge after window expires
- **Finalization Rules**: Cannot finalize challenged or already-finalized claims
- **Fraud Proof Verification**: Only valid proofs accepted
- **State Exclusivity**: Claim cannot be both finalized and challenged
- **Reentrancy Protection**: All functions protected

**Critical Invariants**:
```solidity
invariant claimStateExclusive(uint256 depositId)
    claims[depositId].finalized == false || claims[depositId].challenged == false;
```

### 3. InboxETH

**Specification**: `verification/certora/specs/InboxETH.spec`

**Properties Verified**:
- **Rate Limiting**: Cooldown period enforced (60 seconds)
- **Rate Limiting**: Hourly limit enforced (100 claims/hour)
- **Minimum Deposit**: Minimum deposit amount enforced (0.001 ETH)
- **Relayer Fee Calculation**: Fee = (amount * relayerFeeBps) / 10000
- **No Duplicate Claims**: Cannot submit duplicate claims for same depositId
- **Fee Claiming**: Fee can only be claimed after finalization, by relayer, once
- **Reentrancy Protection**: All functions protected

### 4. LiquidityPoolETH

**Specification**: `verification/certora/specs/LiquidityPoolETH.spec`

**Properties Verified**:
- **Minimum Ratio Enforcement**: Withdrawals blocked if below minimum ratio
- **Fee Calculation**: LP fee calculated correctly
- **Liquidity Tracking**: `totalLiquidity` correctly updated
- **Pending Claims Tracking**: `pendingClaims` correctly managed
- **Access Control**: Only authorized addresses can release funds
- **Reentrancy Protection**: All functions protected

**Critical Invariants**:
```solidity
invariant liquidityRatioMaintained(AssetType assetType)
    pools[assetType].totalLiquidity >= (pools[assetType].pendingClaims * minLiquidityRatioBps) / 10000;
```

### 5. Lockbox138

**Specification**: `verification/certora/specs/Lockbox138.spec`

**Properties Verified**:
- **Deposit ID Uniqueness**: Each depositId is unique
- **Replay Protection**: Nonce prevents duplicate deposits
- **Processed Deposits**: `processedDeposits[depositId]` correctly tracked
- **Nonce Increment**: Nonces increment correctly per depositor
- **Input Validation**: Zero amounts and recipients rejected
- **Reentrancy Protection**: All functions protected

**Critical Invariants**:
```solidity
invariant depositIdUniqueness(uint256 depositId)
    processedDeposits[depositId] == true || processedDeposits[depositId] == false;
```

## Running Verification

### Prerequisites

1. **Certora License**: Obtain license from Certora
2. **Certora Installation**: Install Certora Prover
3. **Dependencies**: Ensure all contract dependencies are available

### Run All Verifications

```bash
bash scripts/bridge/trustless/verify-contracts.sh
```

### Run Individual Contract Verification

```bash
certoraRun contracts/bridge/trustless/BondManager.sol \
  --verify BondManager:verification/certora/specs/BondManager.spec \
  --solc solc-0.8.19 \
  --optimistic_loop \
  --loop_iter 3 \
  --smt_timeout 600
```

### Using Configuration File

```bash
certoraRun verification/certora/certora.conf
```

## Interpreting Results

### Verification Passed ✅

- All specified properties hold
- No counterexamples found
- Contracts satisfy all invariants

### Verification Failed ❌

- Counterexample found
- Property violation detected
- Review counterexample to understand issue

### Verification Timeout ⏱️

- Prover could not complete in time
- May need to adjust timeout or simplify specification
- Consider breaking into smaller properties

## Critical Properties

### Economic Security

1. **Bond Sizing**: Bond always >= 110% of deposit (or minimum)
2. **Slashing Correctness**: Slashing splits 50/50 correctly
3. **Economic Invariant**: Fraud is always unprofitable

### State Invariants

1. **No Double Processing**: Each depositId processed once
2. **Challenge Window**: Finalization only after window expires
3. **Bond State**: Bond cannot be both slashed and released

### Access Control

1. **Authorization**: Only authorized addresses can call admin functions
2. **Permissionless**: Public functions accessible to all

### Reentrancy Protection

1. **No Reentrancy**: All state-changing functions protected
2. **External Calls**: Safe external call patterns

## Integration with CI/CD

### GitHub Actions Example

```yaml
name: Formal Verification

on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2
      - name: Run Formal Verification
        run: |
          bash scripts/bridge/trustless/verify-contracts.sh
```

### Pre-commit Hook

Add to `.git/hooks/pre-commit`:

```bash
#!/bin/bash
# Run formal verification before commit
bash scripts/bridge/trustless/verify-contracts.sh
```

## Specification Files

All specification files are located in `verification/certora/specs/`:

- `BondManager.spec` - Bond management properties
- `ChallengeManager.spec` - Challenge and finalization properties
- `InboxETH.spec` - Rate limiting and fee properties
- `LiquidityPoolETH.spec` - Liquidity and ratio properties
- `Lockbox138.spec` - Deposit uniqueness and replay protection

## Updating Specifications

When updating contracts:

1. Review affected specifications
2. Update properties if contract logic changes
3. Re-run verification
4. Update documentation if properties change

## Limitations

- **Certora License Required**: Commercial tool requiring license
- **Specification Complexity**: Complex properties may timeout
- **Loop Handling**: Requires careful handling of loops
- **External Calls**: May require additional modeling

## Alternative Tools

If Certora is not available, consider:

- **K Framework**: Open-source formal verification
- **Dafny**: Microsoft's verification-aware language
- **Why3**: Multi-prover verification platform

## Resources

- [Certora Documentation](https://docs.certora.com/)
- [Certora Prover Guide](https://docs.certora.com/en/latest/docs/prover/intro.html)
- [Specification Language Reference](https://docs.certora.com/en/latest/docs/cvl/index.html)

## Status

**Current Status**: ✅ Specifications created and ready for verification

**Next Steps**:
1. Obtain Certora license
2. Run initial verification
3. Address any property violations
4. Integrate into CI/CD pipeline