Verification Protocol

Verification Protocol -- Aptos Move

How to prove a hypothesis is TRUE or FALSE using Move unit tests.

Evidence Source Tracking (MANDATORY)

CRITICAL: For EVERY piece of evidence used in verification, you MUST tag its source. Evidence from mocks or unverified external modules CANNOT support a REFUTED verdict.

Evidence Source Tags

Evidence Audit Table (REQUIRED in every verification output)

Before ANY verdict, fill this table:

### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
|-------|-----------------|-----|-------------------|
| "External module returns X" | Mock module | [MOCK] | NO |
| "State changes to Y" | protocol_module.move:123 | [CODE] | YES |
| "Coin transfer triggers Z" | Aptos Explorer source | [PROD-ONCHAIN] | YES |

Mock Rejection Rule

AUTOMATIC OVERRIDE: If ANY evidence supporting REFUTED has tag [MOCK] or [EXT-UNV]:

• CANNOT return REFUTED
• MUST return CONTESTED
• Triggers production verification

Example:

## Verdict: REFUTED -> CONTESTED (mock evidence override)

### Evidence Audit
| Claim | Source | Tag | Valid? |
|-------|--------|-----|--------|
| "Staking returns shares" | test_staking.move:45 | [MOCK] | NO |

**Override reason**: REFUTED verdict relies on mock behavior at test_staking.move:45.
Production module behavior is UNVERIFIED. Must verify against on-chain source.

Pre-Verification Understanding

Before writing ANY test code, you MUST answer:

Question 1: What is the EXACT bug?

NOT: "Something is inconsistent"
NOT: "State is wrong"
NOT: "Capability leak possible"

YES: "[Variable/resource] is [read/written/moved] at [location] but should be
      [read/written/moved] at [other location] because [specific reason]"

Question 2: What OBSERVABLE difference proves it?

NOT: "Values are different"
NOT: "State changed"

YES: "Before operation: [resource/value] = [expected value]
      After operation: [resource/value] = [actual value]
      Expected: [what it should be]"

Question 3: What is the EXACT assertion?

NOT: assert!(bug_exists, 0)
NOT: assert!(!is_secure, 0)

YES: assert!(actual_value == expected_value, ERROR_CODE)
 OR: assert!(before != after, ERROR_CODE)  // "value changed when it shouldn't"
 OR: assert!(error > threshold, ERROR_CODE)  // "error exceeds acceptable threshold"

If you cannot answer all three -> ASK FOR CLARIFICATION

Pre-PoC Feasibility Gates (MANDATORY)

Before writing test code, verify these two gates. If either FAILS, adjust the hypothesis.

Gate F1: Reachability

Trace a call path from a permissionless entry point to the vulnerable code.

• Entry point identified (public/external/entry function)
• Call path traced through intermediary functions
• All access checks on the path are passable by the attacker profile

If NO entry point reaches the vulnerable code → UNREACHABLE → FALSE_POSITIVE. If reachable only through a restricted path → document the restriction, adjust likelihood.

Gate F2: Math Bounds

Substitute real-world value domains into the expression that triggers the bug.

• Parameter domains identified (token decimals, max supply, TVL range, fee range, time bounds)
• Expression evaluated at worst-case feasible inputs
• Result crosses the bug threshold

If the bug requires values outside feasible domains → INFEASIBLE → FALSE_POSITIVE. If feasible only at extreme but realistic parameters → document the threshold, proceed with adjusted severity.

Both gates PASS → proceed to PoC. Either gate FAILS → document and stop.

Test File Template

See templates.md in this directory for all Move test file templates and Move-specific test patterns.

Interpreting Results

Test PASSES -> Bug CONFIRMED

The assertion that "proves the bug" succeeded.

• If assert!(after != before, 0) passes -> values ARE different (bug exists)
• If assert!(error > threshold, 0) passes -> error IS above threshold (bug exists)

Test FAILS -> Check Why

Common Aptos-Specific Test Issues

Iteration Protocol

Attempt 1: Direct implementation of test strategy from hypothesis

Attempt 2: Adjust parameters

• Different amounts (larger/smaller, boundary values)
• Different timing (advance more/fewer seconds)
• Different actors (swap attacker/victim roles)
• Different resource initialization order

Attempt 3: Re-examine assumptions

• Is setup correct? (all resources initialized, correct init order)
• Are preconditions met? (correct signer, sufficient balance, required state)
• Is the bug mechanism correctly understood?
• Are module dependencies correctly configured in Move.toml?

After 5 attempts:

• If still fails -> FALSE_POSITIVE with documented reasoning
• Explain why the hypothesis was wrong

Severity Determination

CRITICAL

• Direct fund theft possible (drain FungibleStore, mint unlimited tokens)
• Protocol insolvency (assets < liabilities)
• No special prerequisites needed (permissionless exploit)
• Attacker profits significantly
• Ref capability leak granting unrestricted mint/transfer/burn

HIGH

• Fund loss with some setup (specific state required)
• Broken core functionality (deposits, withdrawals, swaps non-functional)
• Significant value at risk
• Cumulative error compounds quickly
• Ref capability leak with limited but significant blast radius

MEDIUM

• Limited fund loss (bounded by rate limits, caps)
• Requires specific conditions (timing, state, multi-step)
• Edge cases with real impact
• Moderate value at risk
• Access control weakness that requires compromised friend module

LOW

• Negligible direct impact
• Extreme edge cases only
• Admin/owner controlled risk with compensating controls
• Informational with minor consequence