Invariant-First Auditing: Closing the 40% Gap in Automated Coverage

Tooling catches many bugs, not all of them.

The misses are usually compositional, economic, or state-transition failures.

Invariant-first auditing is the practical way to target that gap.

What makes a strong invariant#

A strong invariant is:

• global (covers system behavior, not one function),
• adversarially meaningful,
• inexpensive enough to run continuously.

Example: split-merge equivalence invariant#

function invariant_splitMergeEquivalence() public {
    uint256 x = bound(rand(), 1e6, 1e24);
    uint256 a = x / 3;
    uint256 b = x - a;

    uint256 outDirect = model.simulateSinglePath(x);
    uint256 outSplit = model.simulateSplitPath(a, b);

    // allow explicit fee tolerance only
    assertLe(_absDiff(outDirect, outSplit), model.maxRoundingBudget());
}

This catches rounding composition bugs that single-call unit tests miss.

Multi-step adversarial state transitions#

Every edge should preserve a declared global safety property.

Harness design pitfalls#

1. Handlers that revert too often create false confidence.
2. Unrealistic bounds hide edge behavior.
3. Missing malicious mocks removes real attack surfaces.

Foundry structure that scales#

forge test --match-path test/invariants/*.t.sol -vvvv
forge test --match-test invariant_ -vvvv

contract InvariantHandler {
    function act_deposit(uint256 amt) external { /* bounded adversarial input */ }
    function act_withdraw(uint256 shares) external { /* ... */ }
    function act_rebalance(bytes calldata path) external { /* external-call boundary */ }
}

Practical rollout plan#

Further reading#

• Foundry invariant testing
• Building secure contracts