The first time I audited seriously, I opened the biggest contract in the repo and started reading line one. Two hours later I had a headache and zero findings. I had memorized how the code worked without ever asking what it was supposed to guarantee. That is backwards, and it took me a while to unlearn it.

Now I do not read Solidity first. I read the scope, and before I look at a single function body I write down what must always be true. Bugs are violations of those truths. If you do not know the truths, you are just admiring the code.

Step one: write the invariants before you read

An invariant is a property the protocol claims will always hold, no matter who calls what in what order. For a contest, I start with money and control, because that is where severity lives.

Two questions cover most of it:

  • Who can move funds, and under what conditions?
  • What must always hold about the accounting?

For a lending-pool-shaped protocol my starting invariant list looks like this, written in plain language before I care how any of it is implemented:

  • The sum of all user deposits minus all borrows equals the pool's available liquidity plus outstanding debt. Accounting must reconcile.
  • A user can only withdraw up to their own balance, never more, never someone else's.
  • A position can only be liquidated when it is actually under the health threshold.
  • Interest accrues monotonically, it never goes backwards in a way that lets someone repay less than they owe.
  • Only the borrower, or a liquidator on an unhealthy position, can reduce a debt.
  • Nobody except governance can change interest rate parameters or the oracle.

Notice none of that mentions a function name. These are the promises. Now my job for the rest of the contest is simple to state: find an ordering of calls that breaks one of these.

Step two: map the external entry points

Funds do not teleport. Something has to be called from outside for state to change. So I list every externally reachable function, because the attack surface is exactly that set and nothing else.

I do this fast with grep before reading anything carefully:

# every external / public function in scope
grep -rnE "function .*\b(external|public)\b" src/ \
  | grep -v "view\|pure"

Enter fullscreen mode Exit fullscreen mode

I drop the views and pures because they cannot change state. What is left is the list of levers an attacker can pull. For a lending pool that is usually the familiar set: deposit, withdraw, borrow, repay, liquidate, and whatever admin setters exist.

Then I annotate each one with the invariant it could threaten. deposit and withdraw threaten the accounting reconciliation. withdraw threatens the "only your own balance" rule. liquidate threatens the "only when unhealthy" rule. The setters threaten the governance-only rules. Now I have a grid: entry points down one side, invariants across the top, and cells where they intersect are where I go hunting.

Step three: draw the trust boundaries

Most real findings live at the seams where the protocol trusts something it should not fully trust. Before reading logic I mark every boundary:

  • Oracles. Where does price come from? Can it be manipulated in a single transaction (spot price from an AMM is the classic footgun)? What happens if it returns stale data, or zero, or reverts?
  • Admin and roles. What can a privileged role do, and is any privileged path reachable through a proxy or a delegatecall in a way the code did not intend? "Admin can rug" is often out of scope, but "a non-admin can reach an admin-only effect" is a High.
  • Cross-contract calls. Every external call is a place where control leaves the contract and can come back (reentrancy), or where the callee can behave adversarially (a malicious token with a weird transfer, a fee-on-transfer token, a rebasing token).
  • Token assumptions. Does the code assume 18 decimals? Assume transfer returns a bool? Assume no fee on transfer? Each assumption is a boundary that a hostile token crosses.

For the lending pool, the oracle boundary is where I would look first, because "manipulate price, borrow against inflated collateral, walk away" is the shape of a lot of Highs.

Step four: now read the code, hunting for violations

Only now do I open function bodies. And I do not read them as "what does this do." I read them as "which invariant does this touch, and can I break it here."

Here is a mini worked example. Pseudocode, lending-pool-shaped, deliberately buggy:

// invariant at risk: a user can only withdraw up to their own balance
function withdraw(uint256 amount) external {
    uint256 shares = amountToShares(amount);
    // BUG: no check that balanceOf[msg.sender] >= shares
    balanceOf[msg.sender] -= shares;   // underflows? or does it?
    totalShares -= shares;
    token.transfer(msg.sender, amount);
}

Enter fullscreen mode Exit fullscreen mode

Reading invariant-first, I do not ask "does this transfer tokens." I ask "does this enforce that you only take your own balance." The answer is no, there is no bound check before the subtraction. In old Solidity that underflows to a giant balance. In 0.8+ it reverts, so maybe safe... unless amountToShares rounds in a way that lets shares come out to zero while amount is nonzero, in which case you withdraw tokens while decrementing nothing. That is the crack. I go verify it with a Foundry PoC, because a hypothesis is not a finding until it fails a test.

Compare that to the oracle boundary:

// invariant at risk: only genuinely unhealthy positions can be liquidated
function liquidate(address user) external {
    uint256 price = ammPair.getSpotPrice();   // single-block manipulable
    uint256 collateralValue = collateral[user] * price;
    require(collateralValue < debt[user], "healthy");
    // seize collateral, repay debt
}

Enter fullscreen mode Exit fullscreen mode

The invariant says liquidation only happens when a position is truly unhealthy. But price comes from a spot AMM read, which a well-funded attacker can push within a single transaction using a flash loan. So they can make a healthy position look unhealthy, liquidate it, and profit. The bug is not in the arithmetic, it is in trusting a manipulable source. Invariant-first thinking finds it because I already flagged the oracle as a boundary in step three, before I ever read this function.

Why this order matters

If you read code first, you get anchored on how it works and you start believing it. The author's mental model leaks into yours. You end up checking that the code does what it appears to intend, which is the opposite of auditing. Auditing is checking whether the code can be made to do what it must never do.

Invariants first flips the frame. You decide what the protocol promised, independent of the implementation. Then every function is a suspect measured against those promises. When I built spectr-ai, this is the structure I tried to bake into how it reasons: state the properties, then check the code against them, rather than free-associating about "vulnerabilities."

It is also faster. On the contest I picked this week, writing the invariant list took maybe 40 minutes and it turned a 2,000-line codebase into a short list of "here are the six things worth breaking, and here are the three seams where they probably break." That is a map. Reading line one to line two thousand is just wandering.

When you sit down with an unfamiliar codebase, do you write down what must always be true before you read it, or do you dive into the code and reconstruct the rules as you go?