Testing & Verification

Last Updated: 2026-07-19

Our V2 smart contract testing strategy employs an 8-layer security stack to ensure security, correctness, and resilience against edge cases and attacks. All 3 V2 contracts are deployed to Base Mainnet and verified on BaseScan.

2026-07-19 Verification Session — sqrt Score v2.1.0 Candidate

The scoring model is being upgraded from flat (+1 winner / −3 dispute loss / −5 abandonment) to value-scaled sqrt scoring: every settled job earns isqrt(lockedAmount) points (diminishing returns — many real jobs beat a few big ones), dispute losers pay 3× the job’s points, abandonment costs 5×. This makes reputation farming with micro-jobs economically pointless.

Results:

sqrt v2.1.0 Candidate (July 19, 2026)
├── 95/95 Hardhat unit + integration tests — first green full run vs sqrt
├── 23/23 Foundry fuzz tests @ 10K runs (incl. differential ground-truth suite)
├── Differential spec rewritten as sqrt ground truth (amount-based deltas, raw-scale tiers)
├── Halmos proofs rewritten to quantify over arbitrary amounts (solver re-run pending)
├── Echidna/Medusa harnesses reconciled to the sqrt API (campaign re-run pending)
└── Ops preflight vs production: 11/11 (resolver role, queue, AI arbitrator)

Flags found & fixed this session (full detail in the internal session report):

• The test suite had been self-inconsistent since the sqrt change entered source — Escrow integration tests and all fuzz/formal harnesses still asserted the flat model. Reconciled.
• The fuzzer caught a live bug on its first execution: the tier fuzz test bounded scores on the displayed scale while the contract tiers on the raw scale. Fixed.
• Escrow NatSpec still described flat scoring. Fixed.

Before v2.1.0 deploys: score-scale storage migration (raw = displayed×1000 — existing scores must scale ×1000 in the upgrade or graduated agents would regress), Echidna/Medusa campaigns, Certora re-verification, Gambit mutation, Slither — then Sepolia bake before any mainnet upgrade.

Testing Overview

V2 Test Suite (March 1, 2026 — post staging red team)
├── 95 Hardhat Unit Tests (~45s)
├── 16 Foundry Fuzz Tests @ 10K runs (160K iterations)
├── 137 Medusa Parallel Fuzz Tests (8 workers)
├── 60/64 Halmos Symbolic Proofs (4 solver timeouts — 2 resolved post-CEI refactor)
├── 19 Certora Formal Verification Rules (all re-verified post-CEI)
├── 441 Gambit Mutation Mutants Generated
└── Slither Static Analysis (0 high/medium)

1. Unit Tests (Hardhat — 95 Tests)

Traditional unit tests covering expected behavior, edge cases, and full lifecycle for all V2 contracts.

Coverage Areas

Running Unit Tests

cd contracts
npx hardhat test
 
# With coverage
npx hardhat coverage

2. Fuzz Testing (Foundry — 16 Tests)

Foundry fuzz tests with 10,000 runs per test, covering fee calculations, tier boundaries, score deltas, and escrow lifecycle edge cases.

160,000 total fuzz iterations with zero failures.

Running Foundry Fuzz Tests

cd contracts
forge test --fuzz-runs 10000

3. Parallel Fuzz Testing (Medusa — 137 Tests)

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

Note: Count decreased from 138 to 137 on Mar 1 when MockERC20.burn() was removed (real USDC has no public burn; its presence was causing false-positive invariant failures with testAllContracts: true).

Key Invariants Tested

• Platform fee is exactly 2% (200 BPS)
• Locked amount is exactly 98%
• Treasury receives fee at creation
• Balance conservation across all escrows
• Valid status transitions (never backward)
• Dispute only from Delivered state
• Abandon only from Funded after deadline
• Seller receives exactly lockedAmount
• Score can go negative (no floor on trust score)
• Score 100+ = unlimited max job value
• Score 0 = $10 floor
• Tier values are monotonically increasing

Running Medusa

cd contracts
medusa fuzz --config medusa-v2.json

4. Symbolic Execution (Halmos — 60/64 Proofs)

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

4 timeout analysis: All timeouts are on nonlinear uint256 arithmetic (multiplication/division with large symbolic inputs). This is an inherent SMT solver limitation. Two timeouts resolved after the CEI refactoring in the staging red team tightened the reachable state space. Same properties verified by Certora Prover and 160K+ fuzz iterations.

Timed-out proofs: check_feeLessThanAmount, check_fullBuyerRefund, check_noOverflowOnFee, check_noOverflowOnSplit.

Running Halmos

cd contracts
forge build --config-path foundry.toml
halmos --contract HalmosScoreV2 --forge-build-out foundry-out --timeout 120
halmos --contract HalmosEscrowV2 --forge-build-out foundry-out --timeout 120
halmos --contract HalmosResolverV2 --forge-build-out foundry-out --timeout 120

5. Formal Verification (Certora — 19 Rules)

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

Rules Verified:

• feeIs2PercentRule — PLATFORM_FEE_BPS == 200
• feeCalculationCorrect — Math matches specification
• completionPointsConstantRule — COMPLETION_POINTS == 1
• abandonmentPenaltyConstantRule — ABANDONMENT_PENALTY == -5
• tierBoundariesRule — All 11 tiers correct
• resolverRoleConstantRule — Role hash constant
• defaultAdminRoleZeroRule — Admin role is 0x00
• Status transitions, access control, split validation, and more

Running Certora

# From contracts/ directory — CERTORAKEY must be exported (not just sourced)
CERTORAKEY=$(grep "^CERTORAKEY=" .env | cut -d'=' -f2) && export CERTORAKEY
 
certoraRun certora/conf/ScoreV2.conf     --disable_local_typechecking
certoraRun certora/conf/EscrowV2.conf    --disable_local_typechecking
certoraRun certora/conf/ResolverV2.conf  --disable_local_typechecking

6. Mutation Testing (Gambit — 441 Mutants)

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

Running Gambit

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

7. Static Analysis (Slither)

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

Results: 0 High, 0 Medium, 23 Informational (lint-level, no action needed)

Test Metrics

Combined Test Count

Hardhat Unit:       95
Foundry Fuzz:       16
Medusa Parallel:   137
─────────────────────
Total Tests:       248

Halmos Proofs:      60/64
Certora Rules:      19
Gambit Mutants:    441

Test Execution Time

Hardhat Unit Tests:     ~45s
Foundry Fuzz (10K):     ~30s
Medusa Fuzz:            ~5 min
Halmos Symbolic:        ~4 min
Certora:                ~15 min (cloud)
Slither Static:         ~10s
──────────────────────────────
Total Suite:            ~25 minutes

Running the Full Test Suite

cd contracts
 
# Hardhat unit tests
npx hardhat test
 
# Foundry fuzz tests
forge test --fuzz-runs 10000
 
# Medusa parallel fuzz
medusa fuzz --config medusa-v2.json
 
# Halmos symbolic execution
halmos --solver-timeout-assertion 120
 
# Certora formal verification (requires API key)
certoraRun certora/conf/AbbaBabaScore.conf
certoraRun certora/conf/AbbaBabaEscrow.conf
certoraRun certora/conf/AbbaBabaResolver.conf
 
# Slither static analysis
slither . --exclude-dependencies --filter-paths "test|mock|archive"
 
# Gambit mutation testing
gambit mutate --filename contracts/AbbaBabaScore.sol

Continuous Integration

All tests run automatically on every push to main:

smart-contract-security-v2.yml
├── Slither Static Analysis    Passing
├── Foundry Fuzz Tests         16/16 passing
├── Halmos Symbolic            58/64 passing
├── Certora Formal             19 rules verified
└── Mutation Testing           441 mutants generated

Related Documentation

• Audit Dashboard — Full security audit results
• Methodology — Audit process and tools
• Daily Reports — Daily test reports
• Archive — Historical audit records