Smart Contract Security As A Delivery Practice

There is a version of smart contract security that most teams practise without having chosen it. You build for some months, engage an audit firm near the end, receive a report, fix what it contains, deploy, and treat the report as the security artefact. Security, in this model, is an event that happens to the code shortly before launch.

This is the stage-gate pattern under another name, and it fails for the usual reason: it applies scrutiny at the point of maximum batch size, minimum remaining time and maximum sunk cost. An auditor arriving at a finished system meets months of coupled design decisions at once and delivers findings to a team whose launch date is already public. The findings cheapest to act on — the architectural ones — arrive too late to act on.

The alternative is not more audit. It is to move most of the security work into the ordinary development loop, so that external review checks a system that has already been attacked rather than discovering it. What follows is what that loop contains, and where each technique stops working.

Threat modelling as a living document

Before there is code worth attacking, write down what you are defending and from whom.

A usable threat model is short and specific. It names the assets — what value sits where, and who can move it — and the actors, including the ones you would rather not think about: an ordinary user, a large holder, a block producer who can order transactions, a compromised operator, a malicious counterparty contract, a governance participant with a large stake. For each it asks the only question that matters: what is the most profitable thing this actor can do, and what stops them?

The value is not the document. It is that the exercise forces trust assumptions into the open. Most serious failures here trace back to an assumption nobody wrote down — that a price source would be honest, that a caller would be a contract of a particular shape, that an administrative key would stay under control, that a token would behave conventionally on transfer. Written assumptions get challenged; assumptions living in one engineer's head get inherited by a team that does not know they exist.

Keep it in the repository beside the code, review it when the design changes, and require an entry for any new external interaction. It is also the most valuable thing you can hand an auditor.

Stating invariants explicitly

If one practice separates teams that survive this domain from teams that get lucky, it is writing invariants down as executable statements rather than carrying them as intuitions.

An invariant is a property that must hold after any operation, by any caller, in any order: accounted balances never exceed actual holdings, the sum of user positions equals the recorded total, no user withdraws more than they deposited plus their accrued share.

Stating these is harder than it sounds, and the difficulty is the point. Teams routinely discover, in trying to write one precisely, that they do not agree about what the system guarantees. That disagreement surfacing in week three is worth far more than in an audit report. Some properties resist formalisation; record those as human-review items rather than letting them disappear because the tooling could not hold them.

// invariant: accounted supply never exceeds held balance
function invariant_solvency() public view {
    assertLe(vault.totalShares(), asset.balanceOf(address(vault)));
}

Once written as code, an invariant can be attacked mechanically, checked on every commit, and used as the specification against which everything else is judged. It is also the natural interface to any external reviewer: here is what we claim, here is how we check it.

Keep them system-level. A property holding only within one function is a unit test.

Include negative invariants. Things that must never happen are often easier to state, and more revealing, than things that must always hold.

Fuzzing, property tests and forked reality

Example-based tests confirm that the cases you thought of behave as expected. They are necessary and structurally incapable of finding the thing that gets you, because that is by definition a case you did not think of.

Property-based testing inverts the relationship. You state the property; the tool generates inputs, exploring boundaries, extreme values and whatever else has historically broken code of this shape. Stateful fuzzing — invariant testing — is the more powerful form: it generates sequences of calls from multiple simulated actors and checks your invariants after each step. Because most economic-logic defects are sequence defects, this is where the highest-value findings come from.

Getting real value from it requires some care.

Bound the actors realistically. If every simulated caller holds the admin role, you will not find access-control problems.

Include the hostile handlers. Reentrant callbacks, tokens with unusual transfer semantics, calls that revert, calls that burn all available gas. A handler set of well-behaved participants is fuzzing a fantasy.

Watch coverage, not just pass rate. A suite that runs a million cases and never reaches the liquidation path is reporting a million successes about code it never executed.

Run deep campaigns on a schedule. Short runs on every commit; long overnight campaigns at greater depth. Treat a failure from the long campaign as a priority defect and keep the failing sequence as a regression test forever.

Mainnet forking addresses a different blind spot. A contract correct in isolation can be a loss in context, because most systems depend on code they did not write: tokens with their own quirks, price sources, routers, other protocols. A mocked suite confirms every assumption you encoded into the mock — exactly the set you are least able to check.

Pin the fork to a block so tests are deterministic, and run a separate unpinned job against recent state so a dependency changing behaviour reaches you as a test failure rather than an incident. Use forked state for adversarial rehearsal too: an attack you can execute is an attack you can reason about, whereas one described in a paragraph is a debate.

Static analysis, symbolic execution and the shapes they catch

Static analysis is the cheapest check you own and belongs in the pipeline from day one, failing the build above a defined severity. It catches known-bad patterns: state changes after external calls, unchecked return values, untrusted delegate targets, missing access modifiers. It produces false positives, and the discipline is to triage each once, suppress it with a written justification in the code, and never leave an unreviewed warning in the output — a noisy tool nobody reads gives the feeling of coverage without the substance.

Symbolic execution goes further, exploring paths with symbolic rather than concrete inputs and either proving a state unreachable or producing an input that reaches it. It is more expensive and prone to path explosion, but on a bounded critical component it answers questions fuzzing can only fail to disprove. Static analysis on everything as a gate; symbolic execution where a wrong answer is catastrophic.

You do not need a catalogue of incidents to direct this work, only the shapes — because a shape you recognise is a shape you can build a check for.

Class	Shape of the defect	What catches it early
Reentrancy	External call made before internal state is settled	Static analysis, checks-effects-interactions, invariant tests with reentrant handlers
Integer and precision	Rounding the wrong way, truncation, decimal mismatch, unchecked casts	Property tests on arithmetic, invariants on conservation of value
Access control	A privileged function missing a modifier, or a role granted too broadly	Static analysis, role-aware invariant tests, a permission matrix
Oracle manipulation	A trusted value an adversary can move	Threat model, simulation under adversarial price movement, forked attack tests
Ordering and front-running	Profit available to whoever orders transactions in a block	Threat modelling with a block-producer actor, design review of price-sensitive paths
Signature and replay	A signed message usable twice, on another chain, or by another party	Property tests on nonce and domain handling, invariants on signature consumption
Upgrade and key compromise	Authority to change code held more loosely than the value warrants	Signer topology review, timelocks, treating keys as part of release design
Economic design flaws	The code does what it says, and what it says is exploitable	Adversarial review and simulation — no tool finds these

The last row deserves emphasis. The failures causing the largest losses are frequently not bugs a compiler would recognise: the code executes as written and the design is wrong. No static analyser helps, which is why human adversarial review is irreplaceable and the threat model is the foundation rather than the paperwork.

Adversarial review, and where formal methods earn their cost

By the time an external auditor sees the code, your team should already have attacked it hard. This is distinct from code review and needs scheduling as such: review asks whether the code does what it intends; attack asks how to profit from it.

Assign the adversary role explicitly. Someone whose whole job for a fixed period is to extract value. Not the author. Give them time, not a checklist.

Run it with stated goals. Pick a target — drain this vault, mint without depositing, freeze another user's funds, become admin — and work backwards. Concrete goals produce better attacks than open-ended reading.

Require attacks as executable tests. A written concern is an opinion; a failing test against forked state is a finding.

Bring in an outsider. Teams share blind spots because they share assumptions. An engineer who has never seen the design will ask the question you have all stopped asking.

Formal verification sits at the top of this ladder and is not free. It requires specialist skill, considerable time, and a specification precise enough to prove things against. It earns its cost when the component is small and self-contained, the property is crisply expressible, the value at risk justifies weeks of specialist effort, the code is stable, and the failure mode is catastrophic rather than degrading. It is poor value when the component is large and coupled, when requirements are still moving, when the property is economic rather than mechanical, or when the effort would displace fuzzing and adversarial review you have not yet done. A team with no invariant suite should not be buying proofs; they should be writing invariants, the same intellectual work at a fraction of the cost.

Formal methods extend the ladder rather than replacing it. Property-based testing tells you a property survived many attempts to break it; formal verification tells you it cannot be broken — within the bounds of the model, the assumptions, and the correctness of your specification. That last clause does real work: a proof of the wrong property is an expensive way to be confident.

Making it a pipeline, not a phase

All of this becomes a practice rather than a collection of good intentions at the point where it runs automatically and blocks merges.

On every commit. Warnings as errors, the full test suite, static analysis gating on severity, short fuzz campaigns, the invariant suite at shallow depth, forked tests at a pinned block, coverage reporting.

Nightly. Deep fuzz and invariant campaigns, unpinned forked tests, symbolic execution on designated critical components.

Per change of significance. Threat model updated, invariants amended, an adversarial session, and a written note on what new trust assumptions the change introduces.

Per release. Deployment rehearsal on forked state, the evidence pack assembled from pipeline output rather than by hand, external review scheduled well in advance.

This is the evidence-by-default argument of agile in regulated environments, applied where enforcement is economic rather than supervisory. Nobody assembles the record under pressure, and what you hand a reviewer has already survived a great deal.

What to do on Monday

Write five invariants for your most valuable contract and commit them as executable assertions. Not twenty — five, the ones that if violated would mean funds are gone. Most teams find at least one is hard to state precisely, and that difficulty is the most valuable output of the exercise.

Point a stateful fuzzer at them with at least two actor classes and one hostile handler, and let it run overnight. Check coverage in the morning: if the fuzzer never reached your critical paths, fix the harness before you trust a single passing run.

Then book two hours with an engineer who did not write the code, give them one objective — extract value from this contract — and ask for the result as a test rather than a paragraph. Do that fortnightly. It costs almost nothing, it is available immediately, and it finds the class of defect no amount of additional tooling will.