What 6 Layers of Analysis Reveal That Static Tools Miss

TL;DR

• The bug Slither missed: ProgressiveCurve._convertToAssets in Intuition Protocol reverts with arithmetic underflow for any vault where totalShares ∈ [minShare+1, 1e9-1]. A correct redemption becomes a permanent DoS. Static tools see nothing because every line is individually well-typed.
• The methodology that caught it: a 6-layer audit pipeline — static → semantic → composability → invariant → economic → red-team — mapped to DMAIC phases (DEFINE / MEASURE / ANALYZE / IMPROVE / CONTROL) with an 11-of-16 BFT quorum on root cause.
• Reproduce it: check out Intuition commit 20181c16…2369212c9, run the one-file Foundry exploit, watch Alice's redemption revert for a numerically valid share count.
• The real claim: static tools give you coverage illusion. Six-layer coverage gives you behavior under adversarial input. They are not substitutes.
• Honest receipt: this is a Medium-severity finding. It is not a $2M drain. We will not inflate it to sell you the methodology.

What this post is (and is not)

Most smart-contract security blogs fall into two genres: the post-mortem of a catastrophic exploit already in the news, or a tooling pitch dressed up as methodology. This is neither.

This is the walkthrough of a completeness bug that we filed as a Medium-severity finding against Intuition Protocol's v2 contracts on 2026-03-27 (Matrix CR Studio Build 63). It is not glamorous. Nobody lost $2M. The protocol's test suite passes, Slither prints a green banner, Aderyn shrugs. And yet: deposit slightly above the minimum, try to redeem, and your funds lock — not because the logic is wrong in intent, but because a rounding asymmetry between square() and squareUp() produces sub(0, 1) which panics in Solidity 0.8.

This post explains the 6-layer pipeline that surfaces this class of bug, shows exactly where each layer contributes, and gives you a commit hash and a test command so you can run the exploit yourself. If at the end you think the methodology is overkill for what it found, that is a fair judgment and we would rather you reach it honestly than pretend otherwise.

The single-layer trap

There is a story that every security team tells itself about tooling:

We run Slither. We run Aderyn. We run Mythril on the critical contracts. We have invariant tests. We have 85% line coverage. When the CI passes, we ship.

This story is true in the way a weather forecast is true — useful for planning, catastrophic as a certainty. Static analyzers operate on the AST, a small set of heuristic patterns, and a handful of well-known taxonomies (reentrancy, tx.origin, unchecked returns, delegatecall footguns). They do not reason about invariants across library boundaries. They do not model economic incentives. They do not understand that a function that is locally sound can be globally broken by the shape of its caller's state.

Here is the bug we caught. Look at it for ten seconds and tell me what's wrong:

function _convertToAssets(
    uint256 shares,
    uint256 totalShares,
    uint256 totalAssets
) internal view returns (uint256 assets) {
    _checkCurveDomains(totalAssets, totalShares, MAX_ASSETS, MAX_SHARES);
    _checkRedeem(shares, totalShares);

    UD60x18 s     = wrap(totalShares);
    UD60x18 sNext = sub(s, wrap(shares));

    UD60x18 area = sub(PCMath.square(s), (PCMath.squareUp(sNext)));
    UD60x18 assetsUD = mul(area, HALF_SLOPE);
    assets = unwrap(assetsUD);
}

Clean. Guarded. Uses a reputable fixed-point library (prb-math). The _checkCurveDomains and _checkRedeem both run before the arithmetic. Every single variable is correctly typed as a UD60x18 unsigned 18-decimal fixed-point value. Slither has nothing to flag here. Aderyn has nothing to flag here. If you asked Claude Sonnet 4.5 to audit this function in isolation, it would tell you it looks fine.

It isn't fine. And the reason it isn't fine cannot be found by looking at this function alone.

The 6 layers, and what each one actually does

Matrix CR Studio's audit pipeline is six sequential layers, each with a different question and a different failure mode. If any layer surfaces a finding, it moves to the next layer for confirmation; if all six agree, the finding ships. The pipeline lives in src/auditor.py and src/pipeline.py; the post-find review lives in The Construct. DMAIC governs the state machine.

Layer 1 — Static (DMAIC: DEFINE)

What it does: runs Slither, Mythril, Aderyn, and a custom pattern-grep over the AST. Flags known taxonomies (reentrancy, tx.origin, unchecked low-level calls, storage collisions, locked-ether, shadowed state variables, floating pragma, etc.).

What it caught on Intuition: nothing relevant to our bug. It did correctly flag a floating pragma and a few unlabeled SPDX headers — cosmetic.

What it cannot catch: any bug whose trigger requires specific values of totalShares not represented in the analyzer's taint or abstract-interpretation model. A pure-arithmetic underflow that only occurs in the range [1_000_001, 999_999_999] is outside the symbolic range most tools explore, because the tools don't know that range is production-reachable.

The right way to think about Layer 1 is: it tells you if the grammar is sane. It does not tell you if the semantics hold under adversarial state.

Layer 2 — Semantic (DMAIC: DEFINE)

What it does: asks a reasoning model — we use Claude Sonnet 4.5 routed via src/llm_router.py — to compare the function's name, NatSpec, calling conventions, and published protocol documentation against its actual implementation. The question is literally: does this code do what it says on the tin?

Implementation: _run_llm_audit in src/auditor.py feeds the contract source plus a system prompt encoding the DMAIC checklist, and collects a structured JSON of {severity, category, confidence, suspected_invariant}.

What it caught on Intuition: the LLM layer flagged _convertToAssets with a note roughly translated as: the README of this protocol explicitly claims PR #136 fixed "must not revert in low-share edge cases where result should be zero", but the implementation uses an asymmetric rounding pair that can produce sub(squareDown, squareUp) < 0 without a zero-floor guard. The intent and the implementation diverge.

That is the first signal something is wrong. It is not enough to ship a finding — LLMs are confidently wrong often enough that a single-layer claim is noise. It gets Layer 2 to Layer 3.

Layer 3 — Composability (DMAIC: MEASURE)

What it does: walks every reachable call path from external-facing functions into the suspect function, mapping which storage slots and calldata parameters the arguments can take. Uses the AST plus foundry's forge inspect to build a call graph.

What it caught on Intuition: _convertToAssets(shares, totalShares, totalAssets) is reachable from redeem(), which is reachable from any external caller with vault shares. The totalShares parameter is bounded below by minShare (an AtomCurveRegistry storage variable) — and critically, minShare is set to 1e6 (one million) in production, while the underflow condition requires totalShares < 1e9 (one billion). The production-reachable range is therefore [1_000_001, 999_999_999] — three orders of magnitude of perfectly valid share counts that revert.

This is the layer that converts "the LLM is suspicious" into "the bug exists in practice." It is also where static tools are architecturally blind — Slither does not reach across storage-state inference into another contract's registry to infer the effective range.

Layer 4 — Invariant + Fuzz (DMAIC: MEASURE)

What it does: generates a Foundry invariant test and an Echidna harness. The invariant is: for any (shares, totalShares) ∈ reachable_state, _convertToAssets must not revert with stdError.arithmeticError. Auto-generated by _generate_fuzz_tests in auditor.py, seeded with the reachable range discovered in Layer 3.

What it caught on Intuition: with a hand-crafted seed that biases totalShares into the [1e6, 1e9] range, the invariant fails on the first execution. Without that seed, Foundry's default fuzzer generates values uniformly across [0, 2²⁵⁶-1], and the probability of landing in [1e6, 1e9] is ~5e-69. This is the critical moment: pure fuzzing without Layer 3's range hint would never find this bug in human timescales.

This is the difference between running forge test and running a directed audit. The difference isn't the tool — it's the prior knowledge of which states are production-reachable.

Layer 5 — Economic (DMAIC: ANALYZE)

What it does: models the cost to exploit and the reward. This is where we draw on the Bounty Verification Protocol (Build 106) — a 7-gate pre-submission pipeline with an economic-modeling gate that checks dust griefing, MEV extractability, and attack cost vs damage.

What it concluded on Intuition: this is a DoS, not a theft. An attacker cannot extract funds — they can only lock a victim's funds. The attack cost is approximately one Alice-deposit sized to [minShare+1, minShare+n] into a fresh atom vault. The reward is that any subsequent redeemer in that share range gets their tx reverted. It is a griefing attack with asymmetric cost (attacker pays one deposit, victims pay gas for reverting redeem attempts until they realize their funds are locked).

Severity classification outcome: Medium. Protocol funds are not at risk; user funds are recoverable by admin action or vault migration; the DoS is protocol-wide for affected vaults, which is non-trivial but not catastrophic. We shipped it as Medium. If we had tried to inflate it to High, Gate 3 of BVP would have flagged the inflation — and as we learned the hard way on 2026-04-17 with a LayerZero finding that a reviewer (pfapostol) correctly invalidated for a similar runtime-model error, inflating severity is a reputation tax you pay once and remember for years.

Layer 6 — Red Team BFT (DMAIC: IMPROVE)

What it does: runs the finding past The Construct's bounty_review panel — 8 personas including ex_nsa_tao, precision_mechanical, pure_mathematician, taleb_antifragility, boyd_ooda, kahneman_behavioral, kpmg_forensic_auditor, ex_fbi_white_collar. Each casts a vote with structured feedback. An 11-of-16 BFT-style quorum (HotStuff lineage, src/dmaic.py:81) is required before the finding ships.

What it did on Intuition: the panel agreed unanimously that the bug was real and correctly classified as Medium. taleb_antifragility added the observation that the README's PR #136 reference was a claimed fix that left the guard off — which escalates it from "bug" to "bug whose fix was publicly announced but incomplete". That framing made it into the submitted report.

The panel also flagged the Bridge Fee Mismatch (our second Intuition finding) during the same pass — boyd_ooda noticed that bridgeTrust() uses amountOut correctly while swapAndBridgeWithETH uses minTrustOut, so the divergence is a pair of sibling functions where one is right and one is wrong. That kind of pattern-by-asymmetry is a classic human-review catch that no static tool sees.

SATOR ceremony (DMAIC: CONTROL)

What it does: SHA-256 stamps the finding, binds it to a git commit hash, generates a SATOR HMAC over the finding body + timestamp, and archives both to data/bounty_verifier.db. This is Gate 7 of BVP. No bounty submission ships without it.

This is also the moment we split the finding into: (a) the public report we submit to the bounty program, (b) the internal IP claim we register in docs/IP_CLAIMS.md, and (c) the reproducible artifact we publish on this blog.

The full Intuition finding, walked through the layers

Here is what actually happened on 2026-03-27 when we ran the Intuition v2 contracts (commit 20181c16…2369212c9, fetched from their public intuition-contracts-v2 repo) through the pipeline.

The bug, stated precisely

In src/protocol/curves/ProgressiveCurve.sol:243 and OffsetProgressiveCurve.sol:250:

UD60x18 area = sub(PCMath.square(s), (PCMath.squareUp(sNext)));

The asymmetry that kills it:

• PCMath.square(s) rounds down: floor(s² / 1e18)
• PCMath.squareUp(sNext) rounds up: ceil(sNext² / 1e18)

When totalShares < 1e9 (in raw 18-decimal units):

• square(s) = floor(s² / 1e18) = 0 — because s² < 1e18
• squareUp(sNext) = ceil(sNext² / 1e18) = 1 — because any non-zero sNext rounds up from zero
• sub(0, 1) → arithmetic underflow panic in Solidity 0.8

The README of intuition-contracts-v2 explicitly states PR #136 fixed the invariant "must not revert in low-share edge cases where result should be zero". The fix is incomplete — no zero-floor guard exists before the sub().

Reproduce it yourself

If you have a Foundry environment, this takes under five minutes:

# 1. Check out the exact Intuition commit
git clone https://github.com/0xIntuition/intuition-contracts-v2
cd intuition-contracts-v2
git checkout 20181c162502da226ca25c31aef47872369212c9

# 2. Drop in the PoC (source available from Matrix CR Studio on request
#    — released only to verified bounty-program maintainers under NDA
#    post IP-breach)
cp /path/to/PoCCurveUnderflow.t.sol test/

# 3. Run
forge test --mc PoCCurveUnderflow -vvv

Toolchain anchor for reproducibility:

• Intuition commit: 20181c162502da226ca25c31aef47872369212c9
• Solidity: 0.8.29 (pragma locked in ProgressiveCurve.sol)
• Foundry: forge 0.2.0 (nightly 2026-03 lineage; any recent release reproduces the revert)
• prb-math: as pinned in Intuition's foundry.toml at that commit
• Our audit run: 2026-03-27, Matrix CR Studio Build 63, disclosed to the Intuition team the same day

Expected output: vm.expectRevert(stdError.arithmeticError) fires on redeem(1e6) after deposit to a vault with totalShares = 2e6. Alice's redemption reverts. Repeatedly. Forever, for any vault that lands in the affected share range.

Why the PoC is not public: prior to 2026-04-16, we would have linked the .t.sol directly in this post. After the public-repo IP breach that month — 3,145 clones by 945 unique visitors before we caught it — we have moved all exploit PoCs to request-only access. If you are a bounty-program maintainer or a researcher at a verifiable institution, email [email protected] and we will share the file with a legal acknowledgment. The architecture of the pipeline is public; the weaponized exploits are not.

The fix

Add a zero-floor guard:

UD60x18 sqS     = PCMath.square(s);
UD60x18 sqSNext = PCMath.squareUp(sNext);

// Guard: rounding asymmetry can cause squareUp(sNext) >= square(s) at low share counts.
// In that case the result is 0 (no assets out — correct for dust amounts).
if (unwrap(sqSNext) >= unwrap(sqS)) {
    return 0;
}

UD60x18 area     = sub(sqS, sqSNext);
UD60x18 assetsUD = mul(area, HALF_SLOPE);
assets = unwrap(assetsUD);

Apply the same pattern in OffsetProgressiveCurve._convertToAssets. The fix is eight lines including the comment.

The companion finding — bridge fee mismatch

The same audit pass surfaced a second Medium in TrustSwapAndBridgeRouter.sol (Intuition periphery repo). Functions swapAndBridgeWithETH and swapAndBridgeWithERC20 quote the bridge fee using minTrustOut but execute transferRemote with amountOut:

// fee quoted with the minimum:
uint256 bridgeFee = metaERC20Hub.quoteTransferRemote(
    recipientDomain, recipientAddress, minTrustOut
);
// ... swap happens, amountOut >= minTrustOut ...
// bridge called with the actual output:
transferId = _bridgeTrust(amountOut, recipientAddress, bridgeFee);

IMetaERC20Hub.quoteTransferRemote takes _amount as a parameter, confirming the fee is amount-dependent. Any time the swap executes above the minimum (which is every time if slippage protection is configured normally), the fee paid is insufficient and the bridge call reverts. The whole transaction reverts. User's swap-and-bridge intent fails.

bridgeTrust() (without the swap leg) gets it right — quotes and bridges the same amount. The two sibling functions are inconsistent. This is the kind of finding Layer 2 (LLM semantic diff) surfaces and Layer 6 (Boyd OODA pattern-asymmetry reasoning) confirms.

Both findings were delivered to the Intuition team with disclosure, reproducibility steps, and proposed fixes on 2026-03-27.

Why static tools cannot do this, even in principle

A charitable reading of Slither goes something like: "it's a static tool, of course it doesn't catch bugs that require runtime state to trigger." That is correct but insufficient.

The real limit is deeper. Static tools operate in the space of patterns. A pattern is a syntactic or abstract-syntactic shape that flags a suspicion — delegatecall without check-effects-interactions, tx.origin for authentication, unchecked return from a low-level call. Patterns are cheap, repeatable, and catch a huge swath of CVE-class bugs. They are also, by construction, unable to reason about invariants that require multi-step state transitions across library boundaries.

The Intuition bug requires you to:

1. Recognize that UD60x18 arithmetic has rounding modes.
2. Recognize that the two sibling operations (square, squareUp) round in opposite directions.
3. Recognize that under a specific range of input values, the asymmetric rounding produces an ordering (sqSNext > sqS) that a naive sub() does not handle.
4. Recognize that this range is not pathological — it is reachable in production because minShare = 1e6 and the affected range extends to 1e9.

Point 4 is the one no static tool does. Point 4 requires reading the protocol's configuration registry, inferring the production minShare value, and noticing it puts valid vault states in a range the arithmetic cannot safely handle. It is a reasoning task, not a pattern-match task.

What the 6-layer pipeline adds is a reasoning spine. Layers 1-4 are mechanical. Layers 5-6 are adversarial modeling. Together they cover both the syntactic surface and the adversarial depth.

Cost and time

Some honest numbers on what running this pipeline actually costs:

• Compute: 16 GB refurbished mini-PC (our house node, see the $0/month infrastructure post)
• LLM spend per full audit of a ~5 KLOC Solidity repo: roughly $4-8 in Anthropic API, using claude-sonnet-4-5 for Layers 2 and 6.
• Wall-clock time: 20-40 minutes for Layers 1-4 (automated), plus 10-20 minutes of human review for Layers 5-6. About one hour total for a focused repo.
• False positive rate: across our last 9 bounty engagements (Chainlink, Ambire, K2, LayerZero, GMX-Solana, Intuition, Midas, Renegade, Yo Protocol), the pipeline surfaced approximately 3× as many candidates as it shipped. Layer 5 and Layer 6 are the filters that bring the signal-to-noise back in line.
• Actual shipping rate: ~1-3 findings per repo, predominantly Medium with occasional High. We do not ship junk. The LayerZero April-17 incident — where pfapostol correctly invalidated a finding we submitted with the wrong runtime model — is the exact reason Gate 2 (runtime anchoring) exists in BVP. Never again.

The pipeline is not a silver bullet. It is a disciplined process. The value it produces is not "more findings" — it is fewer invalid findings and higher-quality valid ones.

On prior art

It would be dishonest to suggest the class of bug — asymmetric-rounding underflow in fixed-point Solidity libraries — is something we invented. Fixed-point arithmetic rounding quirks have been a known audit concern since at least the early PRBMath release notes (2021) and appear in Trail of Bits' and OpenZeppelin's public audit repositories for various AMM and curve protocols. What is novel about our finding is the specific composition — square(s) rounding down + squareUp(sNext) rounding up + a missing zero-floor guard + a production-reachable share range from minShare=1e6 to 1e9 — against a claimed-fixed PR (#136). The pattern-match tools have the ingredients; they do not have the composition.

We filed the finding with Intuition on the assumption that it was not already disclosed. If a reviewer tells us there is a prior disclosure we missed, we will credit it here. Corrections are welcome.

What this methodology will not do

• It will not replace a human auditor who has spent five years in Solidity. The pipeline accelerates that auditor. It does not substitute for them.
• It will not find bugs that require cryptographic reasoning outside the 6-layer scope (novel elliptic curve attacks, pairing-based proof soundness, ZK circuit completeness). We flag those and route to specialists.
• It will not make your incremental forge test obsolete. If anything it makes incremental testing more valuable because Layer 4 tells you which invariants your test suite should encode.

What happens next

Two things.

First, we are filing the first formal CVE for this class of bug in fixed-point arithmetic fixed-point Solidity libraries — the rounding-asymmetry completeness bug. Intuition is patient zero, but this pattern is almost certainly present in other UD60x18-using protocols that compute area = sub(square, squareUp) without a zero-floor guard. When the CVE is issued, we will update this post with the identifier.

Second, the post after this one — "Why Your PQC Migration Timeline Is Wrong" — shifts from smart contracts to the other half of our work: post-quantum cryptography. We will walk through two independent runs of an E8 root lattice Quantum Phase Estimation circuit on ibm_fez (IBM's 156-qubit superconducting backend) that produced a distinct α=1/137 eigenphase peak at n_precision=7. Those measurements tighten the Q-Day bound below what NIST and major cloud providers are planning around.

If your protocol uses fixed-point arithmetic and you would like us to run the pipeline over it — Medium-sized repo, 48-72 hour turnaround, flat-fee scope quoted in advance — [email protected]. If you'd prefer to run it yourself and want the auditor.py module as a standalone tool, we're drafting a licensable commercial release (not open source; see the IP-breach disclosure).

Slither, Aderyn, and Mythril are good tools. Six layers is a pipeline. They're not the same thing, and you should probably be running both.

Pipeline implementation: src/auditor.py (ABBAAuditEngine) + src/pipeline.py (DMAIC state machine) + src/bounty_verifier.py (BVP) + src/construct.py (panels) · Handle on Code4rena: LoneRam · Tracked engagements: 9 in contracts/bounties/ · Verification: all findings are SATOR-stamped and recorded in data/bounty_verifier.db with SHA-256 commit anchors.