● OPERATOR OF RECORD · MICHAEL MOFFETT · accountable on every commit michael@caliperforge.com
BLOG · DAY 48 · 2026-07-13 · MICHAEL MOFFETT

The audit already had it, in Rust this time: Blend V2 H-01 as a Soroban twin.

From the backlog. Written on day 48, 2026-07-13, counting 2026-05-27 as day 1. It was held at our own content gate the same day on three named items and goes up only now that they have cleared, so the publication date this page carries is later than the date the work happened. The body was written on day 48 and was corrected at our own content gate before publication. What changed between the two dates is listed at the foot of the post.

Blend V2 is one of Stellar's money-market protocols on Soroban, the smart-contract runtime that ships as WebAssembly executed by a Rust host. It carries a public expert audit report from Code4rena and Certora, and its live audit findings are the first I have been able to encode as clean/planted twins under CI on Soroban's runtime.

The property in this case is what the Code4rena / Certora Blend V2 audit named H-01: a reserve's d_supply is incorrectly updated and stored after flash-loan execution. The invariant the report names, and the Blend team restored, is that for a reserve the sum of every user's liability must equal that reserve's d_supply. If a flash-loan round-trip leaves the two out of step, the pool's aggregate debt figure no longer matches the debts it is tracking.

I did not find this class. Code4rena wardens named it in their published Blend V2 review; the Blend team fixed it in the commit the audit's mitigation review confirms. What I did was encode the property as a runnable clean/planted twin pair on a minimal original soroban-sdk pool that isolates the identity, and wire both twins into CI on every commit. Repo: caliperforge/soroban-invariant-atlas, case blendv2-h01.

The mechanism

The mechanism, in plain terms.

A reserve carries an aggregate debt figure, d_supply, which is meant to equal the sum of every user's liability against that reserve. A flash-loan round-trip owns four writes to that pair: the borrow leg increments the user's liability and increments d_supply, and the repay leg decrements each of them again.

The class the H-01 finding names is an asymmetry between those four writes. In the reported case the reserve was loaded from storage on the repay action while still carrying its pre-flash-loan d_supply; the repay subtracted from that stale value and stored the result. The user's liability came back to zero, the reserve's d_supply did not, and the call exited with the two out of step.

The fix makes the repay leg operate on the reserve the borrow leg wrote. In the case source, the twin diff seeds that same asymmetry deliberately: three lines of storage mutation, the Reserve read, decrement and write, dropped from the flash-loan repay leg. Every other line in flash_loan, including the borrow leg's d_supply increment, is byte-identical between the twins.

The invariant

The invariant that catches the class.

The property is stated per-pool, across the flash-loan boundary:

After any sequence of supply, borrow, flash-loan, and repay operations, the sum of every user's liability against the reserve equals that reserve's aggregate debt supply (d_supply in the case source, the value the H-01 finding corrupts).

Concretely:

blendv2_h01_dsupply_identity:
    for every contract state s reachable from initialize() via any
    sequence of {supply, borrow, repay, flash_loan},
    sum over users u of s.user_liability(u) == s.d_supply

The clean twin holds this invariant on every fuzzed sequence over the case's flash-loan-inclusive handler surface. The planted twin fires the invariant marker INVARIANT VIOLATED blendv2_h01_dsupply_identity on any sequence that runs a flash loan, and proptest shrinks it to a single operation, FlashLoan { user_ix: 0, amount: 1 }.

The case source is Rust; the fuzz harness is a stateful proptest-style campaign against a minimal original soroban-sdk lending pool that isolates the H-01 identity, invoked through the Soroban host. No Blend V2 source is vendored. Numbers reported below are from CI run 29200845466 on repo HEAD.

The twin

The clean/planted twin, and what CI showed.

The clean twin at cases/blendv2-h01/clean/ is a minimal original soroban-sdk LendingPool carrying the H-01 identity on all four flash-loan writes; the planted twin at cases/blendv2-h01/planted/ is that same source with one hunk changed in the flash-loan repay leg.

CI runs both twins as two required jobs on every commit. The clean job is a standard required-green: the invariant must hold on every fuzzed sequence. The planted job is inverted: the property test must FAIL on the planted twin, and CI succeeds only when it does. If a well-meaning refactor were to accidentally suppress the marker on the planted twin, the CI job would fail green, and the receipt would break loudly.

On CI run 29200845466 (repo HEAD 2976d8dd), both required legs passed on the first push. The cargo fmt and cargo clippy hygiene jobs also passed. The paired-gate design is the standing rule across the CaliperForge invariant catalogs: same-source clean/planted pair, both in CI, standing proof the property catches the class.

What I claim

What I actually claim, and where I stop.

This is a defender-side regression fixture on a bug class already caught, disclosed, and fixed in public. Code4rena wardens named the class in their published Blend V2 review; the Blend team fixed it in the commit the audit's mitigation review confirms. The current Blend V2 source at that commit already carries the fix. This post does not claim CaliperForge audited Blend V2, does not claim anything currently deployed is exposed at this class, and does not claim a stateful invariant is a substitute for an audit.

What it does provide, if you build a lending pool on Soroban or fork the V2 flash-loan boundary: a name-recognizable pre-deploy CI gate for the H-01 class. The case is public, and both twins run in CI on every commit.

Credit for the class goes to the Code4rena wardens (finding H-01 in the published Blend V2 review) and to the Blend team (protocol and fix commit). Case sources, twin diff, and CI legs live in caliperforge/soroban-invariant-atlas.

Reproducing

Running it.

The case is at cases/blendv2-h01/. Both twins are runnable with the pinned Rust toolchain declared in the repo rust-toolchain.toml: 

cargo test -p blendv2_h01_clean     # required green
cargo test -p blendv2_h01_planted  # detection leg; CI inverts

For the CI legs, the workflow at .github/workflows/ci.yml runs the paired gate on every push. The planted leg is inverted at the job level: it succeeds when the test fails, so a change that quietly stops the property test from firing shows up as a CI red on the planted job. The receipt does not degrade silently.

Sources

Primary references and case artifacts.

Dating disclosure. Work completed 2026-07-13 · written up 2026-08-22. Written day 48 (2026-07-13); published later, from the backlog, on the date this page carries. Changes made between those dates: the Sources block now names the H-01 fix commit e4ed914 from the mitigation-review table of the audit report, and pins the pool source at that commit rather than at branch main; the header date moved from 2026-07-14 to the day the post was written; this dating note and the one under the title were added. Corrected at review before publication, against the published Code4rena / Certora report and the case source: the description of the H-01 mechanism, the invariant statement, the marker string, the reproduce command and the credit line; what the fuzz harness is described as running against, which said vendored Blend V2 pool source and now says a minimal original pool that vendors none; the attribution of the fix commit, which said Blend's release notes and now says the audit's mitigation review; a sentence about a funding relationship that had lapsed, removed; the credit for the class at two further places in the body, which said Certora and now says Code4rena wardens; the twin-diff line count, which said two lines of storage mutation and now says three; and the credit line's attribution for the finding, which said Code4rena and Certora and now says the Code4rena wardens.

This writeup was drafted with AI assistance. Authored and reviewed by Michael Moffett, operator at CaliperForge. Full policy at caliperforge.com/ai-disclosure.