/verification-protocol

name: "verification-protocol"
description: "How to prove a hypothesis is TRUE or FALSE using Move unit tests."

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

| Tag | Meaning | Valid for REFUTED? | |-----|---------|-------------------| | [PROD-ONCHAIN] | Production module verified on Aptos Explorer | YES | | [PROD-SOURCE] | Source code verified on-chain (Aptos Explorer source verification) | YES | | [CODE] | Audited codebase (in-scope) | YES | | [MOCK] | Mock/test module | **NO** | | [EXT-UNV] | External module, unverified behavior | **NO** | | [DOC] | Documentation/spec only | NO (needs verification) |

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`](references/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

| Failure | Meaning | Action | |---------|---------|--------| | Assertion failed (abort code) | Bug doesn't exist as hypothesized | Re-examine hypothesis | | Abort in setup | Module initialization wrong | Fix setup (check init order, missing resources) | | Abort in action | Operation blocked (access control, precondition) | Check preconditions, signer requirements | | ARITHMETIC_ERROR (0x20001) | Overflow/underflow or division by zero | Check calculations, validate inputs | | RESOURCE_NOT_FOUND | Missing `move_to` in setup | Ensure all required resources are initialized | | ALREADY_EXISTS | Duplicate resource creation | Check init called only once |

Common Aptos-Specific Test Issues

| Issue | Cause | Fix | |-------|-------|-----| | `ENOT_FOUND` on coin operations | Account not registered for coin type | Add `coin::register<CoinType>(user)` before operations | | Timestamp not available | `timestamp` module not initialized | Add `timestamp::set_time_has_started_for_testing(aptos_framework)` | | Object not found | Object created at unexpected address | Use `object::create_named_object` with deterministic seed | | Module not published | Test module can't import protocol module | Check `Move.toml` dependencies and test address mapping | | Signer mismatch | `@protocol_addr` doesn't match expected | Verify `#[test