Xray Pre Audit

X-Ray Pre-Audit Reconnaissance

Overview

X-Ray generates a structured pre-audit readiness report that gives auditors (human or AI) a fast, accurate understanding of a protocol before diving into line-by-line review. The output is an x-ray/ folder at the project root containing:

Adapted for the EVM Cortex squad from the Pashov Audit Group x-ray skill (upstream: github.com/pashov/skills, skill x-ray, VERSION 2 — see the VERSION file alongside this one). The three scripts under scripts/ are upstream code carried over intact and are the source of truth for enumeration, git security analysis, and SVG generation — the prose here tells you when to call them and how to read their output, never how to reimplement them.

X-Ray is fully autonomous. It runs without user interaction, produces concrete artifacts, and never fabricates findings. When something cannot be determined from the code, it says so explicitly.

When to Invoke

• A new audit engagement begins and you need to orient quickly
• You are asked to "review", "audit", or "assess" a Solidity codebase
• The audit-orchestrator agent kicks off a Light, Core, or Thorough audit
• A developer asks "is this codebase audit-ready?"
• You need to build a threat model or protocol overview from scratch

Relationship to Other Audit Skills

Progress Tracking (Mandatory)

Before doing anything else, call TodoWrite with these three todos, all pending:

1. Phase 1: Enumerate & measure codebase
2. Phase 2: Read sources, classify entry points, synthesize invariants
3. Phase 3: Write x-ray report files

Transitions — update via TodoWrite, never batch:

• Mark Phase 1 in_progress immediately, before running enumeration.
• When Step 1's parallel batch returns, in ONE TodoWrite call mark Phase 1 completed and Phase 2 in_progress.
• When Step 2 (including all sub-steps) finishes, in ONE TodoWrite call mark Phase 2 completed and Phase 3 in_progress.
• After all Step 8 output files are written and the diagram is validated, mark Phase 3 completed.

Rule: exactly one todo is in_progress at any time. Status updates happen the moment a phase starts or ends.

Step 1: Enumerate & Measure

Before reading any code, quantify the target. Numbers ground the analysis and calibrate effort.

Project Root & Source Directory Detection

If the user specifies a path, use it as project root. Otherwise use cwd. If no .sol files or foundry.toml / hardhat.config.* at root, check one level deep.

ROOT="${1:-.}"
cd "$ROOT" || exit 1

# Toolchain
if   [ -f foundry.toml ]; then TOOLCHAIN=foundry
elif [ -f hardhat.config.js ] || [ -f hardhat.config.ts ]; then TOOLCHAIN=hardhat
else TOOLCHAIN=unknown; fi
echo "toolchain: $TOOLCHAIN"

# Source dir: foundry.toml `src = "..."`, else hardhat `contracts/`, else try both
SRC=$(sed -nE 's/^[[:space:]]*src[[:space:]]*=[[:space:]]*"([^"]+)".*/\1/p' foundry.toml 2>/dev/null | head -1)
[ -z "$SRC" ] && { [ -d src ] && SRC=src; }
[ -z "$SRC" ] && { [ -d contracts ] && SRC=contracts; }
[ -d "$SRC" ] || { echo "ERROR: source directory not found"; exit 1; }
echo "src: $SRC"

mkdir -p x-ray

All shell in this skill uses POSIX ERE only — no -P / PCRE, no GNU-only escapes (\s, \w, \b). This keeps every command identical on macOS BSD grep, Linux GNU grep, and ripgrep. Use [[:space:]], [[:alnum:]_], and explicit alternation instead.

Enumeration

Run the bundled enumeration script as a single Bash call. It creates the output directory and emits labeled sections consumed by every later step.

mkdir -p {project-root}/x-ray && bash {SKILL_DIR}/scripts/enumerate.sh {project-root} {src-dir}

{SKILL_DIR} is this skill's directory. The script covers, in one pass: toolchain detection, source files with line counts, per-file and total nSLOC, NatSpec density, test presence, fuzz/formal-verification detection, docs, current commit, and git history statistics. Do not reimplement any of it inline — the script handles quoting and exclusion edge cases that ad-hoc greps get wrong.

Version Check

In the same parallel message as enumeration:

curl -sf https://raw.githubusercontent.com/pashov/skills/main/x-ray/VERSION

Compare against this skill's local VERSION file. If the remote value is higher, print ⚠️ Upstream x-ray is at version N, this skill is vendored at 2. See https://github.com/pashov/skills. If the fetch fails, skip silently — a network failure is not an audit finding.

Reading the Test Signals

Test presence comes from the file scan above. It is always reliable, even when the toolchain cannot compile — which is exactly why it is measured separately from coverage.

Multi-signal categories (echidna, medusa, halmos, certora) report as functions:configs. 5:1 means 5 test functions plus 1 config file. A config with zero functions is worth flagging on its own: the harness exists but nobody wrote properties for it.

A protocol with high test_functions and zero stateful or formal signals is a specific, reportable readiness gap: the state space has never been searched. Route that to fizz for an Echidna/Medusa suite.

Coverage (Background)

Launch coverage in the background. Do not wait for it.

# Foundry
forge coverage 2>&1 || (echo "RETRYING_WITH_IR_MINIMUM" && forge coverage --ir-minimum 2>&1)
# Hardhat
npx hardhat coverage 2>&1

If the toolchain is not installed (forge: command not found, missing node_modules/), this fails. That is expected and carries no information about test quality — see the test-existence rules in Step 8.

Dependency Snapshot

forge tree 2>/dev/null | head -40
grep -rE 'openzeppelin|solady|solmate' foundry.toml remappings.txt 2>/dev/null | head -10
ls lib/ 2>/dev/null

Spec / Whitepaper Detection

Glob **/{whitepaper,spec,design,protocol,architecture,overview,README}*.{pdf,md}, excluding node_modules/, lib/, x-ray/, test/. Skip user-facing docs — tutorials, API references, changelogs, contribution guides. Then apply size-aware handling:

• Path A (≤5 docs, each ≤300 lines) — read them directly as part of the Step 2 parallel message. No subagent needed.
• Path B (>5 docs, or any doc >300 lines) — launch a single scout subagent that reads all doc files and returns a structured extraction of at most 200 lines, with these headings only: Doc-Stated Global Invariants, Actor Definitions, Trust Assumptions, Cross-System Flows, Economic Properties, Key Design Decisions. Require a source quote per claim; omit empty headings.

Extract only: doc-stated global invariants, actor definitions, cross-system flows, trust assumptions, economic properties, key design decisions. Tag every spec-derived claim in the report with (per spec) so auditors can tell code-verified from spec-stated. Doc-stated global invariants feed the NatSpec routing pass in Step 5 — they route to §2/§3/§4 of invariants.md by shape, never to §1 (which is per-call guards only).

Parallel Batch Rule

Issue enumeration, background coverage, git analysis (Step 6), the reference doc reads, and the spec glob in the same message. Proceed to Step 2 without waiting for coverage.

Step 2: Source Analysis

Scope Filtering

• Skip interfaces: interfaces/ directories, or filenames matching I followed by an uppercase letter.
• Skip vendored libraries: copies of Uniswap FullMath/TickMath, OpenZeppelin, Solady, Solmate.
• Skip mocks and test doubles.
• When uncertain, read the file but exclude it from the scope table.

Do NOT read test files or documentation files in this step.

Two Scan Paths

Choose by in-scope source file count.

Path A — ≤20 source files: direct reads

One Read call per file, all in a single parallel message alongside the entry point grep scan. Do not re-read README, docs, or foundry.toml — Step 1 already covered them.

Path B — >20 source files: fan out to parallel subagents

Each Tier 2 subagent extracts facts only — no analysis — and returns the per-file structure below.

Per-File Extraction Contract

Both paths must produce the same facts per file:

• Type — contract, abstract contract, library, or interface
• Inherits — full linearization (affects function resolution order)
• Imports — libraries and contracts pulled in
• Roles / access control — modifiers, role constants, msg.sender checks
• Value-holding state — mappings and variables holding balances, collateral, stakes, reserves, debt
• External calls — every call to another contract, including token transfers
• Fund flows — deposit / withdraw / mint / burn / transfer / borrow / repay / liquidate paths
• Invariant comments — NatSpec @invariant tags, require/assert statements
• Backwards-compatibility indicators — see Step 2c
• Key logic — one or two sentences on what the contract does
• Function-level access map (contracts only, skip libraries) — every public/external non-view non-pure function with its modifier, or NONE — permissionless. For functions with no modifier, also list the external calls they make.

Three extractions carry the invariant synthesis in Step 5 and must be captured precisely:

Delta writes — for each non-view non-pure function, the storage variables that change and the symbolic delta applied. Format Δ(var) = +expr or Δ(var) = -expr. Same-basic-block only; report a pair only when both writes appear in the same function body with no intervening call to an unknown external contract. Do not chase writes through inherited or imported functions unless the semantic effect is unambiguous — OpenZeppelin _mint touching balanceOf and _totalSupply is fine, custom internal helpers are not. List a custom helper's deltas under that helper's own entry.

deposit(): Δ(totalSupply) = +shares, Δ(balanceOf[msg.sender]) = +shares
borrow():  Δ(totalBorrows) = +amount, Δ(underlyingBalance) = -amount

Guard predicates — every require / assert / if-revert that references a storage variable, quoted verbatim with its line number. Skip guards that reference only function parameters.

Vault.sol:206: require(_fee <= 10, "fee is capped at 0.1%")

Enum / one-shot transitions — every require(var == X); ...; var = Y pair where var is a storage enum, uint, or address. Record as X@Lx → Y@Ly. Include one-shot latches such as require(addr == address(0)); addr = concrete.

Entry Point Grep Scan

Issue both greps in the same parallel message as the source reads — they are independent.

# 1. Single-line signatures: name and visibility on the same line
grep -rnE 'function[[:space:]]+[[:alnum:]_]+[[:space:]]*\([^)]*\)[[:space:]]+(external|public)' "$SRC"/ --include='*.sol' \
  | grep -v '/interfaces/' | grep -v '/mock/' \
  | grep -Ev '(^|[^[:alnum:]_])(view|pure)([^[:alnum:]_]|$)'

# 2. Multiline signatures: visibility on the closing-paren line (covers 90%+ of multiline cases)
grep -rnE '^[[:space:]]*\)[[:space:]]+(external|public)' "$SRC"/ --include='*.sol' -B5 \
  | grep -v '/interfaces/' | grep -v '/mock/' \
  | grep -Ev '(^|[^[:alnum:]_])(view|pure)([^[:alnum:]_]|$)'

Combine both result sets. The multiline grep is not optional — Solidity routinely splits parameters across lines, leaving external/public on the ) line while function name( sits several lines above. The trailing filter is the POSIX-portable substitute for \b(view|pure)\b: it drops lines where view or pure appears as a standalone identifier while preserving identifiers like view_param.

Step 2b: Entry Point Classification

Classify all entry points using the grep results plus the function bodies. Do not rely on subagent summaries alone — subagents extract facts at contract level and can misattribute which function makes which call or carries which modifier.

Exclude: view/pure functions, interface-only declarations, library internal functions (downstream calls, not entry points), mock contracts.

A function without a modifier is NOT automatically permissionless. You MUST verify the body before classifying. In Path A the bodies are already in context — classify directly. In Path B, batch all candidate body reads into a SINGLE parallel message. Look for any of:

require(msg.sender == expected);
if (msg.sender != expected) revert Unauthorized();
if (msg.sender != a || cond) revert Unauthorized();   // compound
_checkCaller();                                        // internal check

A modifier-free function with an internal msg.sender check is role-gated. Common offenders: acceptOwnership(), acceptMsig(), confirmX() — no modifier, but restricted to a pending address.

nonReentrant alone is NOT access control.

Record per entry point:

Parameter trust levels: (user-controlled) the caller picks the value freely, (user-signed) the value comes from a user's offchain signature, (keeper-provided) a keeper selects it, (protocol-derived) read from onchain state.

Call chains use concrete contract names, not interface names — write FuturesManager.addCollateral(), not ICollateralManager.addCollateral(). Interfaces describe how the caller references the target; the auditor needs to know which contract actually executes. The only exception is genuinely external third-party contracts (IERC20.safeTransfer()).

The grep scan is a hard gate: the permissionless list in the report must match the grep-verified, body-checked result. Where grep plus code reading conflicts with a subagent summary, grep wins.

Step 2b-flow: Protocol Flow Path Construction

Reorganize the Step 2b data into flow paths for entry-points.md. This is not a new analysis pass and needs no new tool calls.

For each major user-facing entry point (permissionless and role-gated functions that move value):

1. Identify its require statements and state variable checks.
2. For each check, find which function WRITES that state variable — already known from other entry points' "State modified" field.
3. Chain backwards: destination ← writer of its precondition ← writer of THAT precondition ← … ← deployment.
4. Annotate non-function preconditions (time passage, market conditions, position health, available liquidity) with ◄──.

Output is simple arrow chains grouped by actor, 15-30 lines total. Reference earlier flows ([owner setup above]) instead of repeating them.

Step 2c: Backwards-Compatibility Code Detection

Watch for code that looks like the remnant of a removed mechanism, kept so the rest of the codebase still compiles. Signals: empty or trivial function bodies, state variables declared but never meaningfully read or written, comments containing "deprecated" / "legacy" / "backwards compat" / "no longer used", interface implementations that always return a default, storage variables preserved solely for proxy layout compatibility.

After reading ALL source files, cross-reference candidates against these mandatory checks. Batch every caller-check Grep for all candidates into a SINGLE parallel message — do not verify one at a time.

1. Caller check (required) — confirm via Grep that the function or variable has NO active callers. If it IS called from an active path, it is the current design, regardless of whether it returns defaults.
2. NatSpec / comment check (required) — if NatSpec or inline comments explain why it behaves this way ("simplified for X mode", "by design", "intentionally zero"), this is documented intentional design. Do not override explicit developer documentation with heuristic pattern matching.
3. Interface obligation check — a function returning defaults because an interface requires it AND that is actively called is part of the current architecture, not a remnant.

Classify as backwards-compatibility only when ALL of: no active callers, no NatSpec/comments documenting the behavior as intentional, and git history shows the mechanism it belonged to was removed.

Never describe backwards-compatibility code as an active feature. Note it explicitly in Section 1 so auditors do not burn time investigating dead code. If nothing survives the checks, omit the subsection entirely.

Step 2d: Centralization & Pause Coverage Analysis

Two analyses that feed into existing report sections. Neither produces a standalone section.

Centralization analysis — for each privileged role (admin, owner, operator, keeper, service):

1. List every operational action the role can take, from the function-level access map.
2. For each action, note whether a timelock, multisig, or delay exists. Distinguish role transfer delays (for example AccessControlDefaultAdminRules' 1-day delay) from operational action delays. A role transfer delay does NOT protect against a compromised holder using instant operational functions.
3. Identify which actions can extract or redirect user funds (emergencyWithdraw, setTreasury, transferFee).

Integrate into Actors (Capabilities column states what is instant versus delayed), Trust Boundaries (what each boundary actually protects versus what bypasses it), and Key Attack Surfaces (framed as "Admin operational powers" or "[Role] compromise" — the surface is the role compromise, not the individual functions).

Pause coverage analysis — for each critical state-changing function, check whether whenNotPaused or an equivalent applies; note which functions are pausable and which are not. A function that should logically be pausable but is not (for example one callable by a bounded role that operates on user funds) is a detail that worsens that role's compromise scenario — fold it into that role's attack surface rather than raising it independently.

Anti-pattern: do NOT create a standalone "Centralization Risks" section. Centralization detail belongs distributed across Actors, Trust Boundaries, Key Attack Surfaces, and Protocol-Type Concerns. A dedicated section duplicates what those already say. Same for pause coverage.

Step 2e: nSLOC

Use the exact nSLOC TOTAL from Step 1 enumeration — no ~ prefix — in the report header and scope table.

Step 3: Protocol Classification

Protocol Type Detection

Detect type from function signatures, state variables, and architectural patterns found during Step 2. A protocol may match multiple types. Rank by signal density; the type with the most matches is primary.

Hybrid Classification

1. Rank by signal count — more matches means more weight in the threat model.
2. The primary type determines adversary ranking order.
3. Secondary types add their unique threats, de-duplicating overlapping ones.
4. State in the report: "Protocol classified as [Primary] with [Secondary] characteristics."

A protocol with swap(), addLiquidity(), borrow(), liquidate() is Primary DEX/AMM, Secondary Lending.

Temporal Phase Detection

Protocols face different dominant threats at different points in their lifecycle. Detect which phases are relevant from code signals; include only those in the threat model.

Step 4: Threat Model Construction

The threat model is the analytical core of X-Ray. It maps actors, trust boundaries, and attack surfaces.

How to Use the Threat Profiles

The profiles below are a threat identification library, not prose to paste into the report. Use them to know what to look for and who threatens this protocol, then translate that into the report's format.

DO-NOT-EXPLOIT RULE (critical). Attack surfaces describe the concern area, not the exploit. The auditor's value is building the attack path; yours is finding the area fast. If a bullet contains "→ attacker drains X", "→ user trapped", "→ inflated share", "double-counts W", "leads to understated N" — cut it. Replace with "Worth checking…", "Worth tracing…", "Worth confirming…". Name the asymmetry, the divergence, the unusual pattern, the cross-path bookkeeping, then stop.

The exploit-chain prose inside this Step 4 library (for example "oracle manipulation → inflated collateral → drain the pool") is intentional here — it teaches the threat. It is forbidden in the report.

Actor Enumeration

Only named roles from the code. Never "Anyone". Never "Semi-trusted" — use "Bounded (reason)".

Capabilities cells are a scannable reference, not a capability paragraph. For roles with many powers, summarize and enumerate only the dangerous ones inline. Aim for two lines per cell.

Then produce an Adversary Ranking ordered by threat level for this protocol type, adjusted by git evidence. Three to five entries, ONE sentence each stating WHO they are and WHY they matter here. Attack mechanics and code references belong in Key Attack Surfaces, not here.

Trust Boundary Map

┌─────────────────────────────────────────────┐
│ UNTRUSTED ZONE (public internet)            │
│  Users, Flashloan attackers, MEV searchers  │
├─────────────────────────────────────────────┤
│ PROTOCOL BOUNDARY                           │
│  ┌──────────────┐    ┌──────────────┐       │
│  │ Vault.sol    │───▶│ Strategy.sol │       │
│  │ (entry point)│    │ (internal)   │       │
│  └──────┬───────┘    └──────┬───────┘       │
│         │                   │               │
├─────────┼───────────────────┼───────────────┤
│ EXTERNAL TRUST BOUNDARY     │               │
│  ┌──────▼───────┐    ┌──────▼───────┐       │
│  │ Chainlink    │    │ Aave V3      │       │
│  │ (oracle)     │    │ (lending)    │       │
│  └──────────────┘    └──────────────┘       │
├─────────────────────────────────────────────┤
│ ADMIN TRUST BOUNDARY                        │
│  Multisig → Timelock → Parameter changes    │
└─────────────────────────────────────────────┘

For each boundary state what is trusted, the damage if compromised, and whether a timelock or multisig exists. Where a delay protects only the role seat and not operational actions, say so explicitly: "1-day delay protects the admin seat, but emergencyWithdraw and setFee execute instantly." If git analysis shows boundary code was frequently modified or carries fix-scored commits, append *Git signal: N modifications, M fix-scored commits — elevated risk.*

Protocol-Type Threat Profiles

Lending / Borrowing

Adversaries, ranked: flash loan attacker (drives oracle manipulation cost to near zero) → oracle manipulator (the oracle is the sole source of truth for solvency) → liquidation MEV searcher (if extraction makes liquidation unprofitable for honest liquidators, bad debt accrues) → malicious first depositor (share-price manipulation on supply/debt tokens) → compromised admin (collateral factors, oracle address, rate model, pause).

Dominant patterns: oracle manipulation → inflated collateral → max borrow → drain pool. Flash borrow → manipulate spot → liquidate victim at wrong price. Bad debt via unliquidatable positions (oracle lag, gas spikes, illiquid collateral). Utilization manipulation to move interest rates. Recursive borrowing amplification.

Critical invariants: totalBorrows <= totalCollateral * LTV per market and per account. Every position is liquidatable before it can cause bad debt. Liquidation is profitable for liquidators. Oracle price is within acceptable deviation and freshness bounds. Interest accrual is monotonic and unmanipulable.

Look first at: the complete price path (oracle read → normalization → collateral value → health factor — every step is a manipulation point); whether one transaction can borrow, manipulate, and liquidate; liquidation math against gas plus slippage; share price when totalSupply == 0; what admin can change instantly versus through timelock.

DEX / AMM

Adversaries, ranked: MEV searcher / sandwich attacker (every swap without adequate slippage protection is a guaranteed extraction) → flash loan price manipulator → malicious first LP / empty pool attacker → liquidity manipulation attacker → compromised admin (fees, pause, routing, pool whitelist).

Dominant patterns: sandwich attacks. LP share inflation on empty pools via donation. Reentrancy through token callbacks (ERC-777, ERC-1155) while pool state is inconsistent. Spot price exploitation when other protocols read the pool as an oracle. Concentrated liquidity tick manipulation. Fee-on-transfer accounting breaks.

Critical invariants: pool invariant holds before and after every operation. LP share value is monotonically non-decreasing from fees. No tokens leave without proportional LP burn or valid swap math. Swap output matches invariant-derived calculation exactly. Tracked reserves match actual balances.

Look first at: swap math rounding direction; LP mint/burn at totalSupply == 0 and minimum liquidity enforcement; whether the pool exposes getPrice()/observe() (then manipulation has external blast radius); where slippage protection is enforced and whether it can be bypassed; state updates versus external calls in the swap path.

Yield Aggregator / Vault

Adversaries, ranked: share inflation attacker (deposit 1 wei, donate a large amount, next depositor rounds to 0 shares) → malicious or compromised strategy (strategies hold the actual funds) → reentrancy through external protocol callbacks → donation / direct-transfer attacker → compromised admin (add strategies, allocation weights, harvester, migrate funds).

Dominant patterns: ERC-4626 share inflation. Strategy reports fake gain, attacker deposits at inflated price, previous depositors diluted. Strategy retains approvals after migration. Harvest sandwich. Accounting desync when the strategy's real balance drifts from recorded allocation (rebasing, slashing, reward accrual).

Critical invariants: totalAssets() accurately reflects real underlying value. convertToShares(convertToAssets(shares)) <= shares and the reverse. Strategy cannot extract more than allocated. Share price rises only from yield.

Look first at: virtual offset or minimum deposit protecting share math; what a strategy may report and who may add or remove strategies; whether totalAssets() uses balanceOf(this) (donation-exposed) or internal accounting; reentrancy protection and state-before-call ordering; whether migration revokes old approvals.

Stablecoin

Adversaries, ranked: oracle manipulator → economic/governance attacker (collateral parameters, stability fees) → bank run attacker (strategic redemption drains the best collateral) → flash loan minter → compromised admin (collateral types, oracle, debt ceilings, pause redemptions).

Dominant patterns: manipulate collateral price, mint at inflated value, sell, leaving the protocol undercollateralized. Algorithmic death spiral. Redemption DoS draining liquid collateral. Governance-set undercollateralized ratios. Staleness arbitrage between mint and redeem.

Critical invariants: every unit is backed by at least the configured collateral ratio. Mint and redeem are inverse — round-trip preserves value. The peg mechanism converges under sell pressure rather than diverging. Liquidation can always restore individual position collateralization. Total supply is within the debt ceiling across all collateral types.

Look first at: the mint path (accepted collateral → valuation → ratio → who can change the ratio); the redeem path under stress and whether all units can redeem simultaneously; liquidation profitability; what governance can change and how fast; whether a 10% depeg self-corrects or amplifies.

Derivatives / Perps

Adversaries, ranked: oracle manipulator (leverage amplifies oracle error — 1% manipulation on 50x is a 50% PnL swing) → liquidation MEV searcher → funding rate manipulator → position size attacker (positions larger than the protocol can pay out) → compromised admin (max leverage, funding parameters, liquidation thresholds, oracle, pause liquidations).

Dominant patterns: oracle manipulation triggering cascade liquidation. Funding rate manipulation via concentrated one-sided open interest. Position size exceeding payout capacity. Stale oracle enabling a risk-free directional bet against offchain price. Cross-margin cascades within one account. ADL manipulation.

Critical invariants: sum of all PnL is zero minus fees. Available liquidity covers maximum payout under worst-case price movement. Liquidation triggers before any position causes bad debt. Funding rate converges open interest imbalance. Mark price cannot deviate from index price beyond safety bounds.

Look first at: PnL math at leverage limits and in both directions; the margin between liquidation trigger and insolvency; how mark price is derived and whether it moves within a block; whether open interest and position size limits are enforced; the maximum funding rate and how fast it can drain margin.

Liquid Staking

Adversaries, ranked: exchange rate manipulator → validator set attacker → withdrawal queue attacker → oracle/rate arbitrageur (exit at stale rate before a slashing report lands) → compromised admin (validator set, fees, oracle, pause withdrawals).

Dominant patterns: rewards or slashing reporting manipulation. Withdrawal queue griefing with spam requests. Rebasing integration bugs in downstream protocols. Validator collusion suppressing rewards. Share price manipulation via direct transfer to the contract.

Critical invariants: exchange rate reflects true underlying value (staked plus rewards minus slashing). Total derivative supply times exchange rate is at most total underlying staked. The withdrawal queue processes in fair order. Slashing is reflected in the rate before any user can exit at the stale rate.

Look first at: who reports rewards and slashing, how often, and whether it is manipulable; the withdrawal queue delay and griefability; who selects validators; whether the derivative rebases or uses shares; how a massive slashing event is socialized.

Bridge

Adversaries, ranked: validator/relayer set attacker (the single largest bridge exploit vector by value lost) → message replay attacker → race condition exploiter (source/destination finality gaps, reorgs) → fake message crafter → compromised admin (validator set, pause, upgrade to drain locked funds).

Dominant patterns: validator key compromise forging messages to mint unbacked tokens. Message replay from a missing or overflowing nonce. Proof verification bypass. Chain ID confusion. Reorg exploitation after destination minting.

Critical invariants: locked tokens on source equal minted tokens on destination. Every message is processed exactly once. Messages cannot be forged without validator threshold consensus. Accounting is consistent across chains.

Look first at: validator count, threshold, and how the set changes; nonce presence, checking, and overflow; proof and signature verification edge cases; finality assumptions on the source chain; whether admin can drain locked funds.

Governance

Adversaries, ranked: flash loan governance attacker (trivial when voting power reads current balance instead of a snapshot) → governance capture attacker (patient accumulation) → proposal spam / griefing attacker → timelock exploitation attacker → compromised guardian (cancel, pause, emergency bypass).

Dominant patterns: flash loan → vote → return. Bribe attacks. Proposal obfuscation hiding malicious calldata. Timelock front-running to position before parameter changes execute. Guardian emergency powers used for non-emergencies.

Critical invariants: voting power is snapshotted at proposal creation. Quorum prevents minority capture. Timelock delay is long enough for users to exit. No single role bypasses governance for non-emergency actions. Proposal calldata matches its description.

Look first at: whether voting power is a snapshot or a current balance; quorum and threshold against actual token distribution; timelock duration; every parameter governance controls; who holds emergency powers and what they can do.

Cross-Cutting Threats (apply to every protocol)

Temporal Threat Phases

Include a "Temporal Risk Profile" subsection covering only the phases that add NEW information beyond Actors, Attack Surfaces, and Upgrade Architecture. Skip Steady State — the main threat model covers it. One to three bullets per phase, each citing a code location and a mitigation status (mitigated / partially mitigated / unmitigated).

Deployment & Initialization — the most dangerous 24-48 hours.

Market Stress — where the largest DeFi losses have come from.

Governance & Upgrade Windows — the transition between old and new state.

Deprecation & Wind-down — include only with version-transition evidence.

Composability & Dependency Analysis

Every external call extracted in Step 2 gets classified into the composability taxonomy. For each call determine:

1. Target type — oracle, DEX/AMM, lending pool, yield protocol, token, governance, bridge, other
2. Assumptions about the return value — correct price, exact token amount, success, specific format
3. Validation present — bounds check, staleness check, zero check, success check
4. Mutability of external behavior — can it change without this protocol's consent (upgradeable proxy, governed parameters)?
5. Fallback on failure — revert, silent failure, fallback value, try/catch that fails open

Report each significant dependency as a blockquote block:

Chainlink ETH/USD — via Oracle.getPrice()

• Assumes: fresh, positive, 8-decimal price
• Validates: answeredInRound only — NO staleness or deviation check
• Mutability: feed address settable by admin, no timelock
• On failure: reverts

Layer 1 — direct dependency risks. Oracle dependency chains (protocol → oracle → underlying sources; if any source is manipulable within the trust assumptions, the oracle is manipulable). Yield strategy dependencies (the external protocol holds the actual funds; check upgradeability, pausability, emergency withdrawal, loss socialization, retained approvals after migration). Callback reentrancy (guards that are per-function do not stop cross-function reentrancy; ERC-777 tokensReceived, ERC-1155 onERC1155Received, flash loan callbacks, swap callbacks).

Token behavior assumptions. Report only the ones the code does not validate.

Check whether the code uses the balanceOf before/after pattern (handles fee-on-transfer), uses SafeERC20 (handles non-reverting tokens), reads decimals() dynamically, handles rebasing, and whether arbitrary tokens can be used or a whitelist exists.

Layer 2 — shared state risks. Liquidity coupling (two protocols using the same pool; a large action here moves prices there within a block). Oracle sharing (the same feed triggering correlated liquidations, with feedback loops back into this protocol). Approval chain exposure (unlimited approvals to an upgradeable contract mean a future upgrade could drain them; deprecated contracts still holding approvals).

Layer 3 — temporal composability risks. Governance-induced behavior change in a dependency (no contract interaction changed, but economic assumptions broke — for example a lending market lowering a collateral factor under a strategy assuming the old one). Upgrade-induced interface change (same signature, different behavior, revert conditions, or gas). Deprecation without notification (a feed returns stale data silently, or starts reverting into a fail-open try/catch). Dependency-of-dependency upgrades — map the chain two to three levels deep and flag chains deeper than two levels, noting for each level whether it is upgradeable and governed.

Step 5: Invariant Synthesis

Invariants are properties that must hold across ALL state transitions. This step is a reasoning pass over the Step 2 extractions — delta writes, guard predicates, transitions, invariant comments. It needs no new tool calls except the batched write-site Greps in the guard-lift pass.

The output is invariants.md, a catalog of blocks with stable IDs that x-ray.md cross-links into.

Terminology: Guards Are Not Invariants

A guard is a per-call precondition enforced at a single callsite — require(amount >= MIN). It is not falsifiable: the code guarantees it at that callsite. It feeds §1 of invariants.md (Enforced Guards reference) only.

An invariant is a property that must hold globally across any sequence of calls — "every active position is at least MIN". Invariants that are lifted from guards, or stated in NatSpec, feed §2/§3/§4.

ID Scheme

IDs are stable within a run and are written as #### G-1, #### I-17, #### X-4 H4 headings — never as table rows. H4 headings produce slug anchors (#g-1, #i-17) that cross-file markdown links resolve reliably in VS Code and on GitHub. Inline <a id> anchors inside table cells do NOT work cross-file, which is why referenced IDs must never live in tables.

NatSpec Routing (run before the structural walk)

For each NatSpec @invariant tag or inline comment asserting a global property — "totalSupply always equals Σ balances", "fee never exceeds MAX_BP", "only one active epoch at a time" — route DIRECTLY to §2, or §3/§4 if the property spans contracts or derives from multiple primitives, classified by shape. Source tag: NatSpec: Contract.sol:LN. Do NOT place developer-stated global invariants in §1 — §1 is per-call guards only.

Doc-stated global invariants from Step 1's spec extraction route the same way.

After routing, still run the structural scans. They confirm (Onchain: Yes) or contradict (Onchain: No) the stated claim.