Audit Methodology

This document describes the tools, techniques, and processes used in the Abba Baba V2 smart contract security audit. All 3 V2 contracts are deployed to Base Mainnet (March 1, 2026).

8-Layer Security Stack

We employ the most comprehensive smart contract verification methodology:

Phase 1: Static Analysis (Slither)

Tool: Slither v0.10.x

Slither detects common vulnerabilities, optimization opportunities, and best practice violations.

slither . --exclude-dependencies --filter-paths "test|mock|archive"

V2 Results: 0 High, 0 Medium, 23 Informational (lint-level)

Phase 2: Manual SWC Registry Review

The SWC Registry catalogs 37 known smart contract weaknesses. Each V2 contract was manually reviewed against all applicable categories.

Key Categories Checked:

Phase 3: Unit Testing (Hardhat — 95 Tests)

Traditional unit tests covering all V2 contract functionality.

Results: 95/95 passing (~45s)

Covers escrow lifecycle, fee calculations, score deltas, tier boundaries, dispute resolution, abandonment, admin operations, and access control.

Phase 4: Fuzz Testing

Foundry Fuzzing (16 Tests @ 10K Runs)

Uses Foundry’s built-in fuzzer for randomized input testing.

forge test --fuzz-runs 10000

Results: 16/16 passing, 160,000 total iterations, zero failures.

Medusa Parallel Fuzzing (138 Tests)

Medusa runs 8 workers simultaneously for fast parallel coverage of property-based invariants.

medusa fuzz --config medusa-v2.json

Results: 138/138 passing. Tests cover 2% fee invariant, balance conservation, status transitions, timing bounds, score tiers, and more.

Phase 5: Symbolic Execution (Halmos — 58/64 Proofs)

Halmos uses symbolic execution to mathematically verify properties over all possible inputs.

halmos --solver-timeout-assertion 120

Results: 58/64 proofs verified. 6 timeouts on nonlinear uint256 arithmetic (inherent SMT solver limitation). The same properties are verified by Certora and 160K+ fuzz iterations.

Timed-out proofs (all nonlinear arithmetic):

1. check_noOverflowOnFee (Score)
2. check_feeLessThanAmount (Escrow)
3. check_fullBuyerRefund (Escrow)
4. check_lockedIs98Percent (Escrow)
5. check_noOverflowOnFee (Escrow)
6. check_noOverflowOnSplit (Escrow)

Phase 6: Formal Verification (Certora — 19 Rules)

Mathematical proofs that critical properties hold for all possible inputs and states.

certoraRun certora/conf/AbbaBabaScore.conf
certoraRun certora/conf/AbbaBabaEscrow.conf
certoraRun certora/conf/AbbaBabaResolver.conf

Results: 19/19 rules verified across all 3 contracts. Re-verified on March 1, 2026.

Phase 7: Mutation Testing (Gambit — 441 Mutants)

Mutation testing introduces bugs into the code to verify tests catch them.

gambit mutate --filename contracts/AbbaBabaScore.sol
gambit mutate --filename contracts/AbbaBabaEscrow.sol
gambit mutate --filename contracts/AbbaBabaResolver.sol

V2 Results: 441 mutants generated

Phase 8: Differential Testing (13 Comparisons)

Spec contracts implement expected behavior in simplified Solidity. Real contracts are tested against specs to verify they produce identical results.

Results: 13 comparisons, 100% match. Fee calculations, tier boundaries, and score deltas all match spec.

Tools Used

Current Results Summary

V2 Test Suite (March 1, 2026)
═══════════════════════════════
Hardhat Unit Tests:       95/95 passing
Foundry Fuzz Tests:       16/16 @ 10K runs (160K iterations)
Medusa Parallel Fuzz:    138/138 passing
Halmos Symbolic Proofs:   58/64 (6 solver timeouts)
Certora Formal Rules:     19/19 verified
Gambit Mutants:          441 generated
Slither Static:           0 high/medium
Differential:            13/13 match

Total Combined Tests:    249
Total Fuzz Iterations:   82.6M+ (all-time)
Vulnerabilities Found:   0

Continuous Security

What We Achieve

1. 249 automated tests across 3 tools (Hardhat, Foundry, Medusa)
2. 58 symbolic proofs via Halmos
3. 19 formal verification rules via Certora
4. 441 mutation mutants generated via Gambit
5. Static analysis with Slither (0 High/Medium)
6. Daily audit reports published for full transparency

Known Limitations

What This Audit Covers:

• Smart contract logic and state machine correctness
• Access control and role enforcement
• Reentrancy protection
• Economic incentives (2% fee model)
• Upgrade safety (UUPS pattern)

What This Audit Does NOT Cover:

• Off-chain components (backend, UI)
• Key management practices
• Operational security
• Third-party dependencies (OpenZeppelin audited separately)
• Future contract upgrades

Code Review Checklist

Access Control

• All sensitive functions have role modifiers
• Role hierarchy properly configured (DEFAULT_ADMIN, ESCROW_ROLE, RESOLVER_ROLE)
• No public functions that should be restricted
• RELAYER_ROLE removed (v2.2.0) — seller-only delivery

Reentrancy

• CEI pattern followed (Checks-Effects-Interactions)
• SafeERC20 used for all token transfers
• No callback vulnerabilities

Upgrade Safety (UUPS)

• _disableInitializers() in constructor
• _authorizeUpgrade() restricted to admin
• Storage gaps (50 slots) for future variables

Economic Security

• 2% fee calculation verified (Certora + Halmos + fuzz)
• 11 tier boundaries verified (differential testing)
• Score deltas verified (+1, -3, -5)
• Funds cannot be locked permanently

Appendix: Raw Reports

Available in the repository:

contracts/
├── certora/conf/          # Certora configuration files
├── certora/specs/         # CVL 2 specification files
├── test/foundry/          # Foundry fuzz tests
├── test/halmos/           # Halmos symbolic tests
├── test/medusa/           # Medusa parallel fuzz tests
├── test/differential/     # Spec vs real comparison
├── medusa-v2.json         # Medusa configuration
├── echidna-v2.yaml        # Echidna configuration
└── gambit_conf.json       # Gambit mutation config