A subtraction that would have bricked every call before the start date — caught before the Solidity existed

The brief

A revocable, single-token (ERC-20) vesting vault:

• A project funds the vault and creates cliff + linear release schedules for multiple beneficiaries.
• Beneficiaries claim vested-but-unclaimed tokens over time.
• The project (a multisig) can revoke a beneficiary's unvested tokens — vested tokens stay with the beneficiary; unvested return to the project.
• Emergency pause halts both claim and revoke.
• Immutable, solc ^0.8.24, OZ v5.x. Two trust boundaries: a privileged owner and untrusted beneficiaries. Hardened against non-standard ERC-20s — fee-on-transfer, missing return values, ERC-777 reentrancy callbacks. Rebasing tokens are explicitly out of support, not hardened against — a negative rebase breaks the conservation invariant and can't be fixed at the contract layer, so it's carried as a deployment caution instead.

Money-custody, irreversible, adversarial users on one side and a privileged multisig on the other. Exactly where a thirty-second answer costs real money.

The setup: reviewers who only see the artifact

The design ran through a five-stage loop. The part that matters isn't the stage count — it's that each stage is a separate reviewer that sees only the artifacts, not the reasoning that produced them. You can't rationalize a design to someone who never heard your rationalization.

1. Intake → a structured brief: actors, trust boundaries, value flows, failure modes.
2. Contract modeling → storage layout, asset-conservation invariants, the time-based state machine.
3. Interface design → function signatures, revert conditions, events, checks-effects-interactions annotated per function.
4. Security architecture → threat model + the implementation spec.
5. A deterministic gate (structural red-lines), then an independent adversarial reviewer whose only job is to break the design.

It did not pass on the first try. First review came back REVISE — three Major findings. That's the system working; a first-pass PASS on a value-custody contract would make me more nervous, not less.

The catch: a checked-underflow hiding in correct-looking math

The linear-release formula was mathematically fine. The finding was about the gap between correct pseudocode and the naive way someone — an AI code generator or a tired human — actually implements it.

Under solc ^0.8, arithmetic is checked by default: an unsigned subtraction that goes negative doesn't wrap, it reverts. Now watch what happens if the implementer computes the elapsed term before guarding the branch:

Illustration — the trap

// ILLUSTRATION of the trap — not the delivered design; a minimal repro of the pattern.
// solc ^0.8.x: arithmetic is checked, so underflow reverts.
function vested(uint256 funded, uint64 start, uint64 cliff, uint64 duration, uint64 t)
    public pure returns (uint256)
{
    uint256 elapsed = t - start;                 // <-- reverts when t < start
    if (t < start + cliff)   return 0;           // too late — never reached for t < start
    if (t >= start + duration) return funded;
    return funded * elapsed / duration;
}

Fund a schedule whose start is next Monday. Until Monday, t < start, so t - start underflows and the entire call reverts — and because the return 0 branch sits after the subtraction, it never gets the chance to run. Until the start date arrives, every vested(...) view reverts, and every revoke, which reads the same math, reverts with it. The vault looks bricked until its start date passes — for the most ordinary reason there is: you scheduled vesting ahead of time.

The subtle part — and the reason this is a spec bug, not just a coding slip — is that the pseudocode's branch order was already correct. What the spec never did was warn that the subtraction must only be evaluated once its branch guard holds. So the reviewer's fix wasn't "reorder the branches"; it was to write the constraint into the spec as a hard rule, and add the boundary acceptance tests that would have caught a reordering:

Illustration — the fix

// FIXED: the subtraction lives only inside the branch where it's valid.
function vestedFixed(uint256 funded, uint64 start, uint64 cliff, uint64 duration, uint64 t)
    public pure returns (uint256)
{
    if (t < start + cliff)     return 0;         // also covers t < start → 0, no underflow
    if (t >= start + duration) return funded;
    return funded * (t - start) / duration;      // here t >= start+cliff >= start, always safe
}

Plus acceptance tests pinning the boundary on the delivered (id-based) function: vested(id, start - 1) == 0 and vested(id, 0) == 0 — return zero, do not revert. That the return below start had been left undefined in the first place — zero, or revert? — with nothing testing it was itself the third of the three Major findings: the acceptance-side of this same underflow. A spec that says "the math is funded * (t - start) / duration" is not done. A spec that says "…and t - start must never be evaluated before its guard, and here's the test that fails if you do" is.

The part I'm prouder of: the review cleared a bug it couldn't find

Finding bugs is the easy half. The tell of a real adversarial review is whether it will chase a suspicion, fail to land it, and then honestly report the miss instead of dressing it up as a finding to pad the report.

The most suspicious thing in this design was the revoke accounting: when the owner revokes, does the beneficiary's already-vested entitlement stay exactly consistent with what's been claimed, or can the two drift and let someone over-withdraw? The reviewer traced it block by block: revoke refunds funded − vested(now); the post-revoke effective cap is vested(revokedAt); because vested is monotonic non-decreasing in time and revokedAt is at least as late as any prior claim, vested(revokedAt) ≥ released always holds — so the claim delta can't underflow, the conservation invariant can't drift, and there's no path to over-withdraw.

Conclusion: attack failed, design correct — logged as evidence, explicitly not as a finding.

That paragraph is worth more to me than the three findings, because it's the one that tells you the review is trying to break things, not trying to look busy.

I don't trust my own gates either

Stage 5 has a deterministic gate — a structural checker that enforces a handful of design red-lines (value-custody functions must declare their security intent, state-changing functions must carry access control, and so on). When I built that gate, it passed 44 green tests.

Then I did to the gate what I do to the designs: handed it to an independent adversarial review whose only job was to break it. It found the gate failing open. The checker routed each function to a check by its declared security-intent tag — and if that tag was missing, empty, or merely misspelled, the lookup found nothing and the function was silently skipped. A state-changing, value-moving function tagged value_transfer — underscore instead of the expected value-transfer — sailed straight past the floor:

Illustration — fail-open, before

# ILLUSTRATION of the fail-open pattern (simplified). BEFORE — unknown intent → skip, not block.
check = INTENT_CHECKS.get(fn.security_intent)   # misspelled/missing tag → None
if check:                                       # None is falsy → silently skipped
    check(fn)

Illustration — fail-closed, after

# AFTER — fail CLOSED: an intent it can't classify blocks, instead of slipping through.
check = INTENT_CHECKS.get(fn.security_intent)
if check is None:
    raise GateBlock(f"unclassifiable security_intent: {fn.security_intent!r}")
check(fn)

Forty-four passing tests said the gate was fine. It wasn't. A green test suite only proves the cases you thought of; it says nothing about the ones you didn't — and "an attacker feeds you a tag you didn't enumerate" is precisely a case you didn't think of. I changed the gate to block on anything it can't classify rather than skip it, and the suite went from 44 to 51 tests.

If I hold my own tooling to "must survive an independent adversary whose only job is to break it — and get fixed when it doesn't," that's the standard your code gets too.

What this is — and, honestly, isn't

I think the transparency is the product, so here's the scope drawn tightly:

I'd rather tell you precisely what this is than oversell it and get caught in due diligence — which is, not coincidentally, the same instinct that catches the underflow.

Verify what's verifiable

You don't have to take the narrative on trust:

• The underflow is a general Solidity fact, not a claim about my code. Drop both Solidity illustrations into one contract in Remix (under pragma solidity ^0.8.24;), call the naive vested(...) with t < start and watch it revert; call vestedFixed(...) and watch it return 0. The trap is real and language-level.
• The fail-open lesson reproduces from the snippet above — a dictionary-lookup dispatch that treats "unknown key" as "nothing to check" fails open for any checker, not just mine. If your security tooling dispatches this way, go look at it today.
• The design-review artifacts are real and I'll walk you through them — the iter-0 review with the three Major findings, the revised spec, the boundary acceptance tests, and the gate's 44→51 test delta — on request.