Agent skill
verification-protocol
Trigger Pattern Always (used by all verifier agents) - Inject Into security-verifier agents (Phase 5)
Install this agent skill to your Project
npx add-skill https://github.com/PlamenTSV/plamen/tree/main/agents/skills/soroban/verification-protocol
SKILL.md
VERIFICATION_PROTOCOL Skill (Soroban)
Trigger Pattern: Always (used by all verifier agents) Inject Into: security-verifier agents (Phase 5) Purpose: Prove hypotheses TRUE or FALSE using
cargo testwithsoroban-sdktestutils and theEnvharness.
Evidence Source Tracking (MANDATORY)
CRITICAL: For EVERY piece of evidence, tag its source. Evidence from mocks or unverified external contracts CANNOT support a REFUTED verdict.
| Tag | Meaning | Valid for REFUTED? |
|---|---|---|
[PROD-ONCHAIN] |
Production Stellar account/contract data (Horizon RPC / stellar contract read) |
YES |
[PROD-SOURCE] |
Verified source from Stellar Explorer / published audit | YES |
[PROD-FORK] |
Tested with forked production state via stellar-quickstart |
YES |
[CODE] |
Audited codebase (in-scope source) | YES |
[MOCK] |
Mock contracts or test-only state in testutils |
NO |
[EXT-UNV] |
External contract behavior inferred but not verified | NO |
[DOC] |
Documentation/spec only | NO |
Evidence Audit Table (REQUIRED in every verification output)
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
|-------|-----------------|-----|-------------------|
Mock Rejection Rule
If ANY evidence supporting REFUTED has tag [MOCK] or [EXT-UNV]: CANNOT return REFUTED, MUST return CONTESTED, triggers production verification request.
Pre-Verification Understanding
Before writing ANY test code, answer these three questions:
- What is the EXACT bug? -- Not "Authorization is missing" but "Function [withdraw] does not call env.require_auth(&user) before modifying user balances, allowing any caller to withdraw funds (src/lib.rs:line N)"
- What OBSERVABLE difference proves it? -- Concrete before/after values in stroops, expected behavior
- What is the EXACT assertion? -- e.g.,
assert_eq!(client.balance(&attacker), initial_user_balance)orassert!(result.is_err(), "should have panicked")
If you cannot answer all three -> ASK FOR CLARIFICATION
Pre-PoC Feasibility Gates (MANDATORY)
Gate F1: Reachability
- Entry point identified (public
#[contractimpl]function) - Call path traced through internal helpers
- All
require_authchecks passable by attacker profile
If NO public entry point -> UNREACHABLE -> FALSE_POSITIVE. If reachable only through admin-gated path -> document restriction, adjust likelihood.
Gate F2: Math Bounds
- Parameter domains identified (7 decimals for XLM, max supply, TVL range, fee range, ledger bounds)
- Expression evaluated at worst-case feasible inputs
- Result crosses the bug threshold
If values outside feasible domains -> INFEASIBLE -> FALSE_POSITIVE.
Both gates PASS -> proceed to PoC. Either gate FAILS -> document and stop.
Soroban Anti-Hallucination Rules (MANDATORY)
Verify EVERY API call against these known-correct patterns. Do NOT assume Solana/EVM API shapes apply.
// Environment
let env = Env::default(); // NOT: Env::new(), TestEnv::default()
// Auth mocking
env.mock_all_auths(); // Disables ALL auth — for logic tests, NOT auth tests
env.mock_auths(&[MockAuth { ... }]); // Specific auth — for auth flow tests
// Contract registration
let contract_id = env.register(ContractType, ()); // No constructor args
let contract_id = env.register(ContractType, (arg1, arg2,)); // With args
// NOT: env.register_contract(), env.deploy_contract()
// Addresses
let user = Address::generate(&env); // NOT: Address::random(), Pubkey::new_unique()
// Token client (SAC-compatible)
let token_admin = Address::generate(&env);
let (token_address, token_admin_client) = create_token_contract(&env, &token_admin);
let token_client = token::Client::new(&env, &token_address);
// Ledger manipulation
env.ledger().with_mutation(|l| {
l.sequence_number = 100;
l.timestamp = 1_000_000;
});
// NOT: env.set_ledger_sequence(), env.advance_ledger()
// Reading contract storage
let val: T = env.as_contract(&contract_id, || {
env.storage().persistent().get(&DataKey::MyKey).unwrap()
});
// Client invocation
let client = ContractClient::new(&env, &contract_id);
client.my_function(&arg1, &arg2);
// Expecting a panic
let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
client.my_function(&arg1, &arg2)
}));
assert!(result.is_err());
// Storage: persistent (user data), instance (contract-level), temporary (expires on TTL)
env.storage().persistent().set(&key, &value); // .get::<K,V>(), .has()
env.storage().instance().set(&key, &value); // same API
env.storage().temporary().set(&key, &value); // same API
// Auth (production code — what to test against)
env.require_auth(&address); // basic
env.require_auth_for_args(&address, args!(arg1, arg2)); // with args
let auths = env.auths(); // Vec<(Address, AuthorizedInvocation)>
Soroban PoC Test Templates
Template 1: Missing Authorization Check
#[test]
fn test_missing_auth_attacker_can_drain() {
let env = Env::default();
// Do NOT call env.mock_all_auths() — testing that auth IS required
let (admin, user, attacker) = (Address::generate(&env), Address::generate(&env), Address::generate(&env));
let contract_id = env.register(MyContract, (&admin,));
let client = MyContractClient::new(&env, &contract_id);
// Setup: mock admin auth for setup only
env.mock_auths(&[MockAuth {
address: &admin,
invoke: &MockAuthInvoke {
contract: &contract_id, fn_name: "fund_user",
args: (&user, &1000_i128).into_val(&env), sub_invokes: &[],
},
}]);
client.fund_user(&user, &1000_i128);
// EXPLOIT: attacker withdraws without user's auth — if auth missing, succeeds
client.withdraw(&attacker, &user, &1000_i128);
assert_eq!(client.balance(&user), 0_i128, "user drained");
assert_eq!(client.balance(&attacker), 1000_i128, "attacker stole funds");
}
Template 2: Storage Key Collision / Schema Mismatch
#[test]
fn test_storage_key_collision_wrong_deserialization() {
let env = Env::default();
env.mock_all_auths();
let contract_id = env.register(MyContractV2, ());
let client = MyContractV2Client::new(&env, &contract_id);
// Write V1 format data manually (migration scenario)
env.as_contract(&contract_id, || {
env.storage().persistent().set(&DataKey::UserBalance,
&OldDataStruct { field_a: 100_i128, field_b: 50_u64 });
});
// V2 reads V1 data — should trap or return corrupted value
let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| client.get_user_balance()));
if let Ok(balance) = result {
assert_ne!(balance, 100_i128, "Silent data corruption from wrong type");
} // If Err: deserialization trapped — contract bricked for V1 data
}
Template 3: Reentrancy / State Inconsistency
#[test]
fn test_reentrancy_state_inconsistency() {
let env = Env::default();
env.mock_all_auths();
let attacker_id = env.register(AttackerContract, ());
let victim_id = env.register(VictimContract, (&Address::generate(&env),));
let victim_client = VictimContractClient::new(&env, &victim_id);
let attacker_client = AttackerContractClient::new(&env, &attacker_id);
let balance_before = victim_client.total_deposits();
attacker_client.execute_reentrancy_attack(&victim_id);
let balance_after = victim_client.total_deposits();
assert!(attacker_client.profit() > 0, "Reentrancy should be profitable");
assert!(balance_after < balance_before, "Victim drained: before={}, after={}",
balance_before, balance_after);
}
Template 4: Arithmetic Overflow / Precision Loss
#[test]
fn test_arithmetic_precision_loss_at_boundary() {
let env = Env::default();
env.mock_all_auths();
let contract_id = env.register(VaultContract, ());
let client = VaultContractClient::new(&env, &contract_id);
let user_a = Address::generate(&env);
let user_b = Address::generate(&env);
// XLM: 7 decimal places (1 XLM = 10_000_000 stroops)
client.deposit(&user_a, &1_i128); // 1 stroop
client.deposit(&user_b, &10_000_000_000_000_i128); // 1M XLM
let user_a_shares = client.shares(&user_a);
let user_a_withdraw = client.withdraw(&user_a, &user_a_shares);
assert_eq!(user_a_withdraw, 1_i128,
"User A lost deposit to rounding: received {}", user_a_withdraw);
}
Template 5: Ledger Sequence / Timestamp Manipulation
#[test]
fn test_cooldown_bypass_same_ledger_sequence() {
let env = Env::default();
env.mock_all_auths();
let contract_id = env.register(CooldownContract, ());
let client = CooldownContractClient::new(&env, &contract_id);
let user = Address::generate(&env);
env.ledger().with_mutation(|l| { l.sequence_number = 100; l.timestamp = 1_000_000; });
client.action(&user);
// Same ledger — Soroban consecutive ledgers CAN have same timestamp
env.ledger().with_mutation(|l| { l.sequence_number = 100; l.timestamp = 1_000_000; });
let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
client.action(&user)
}));
assert!(result.is_err(), "Cooldown bypassed in same ledger");
}
Template 6: try_invoke_contract Partial State
#[test]
fn test_try_invoke_partial_state_on_external_error() {
let env = Env::default();
env.mock_all_auths();
let failing_external = env.register(FailingExternalContract, ());
let contract_id = env.register(ProtocolContract, (&failing_external,));
let client = ProtocolContractClient::new(&env, &contract_id);
let user = Address::generate(&env);
let initial = client.recorded_deposit(&user);
let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
client.deposit(&user, &1000_i128)
}));
if result.is_ok() {
assert_eq!(client.recorded_deposit(&user), initial,
"Partial state: deposit recorded despite external failure");
}
}
Fuzz Variant (Medium+, Soroban-specific)
Build/test commands and fallback logic are in phase5-poc-execution.md. Below: Soroban-specific harness patterns.
cargo-fuzz (nightly): Use Env::default() + mock_all_auths() + env.register() in harness. Derive fuzz inputs from &[u8] via i128::from_le_bytes. Assert invariants inside catch_unwind. Run: cargo +nightly fuzz run fuzz_target_1 -- -max_total_time=300
proptest (stable fallback):
proptest! {
#[test]
fn test_fuzz_invariant(amount in 1_i128..1_000_000_000_000_i128, seq in 1_u32..100_000_u32) {
let env = Env::default();
env.mock_all_auths();
env.ledger().with_mutation(|l| { l.sequence_number = seq; });
let contract_id = env.register(MyContract, ());
let client = MyContractClient::new(&env, &contract_id);
let user = Address::generate(&env);
let _ = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
client.target_function(&user, &amount);
prop_assert!(client.balance(&user) >= 0);
}));
}
}
Dual-Perspective Verification (MANDATORY)
Phase 1 -- ATTACKER: Complete call sequence? Contracts to deploy? Profit in stroops? Compose multiple invoke_contract calls? Which require_auth is missing/bypassable?
Phase 2 -- DEFENDER: What require_auth prevents this? What storage key uniqueness ensures correct targeting? What external contract validation blocks substitution? Why safe by design?
Phase 3 -- VERDICT: Which argument won?
Realistic Parameter Validation
Substitute ACTUAL contract constants. Apply Rule 10: worst realistic operational state, not current snapshot.
State: 'With real constants [fee_bps=X, precision=7_decimals, tvl=Z] at worst-state
[max_users, min_balance], bug triggers when [condition]'
OR: 'With real constants, bug does NOT trigger because [reason]'
Stellar-specific constants: XLM = 10,000,000 stroops (7 decimals) | Base reserve = 0.5 XLM (5,000,000 stroops) | Max TTL = 3,110,400 ledgers (~1yr at 5s) | Default min persistent TTL = 120 ledgers (~10min)
Anti-Downgrade Guard (MANDATORY for VS/BLIND findings)
Apply Rule 13's 5-question test BEFORE downgrading severity or marking FALSE_POSITIVE:
- Who is harmed by this design gap?
- Can affected users avoid the harm?
- Is the gap documented in protocol docs?
- Could the protocol achieve the same goal without this gap?
- Does the function fulfill its stated purpose completely?
HARD RULE: Contract A has protection X but Contract B lacks it for same user action -> defense parity gap, NOT "by design". Minimum severity: Medium.
New Observations (MANDATORY)
If during verification you discover a NEW bug not covered by any hypothesis:
- [VER-NEW-1]: {title} -- {contract:function} -- {brief description}
Error Trace Output (MANDATORY for CONTESTED/FALSE_POSITIVE)
- Failure Type: AUTH_REQUIRED / CONTRACT_TRAP / ARITHMETIC_OVERFLOW / STORAGE_MISSING / UNEXPECTED_STATE
- Location: {contract}:{function}:{approximate line}
- Error Code: {Soroban host error, e.g.,
WasmVm(InvalidAction),Auth(NotAuthorized)} - State at Failure: {key storage values}
- Investigation Question: {What would resolve this}
RAG Queries Before PoC (MANDATORY for HIGH/CRITICAL)
get_attack_vectors(bug_class="{category}")get_similar_findings(pattern="{vulnerability description}")validate_hypothesis(hypothesis="{finding summary}")search_solodit_live(keywords="{soroban stellar vulnerability pattern}", impact=["HIGH","CRITICAL"], language="Rust", quality_score=3, max_results=15)
Document in output: Attack Vectors Consulted, Similar Exploits Found, Historical Precedent.
RAG Confidence Override
| RAG Confidence | Local Verdict | Final Verdict |
|---|---|---|
| >= 7/8 matches | FALSE_POSITIVE | CONTESTED (override) |
| >= 6/8 matches | FALSE_POSITIVE | CONTESTED (override) |
| < 6/8 matches | FALSE_POSITIVE | FALSE_POSITIVE (allowed) |
Chain Hypothesis PoC Requirements
Chain hypotheses receive PRIORITY verification. Test the COMPLETE sequence: (1) execute enabler action, (2) assert postcondition created via env.as_contract() storage read, (3) execute previously-blocked exploit, (4) assert combined impact exceeds either finding alone. Use standard Env::default() + mock_all_auths() + env.register() setup.
Interpreting Results
Test PASSES -> Bug CONFIRMED
Test FAILS -> Check Why
| Failure | Meaning | Action |
|---|---|---|
Auth error (NotAuthorized) |
require_auth IS present |
Re-examine hypothesis |
| Contract trap / WasmVm error | Logic assertion failed | Check if assertion is the bug or the fix |
| Arithmetic panic | Overflow protection present | Check if complete or partial |
Storage unwrap() panic |
Entry does not exist | Fix test setup |
| Wrong balance | Setup amounts incorrect | Verify stroops (7 decimals for XLM) |
Iteration Protocol
Attempt 1: Direct implementation from hypothesis. Attempt 2: Adjust parameters (amounts, ledger state, call ordering). Attempt 3: Re-examine assumptions (auth mocking, storage keys, stroop vs XLM). Attempt 4: Verify function signatures in source -- do NOT assume Solana/EVM shapes. Attempt 5: Re-read anti-hallucination rules -- confirm correct Soroban testutils API. After 5 attempts: FALSE_POSITIVE with documented reasoning.
Insufficient Evidence (HALT CONDITIONS)
Before marking REFUTED, check ALL boxes:
- External contract behavior verified against PRODUCTION (not mock)
- Attack path checked on ALL public functions accessing same storage
- Profit calculated with attacker HOLDING tokens (not just calling)
- Missing precondition documented (STATE / ACCESS / TIMING / EXTERNAL / BALANCE)
- Searched other findings for matching postconditions (chain integration)
- Storage key derivation verified against actual DataKey enum
-
require_authcalls verified by reading source (not assumed) - TTL of relevant storage entries verified (Temporary may have expired)
Evidence That Does NOT Count
- "Mock external contract shows X" -- mocks are not production
- "Function is called with
invoke_contract" -- does not bypassrequire_auth - "Attacker loses by sending tokens" -- may profit via position held elsewhere
- "Function is
pub(crate)" -- may be reachable via cross-contractinvoke_contract - "Requires admin" -- admin may be compromised EOA or malicious upgrade
- "Storage key cannot collide" -- verify actual
DataKeyenum
Output Format
CONFIRMED
## Verdict: CONFIRMED
### Bug Mechanism Verified
{2-3 sentences on what cargo test proves}
### Test Code
{Full Rust test using soroban-sdk testutils}
### Test Output
{Assertions and values from `cargo test -- --nocapture`}
### Key Evidence
| Metric | Value |
|--------|-------|
| Before / After / Expected / Difference | {stroops} |
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Severity: {LEVEL}
{1-2 sentence justification}
### Suggested Fix
{diff block + Fix scope + Verified: YES/NO}
FALSE_POSITIVE
## Verdict: FALSE_POSITIVE
### Attempts Made
**Attempt 1-N:** Approach, Result (error type/code), Learning
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Why It Is Not a Bug
{2-3 sentences}
### Error Trace
{Failure Type, Location, Error Code, State at Failure, Investigation Question}
CONTESTED
## Verdict: CONTESTED
### Evidence Status
| Checkpoint | Status | Details |
|------------|--------|---------|
| External contract verified against PRODUCTION | YES/NO | |
| All public function paths checked | YES/NO | |
| Auth flow completeness confirmed | YES/NO | |
| Storage TTL verified | YES/NO | |
### Evidence Audit
| Claim | Evidence Source | Tag | Valid for REFUTED? |
### Why This Cannot Be REFUTED
{What evidence is missing}
### Escalation Required
- [ ] Fetch production WASM/state for {external dep}
- [ ] Verify storage keys match DataKey enum in production
- [ ] Check additional function paths: {list}
### Error Trace
{as above}
Recommended Agent Skills
Expand your agent's capabilities with these related and highly-rated skills.
integration-hazard-research
Protocol Type Trigger NAMED_EXTERNAL_PROTOCOL (detected when recon finds import/interface for an identifiable external protocol — not standard libraries). Researches known integration hazards of the target protocol.
outcome-determinism
Protocol Type Trigger outcome_determinism - detected when EITHER of these code patterns are present - - Selection from finite depletable pool with fallback behavior (while(full)...
governance-attack-vectors
Protocol Type Trigger governance (detected when Governor, Timelock, voting, proposal, quorum, delegate patterns found) - Inject Into Breadth agents, depth-external, depth-edge-case
vault-accounting
Protocol Type Trigger vault (detected in recon TASK 0 Step 1) - Inject Into Core state agent OR economic design agent (merge via M4 hierarchy)
lending-protocol-security
Protocol Type Trigger lending (detected when recon finds liquidate|borrow|repay|collateral|lend|loan|LTV|healthFactor|interestRate|debtToken) - Inject Into Breadth agents, depth...
dex-integration-security
Protocol Type Trigger dex_integration (detected when recon finds swap|addLiquidity|removeLiquidity|IUniswapV2Router|ISwapRouter|amountOutMin|amountOutMinimum|slippage - AND the...
Didn't find tool you were looking for?