A Security Gate That Cannot Fail Is Ceremony

A gate is only as strong as the state its search can actually write. Everything else about it is decoration. A suite that spends a hundred thousand calls and a suite that spends a hundred are the same gate if neither can construct the state the property is about, and the expensive one just takes longer to tell you nothing. The badge does not carry that distinction, and neither does the budget.

Below is one reduced staking pool with one accounting defect in it. Three invariant campaigns run over it, same property, same budget, same seed, and the only thing that differs is what each campaign is able to construct. One goes red in four calls. The other two stay green, and one of those reports full marks on every coverage metric Foundry computes. The serious answer here is a coverage threshold enforced in CI, the path Foundry documents, and it catches the first green campaign cleanly. It does not catch the second. What that costs is a pipeline reporting full marks over a live defect, with nobody whose job it was to notice.

Draw the boundary first. This gate sits between a change and a merge inside one repository. It runs after the change exists, so it detects rather than prevents, and its whole value is producing a red that stops the merge. The deployed system and any audit engagement bought from outside sit on the far side of that line.

The campaign that could not have failed#

One pool, one property, and one search over it. The apparatus is small on purpose, so every number in it is checkable by hand. The pool mints shares against stake. A penalty burns stake and leaves the share count alone, so after a penalty every outstanding share is worth strictly less. Exit pays out against the share. No single exit pays more than the share was worth at the moment of the exit.

The pool below is a reduced specimen written for this article, and it stands in for a restaking accounting layer rather than reproducing one. It holds no ether and moves nothing of value. Three functions, twelve executable lines, one bug. Exit pays one unit of stake per share instead of pricing the share against the stake the pool still holds, so an exit after a penalty walks away with more than the share is worth.

Role: reduced executable model, the complete pool under test.

// SPDX-License-Identifier: MIT
pragma solidity 0.8.26;
 
/// A reduced restaking-style pool: shares are minted against stake, a penalty
/// burns stake without burning shares, and exit pays out against the share.
contract StakePool {
    uint256 public totalStake;
    uint256 public totalShares;
    mapping(address => uint256) public sharesOf;
 
    function delegate(address who, uint256 amount) external {
        uint256 minted = totalShares == 0 ? amount : (amount * totalShares) / totalStake;
        sharesOf[who] += minted;
        totalShares += minted;
        totalStake += amount;
    }
 
    /// A penalty burns stake and leaves the share count alone, so every share
    /// is worth strictly less afterwards.
    function slash(uint256 amount) external {
        totalStake -= amount;
    }
 
    /// The defect under test: exit pays one unit of stake per share instead of
    /// pricing the share against the stake the pool still holds.
    function undelegate(address who, uint256 shareAmount) external returns (uint256 paid) {
        paid = shareAmount;
        sharesOf[who] -= shareAmount;
        totalShares -= shareAmount;
        totalStake -= paid;
    }
}

Nothing points a campaign at that contract directly. An invariant campaign in Foundry points at a handler, and the handler is where the campaign's inputs get shaped into something the contract will accept. Foundry's own guide describes handlers as wrappers that constrain inputs and track state for the target contract. the Foundry invariant testing guide That is the right design. The argument is about what else the wrapper decides while it is busy constraining.

Over surface A the campaign ran 25,600 calls with zero reverts and reported the property as holding. Surface A exposes the delegate and the exit and nothing else. Two hundred and fifty six runs, a hundred calls deep, seed 0x1, the invariant evaluated after every call. Green.

That green was not luck and it was not a search that came up empty. On surface A no penalty is callable, so stake and shares move together on every path the campaign can build, and the share price never leaves one. The quantity the property asserts equals the quantity it is compared against on every step, which makes the assertion an arithmetic identity rather than a test. The campaign did not fail to find the defect. It could not have found it. A larger budget would have bought more instances of the same identity.

Everything needed to rebuild that run is on this page or one line away. The budget is runs = 256 and depth = 100 under [profile.default.invariant], fail_on_revert is true, and the seed is pinned at one everywhere. The verdict comes from forge test --match-contract GateSurfaceA --match-test invariant_NoSingleExitOverpays --fuzz-seed 1, the percentages from the same filters under forge coverage. The pool is above in full, so every denominator below is the tool's own. The three handlers differ by one selector and one four line guard, so rebuilding them is an afternoon.

The coverage threshold catches this one, and then stops#

The serious alternative is the coverage threshold, and it is a good rule. It is cheap. It is uniform across every pull request. It needs no per-property design and no reviewer in the loop, and it produces a number every engineer already knows how to read. On a young codebase it is the highest-yield rule available, because the thing it finds, a whole function no test ever enters, is common early and expensive. It is also the supported path, since forge coverage writes the LCOV tracefile a coverage service reads.

A coverage gate would have caught surface A and it deserves that credit, because the summary read 83.33% of lines, 90.00% of statements and 66.67% of functions. A function threshold set anywhere above two thirds goes red on that. One function in three was never entered, and the engineer who pushed gets a red build the same morning. That is the rule working on the failure mode it was built for.

What the summary will not do is say which function. That report is a two row table of percentages with no function name in it. Ask for the LCOV report instead of the summary and the same campaign names it, recording StakePool.slash at zero hits. That function is the penalty, the exact transition the property is about. The invocation is the one above with --report lcov in place of --report summary, and the file it writes carries a hit count for every function in the unit.

So the alternative wins a real round, and granting that is the only honest way into the next one. The question is what the same rule does when the thing the campaign never reached stops being a function. Foundry's coverage guide states that 100% line coverage does not necessarily mean every outcome was tested. the Foundry coverage guide The guide means branches inside conditionals. The gap here is one level wider than a branch.

The threshold itself lives somewhere else, which matters more than it sounds. The percentage is computed by one tool and enforced by a different one. Foundry generates the coverage data and does not enforce a minimum percentage, so the threshold lives in whatever service consumes the tracefile. the coverage guide on LCOV output Whoever set that number set it once, against a codebase that has since changed shape, and nothing in the pipeline asks whether it still corresponds to anything.

The callable surface is the gate#

Put the penalty on the callable surface and the property starts behaving like a test again. On surface B, the same pool and the same property under the same budget and the same seed, the campaign went red and shrank its counterexample from fifteen calls to four. Those four are a delegate, a penalty, a second delegate and an exit. Nothing about the property moved. Nothing about the pool moved. The handler grew one selector.

     one pool, one property, runs 256 depth 100, seed 0x1
     what moves is what the campaign is able to construct
 
  surface A                 surface B                 surface C
  the penalty is not        nothing is held back      the same three selectors,
  a callable selector                                 the ORDER bounded out
  +------------------+      +------------------+      +------------------+
  | delegate         |      | delegate         |      | delegate         |
  | undelegate       |      | slash            |      | slash            |
  |                  |      | undelegate       |      | undelegate       |
  +------------------+      +------------------+      +------------------+
                                                      the exit returns early
                                                      once a penalty has been
                                                      taken in that run
           |                         |                         |
           v                         v                         v
       green                    red, 4 calls               green

Surface B is what the suite should have been. Surface C is the interesting one, because it is the shape a careful engineer produces by accident while cleaning up a noisy campaign. Its handler declares the same three selectors surface B declares, so nothing is missing from the callable surface. What it adds is an override on the exit that returns early whenever the run has already taken a penalty, four lines including the closing brace, the guard someone writes to stop a handler reverting on an underflow and then never looks at again. Other knobs narrow the same way. Foundry documents that a wider check interval can miss bugs that break and then restore the invariant between checks. the same guide on check_interval Each is a legitimate feature with a legitimate use, and each quietly subtracts states from what the campaign can observe.

Surface C makes every function of the pool callable and still reports the property as holding over 25,600 calls with zero reverts. Its selector table prints 8,450 delegates, 8,531 penalties and 8,619 exits, and each is an entry into the handler rather than a call that reached the pool. A counter inside the handler, written after every run and reconciling to that table exactly, puts the pool's own exit at 99 executions across the whole campaign, with 194 of the 256 runs never reaching it once. Every function is still exercised and every line still executed, because 99 clears a bar set at one. What the handler will not generate is the order that breaks the property. The step it subtracts is a single call. The order it forbids is four calls long.

Over surface C the coverage summary read 100.00% of lines, 100.00% of statements, 100.00% of branches and 100.00% of functions, and the defect was still there. A threshold set at anything up to full marks passes that. Surface B, the campaign that goes red, reports exactly the same full marks on all four metrics, so the percentage cannot tell the suite that catches this defect from the suite that cannot. That is the alternative at its strongest, measured on both sides rather than argued from one.

Branches are coverage's strongest dimension here, because they are the only unit that touches control flow, and they do not reach this defect either. A branch is a fork inside one call. What breaks this property is an order across four calls with a penalty between two of them. Coverage counts source locations that executed, every source location executed, and nothing in it describes the sequence.

  surface   penalty    order      property   coverage summary of the pool
  --------------------------------------------------------------------------
  A         absent     free       green      83.33 / 90.00 / 66.67
  B         callable   free       RED        100.00 / 100.00 / 100.00
  C         callable   bounded    green      100.00 / 100.00 / 100.00
  --------------------------------------------------------------------------
  columns are lines / statements / functions, same seed and filter on all three
  branches read 100.00 over 0 of 0 branch points on the surfaces measured, which
  is Foundry's counter reporting that it found no branch point in the file
 
  the same runs, asked for LCOV instead of a summary, name every function:
      surface A    delegate 12837   slash 0      undelegate 11634   FNH 2 of 3
      surface C    delegate  8482   slash 8270   undelegate   101   FNH 3 of 3
  the threshold reads FNH over FNF. It never reads the hit counts beside them.

Every campaign prints a table of calls per selector, and surface A's table carries no row for the penalty at all. That absence is the whole finding, printed by default under the green PASS line on the terminal of whoever ran it. The maintainers treat it as something a reader checks rather than assumes, and the same guide's best-practice table tells you to log call counts so you can verify all functions are being exercised. the guide's best-practice table The coverage side carries a second artifact of the same kind. The same LCOV report puts the pool's exit at 101 hits against 8,482 for the delegate, and the summary percentage throws that number away. The threshold reads the ratio and never the counts beside it. So the narrowing is not hidden. It is unread. No gate consumes the selector table and none consumes the per-function hit counts, which leaves the callable surface as the one artifact nothing checks.

The obvious reply is that a green over a small budget only tells you the budget was small. Raising surface C from 25,600 calls to 1,000,000 calls on the same seed changed nothing, and it still reported zero reverts and the property holding. The wall clock went from 7.74 seconds to 248.60 seconds, roughly thirty two times the machine time for an identical verdict, while the budget itself rose by a factor of 39.06. The search was never short of samples. It was short of a state it was forbidden to write.

What this harness does not establish#

This is one reduced pool of three functions and twelve lines, and it is not a protocol. It was written to make one accounting defect legible, so it says nothing about how a real restaking layer is laid out or how its rounding behaves. The coverage figures come from a three function contract, which is why they move in such large steps. Carry the mechanism out of this article. Do not carry the numbers.

The branch figure needs its own warning, because it is the one number in the table that describes the tool rather than the contract. Foundry's branch counter registered no branch points in this file at all, and the pool's first executable line carries a conditional. The report still prints full marks for branches over zero of zero branch points, a percentage carrying no information. It is a reason to read the point count beside every percentage before gating on it.

Two more things this run does not carry. The cost asymmetry below is reasoning from the mechanism and not a measurement, in either direction, and the same holds for the wall clock cost of a reachability review. And nothing here measures how often real handler surfaces under-reach in production repositories, the number that would say how much this matters at scale.

Who answers when the gate goes green#

Now price the two ways this gate can be wrong. A false pass is paid by whoever holds the stake, at the size of the position, by someone who never saw the pipeline. It stays invisible until it is not. A false alarm is paid by the reviewer, once, on the morning it fires, and everyone involved can watch the cost while it happens.

Those two are not the same order of thing, and no threshold reconciles them, because a threshold cannot be more careful in one direction than the other. Reaching for a person here would be too quick. This run has already printed two machine-readable signals that no gate consumes, and either could be wired into a pipeline in an afternoon, so both have to lose on the merits before a name enters the argument.

Take the selector table first, because it is the cheaper of the two. Require every selector the handler exposes to be called at least some minimum number of times, and fail the build otherwise. Surface A goes red under it, for the same reason its coverage did. Surface C sails through, because its table shows every selector called thousands of times, and the exit that never once ran after a penalty sits inside the largest count on the page.

Take the LCOV hit counts next, which get closer, since they are per function and already inside the file the threshold reads. A rule flagging an order of magnitude gap between functions of one contract would fire on surface C, where the exit records 101 against 8,482 for the delegate. But a hit count has no order in it, so no threshold over hit counts separates an exit taken after a penalty from an exit taken before one, and those 101 hits would read the same if every one of them had followed a penalty.

Only now does a name earn its place. One person owns the question of whether the callable surface can reach the state each property is about, that person may hold a release, and a release goes out over their red only in writing with the reason recorded against it. The hatch has to be visible, because a gate with no usable hatch gets quietly weakened by whoever needs to ship on a Friday, and a weakened gate look like a strong one from outside. And if your codebase still has whole functions no test enters, set the function threshold and come back once they are gone.

The hard case is the shop this is written for. One owner, or a small team with no second pair of eyes in the building, and review time that is its scarcest resource. There the person who owns the callable surface is the same person who wrote the handler, and a reviewer reading his own work at the same sitting is a weak instrument. What survives that is not a second reader. It is a second occassion and a written answer, the question put at a different sitting from the writing, against a list the reviewer is not holding in his head, and the answer recorded in the pull request.

There is a date on this recommendation, and it is worth saying what would retire it. Both mechanical candidates above measure what ran. A machine that measures whether the suite can fail at all exists. It is mutation testing, which alters the source and asks whether the suite notices. In that vocabulary a mutant is killed when at least one test fails, and it survives when the changed code still passes the selected tests. the Foundry mutation testing guide A surviving mutant is a piece of the contract the suite cannot feel, the same object a reachability review hunts for by hand.

The catch is what the tool will do with that answer today. The capability has shipped. The enforcement has not. But survived mutants do not currently make forge test --mutate fail and there is no threshold flag yet, so a team that wants the gate runs with --json and enforces its own threshold from the output. the mutation guide on gating in CI So it is gateable today, at the cost of a script somebody maintains and a bill somebody pays when the run gets slow.

That cost is the whole flip condition. The day the threshold becomes a flag the tool sets, the mechanical check gets cheaper than the human one and the reviewer's pass moves up a level, off individual campaigns and onto the properties themselves. Foundry says as much itself, since the same page calls mutation testing an MVP whose workflow, reporting and supported project configurations are still expected to evolve. the mutation guide's own maturity note The flip is not the day the capability arrives. It is the day carrying the threshold stops being the team's own job.

Until then the check is a reading task, and it costs about as long as reading the handler. Open the handler. List the selectors it exposes, list the orders it declines to generate, and ask of every property whether the state it asserts about is constructible from what is left. Then read the two artifacts the tools already print, the selector table from the last campaign and the per-function hit counts from forge coverage --report lcov, which is the format that names them. Then plant a defect the property is supposed to catch, run the suite, and require a red before the gate goes back to being trusted. That last step is this article performed once, one planted accounting defect and three callable surfaces over it, and only the surface that could construct the order turned red.

Nothing in that procedure belongs to Foundry. Every search-based harness declares a callable surface under some name, a handler here, a strategy or a generator elsewhere, each authored by hand, narrower than the contract it stands in front of, and reviewed by nobody. A gate earns its place only when the search behind it can reach the state the property is about, and someone has checked that it can. A gate that is a formal proof over the full state space samples nothing, so this does not reach it, and neither does a property checked by a tool that enumerates its space instead of sampling it. A rule about what a search can reach stops being true when the tool does not search. Everything else is a green badge, and a green badge is the cheapest thing in the repository to make.

Abdel KIARI
I’ve owned the EVM side of a DeFi protocol with $110M+ in funding, including backing from Coinbase Ventures. I redesigned its architecture from scratch and built the Solidity infrastructure end to end.
Always happy to talk about interesting opportunities
abdel.kiari@gmail.com