T30 · Audit
What does an audit actually examine?
- Capabilities practiced
- Builder
- Hands on
- Write five invariants for your protocol and use fuzzing to check them automatically.
- AI Lab
- Have AI infer invariants from the code; decide yourself which are real safety properties and which are mere implementation details.
A Real-World Problem
A team is preparing to launch and pays a substantial amount for an audit.
Three weeks later, the report arrives with 17 findings: 2 high, 5 medium, and 10 low or informational. The team fixes all 17, the auditors verify the fixes, and the final page says every issue is resolved. The team puts the PDF on its website, announces that it has “passed an audit,” and launches.
Three months later, the protocol is drained.
The most striking fact in the postmortem is not the amount lost: the attack path was not mentioned anywhere in the report. The auditors did not miss one line of code; the attack used no code vulnerability. The attacker raised a collateral price in an external market, then borrowed assets far beyond the collateral's real value. Every call was valid.
When the team asks the auditors, the answer is defensible: the report clearly scoped itself to “correct implementation of the contract code,” excluding “the protocol's economic assumptions in extreme market conditions.” That scope appeared on page 2, which the team had skimmed.
The question becomes: what exactly did the money buy? If fixing all 17 findings still leaves a protocol drainable, which part of an audit carries lasting value?
Thought Experiment
Imagine you are an investor choosing between two protocols. Both show you an audit report.
Protocol A's report: 58 pages and 23 findings, each graded and supported by a code location, reproduction steps, a fix, and a “resolved” mark. It looks highly professional.
Protocol B's report: 19 pages and 6 findings, none high-severity. But it begins with two things A's report lacks:
First, a threat model. It identifies possible attackers—ordinary users, large holders, arbitrageurs who can borrow vast amounts, governance-token holders, and external dependencies—what each can do, and what the protocol explicitly does not defend against. For example: “We assume the price source cannot be moved more than 5% in a block. Beyond that, the protocol may incur bad debt.”
Second, an invariant list. Eleven statements say “whatever happens, this must remain true.” Each has an automated test, such as “the sum of all user deposits never exceeds assets the contract actually holds.”
Which report makes you more willing to invest?
Many people initially pick A: more findings suggest a deeper review. But think again:
- A's 23 findings tell you what was wrong and has since been fixed. They describe the past.
- B's threat model tells you what the protocol believes is dangerous and admits it does not cover. It describes boundaries.
- B's invariants mean those eleven properties are checked again automatically whenever code changes. They describe the future.
A's report starts becoming stale as soon as it is delivered. Every post-launch code change lies outside its snapshot. B's eleven invariants keep living with the repository.
Your Decision
Your protocol launches in two months. The remaining safety budget buys one more action. Which do you choose?
What Happens
These are not mutually exclusive, but each answers a different question. Arrange them by time window:
| Method | Time window | What it can find | Does it expire after delivery? |
|---|---|---|---|
| Audit | One pre-launch snapshot | Issues reviewers imagine within the agreed scope | The next changed line is uncovered |
| Invariants + fuzzing | Now onward | State that violates properties you declared | No; it stays with the repository |
| Monitoring | Every moment after launch | Anomalies already occurring | No, but someone must actually watch |
| Bug bounty | Continuously after launch | Ideas others have that you missed | Depends on bounty versus attack proceeds |
The chapter's most important sentence follows:
An audit is a snapshot, while your protocol must live for years.
A report is most valuable when delivered and gradually decays as code, dependencies, and market conditions change while the report does not.
Which part of an audit does not decay?
Return to Protocol B's 19-page report. The lasting parts are not six findings but its threat model and invariant list. One defines what counts as dangerous; the other makes that definition run automatically. They may be byproducts of the audit process, but they outlive the findings list.
So what does an audit actually examine, and what should it produce?
The lasting output of an audit is a threat model and invariants, not a PDF.
A findings-only audit buys one round of bug fixes. An audit that establishes a threat model and invariants buys an ongoing safety capability, potentially for the same price.
Build a Model
This chapter offers three reusable tools: four threat-model questions, three classes of invariants, and boundaries for four layers of testing tools.
1. Threat model: four questions you must answer
A threat model is not an essay. It answers four questions. If you cannot answer them, you do not yet know what you are defending against.
| Question | What to write | If you cannot, then... |
|---|---|---|
| Who may attack? | List ordinary users, large holders, capital-rich arbitrageurs, governance-token holders, external protocols you depend on, and your own multisig holders | You will miss whole attacker classes, especially the last two |
| What do they want? | User deposits, treasury, LP liquidity, governance control, or simply an outage | You will defend money but miss availability |
| What can each do? | For each role, list callable functions, available capital, transaction-order control, and patience across blocks | You will underestimate borrowable capital from T29 |
| What do you explicitly not defend against? | Write down assumptions you choose to leave uncovered | This is the most important question |
The fourth question separates a professional boundary from a vague hope.
Every protocol leaves something undefended: stolen private keys, failure of an entire oracle network, more than a given amount of single-block price manipulation, or a freeze of underlying assets. Those choices can be reasonable; defending against everything can make a product impossible.
What is unreasonable is leaving them unwritten. Then teammates disagree about the boundary, integrators assume a protection you lack, and an incident cannot be classified as intended behavior or a vulnerability.
Write one concise statement per assumption:
We assume: the price source deviates no more than X% in a single block.
If it does: the protocol incurs bad debt, covered first by insurance and
then pro rata by LPs.
We do not defend against: a price source manipulated for a prolonged period.
Mitigation: heartbeat checks and a deviation circuit breaker.Compare T29: the third threat-model question feeds T29's attack-cost table. Each attacker capability sets a value for capital and time there.
2. Invariants: three useful forms
An invariant says “whatever happens, this must remain true.” Good invariants describe state instead of a procedure, fit into a simple check, and signal genuine harm when broken.
Most useful invariants fall into three classes.
First: accounting invariants. Conservation of money is the easiest and often most valuable.
Sum of all user balances <= assets actually held by the contract
Total supply == sum of all holders' balances
Total lent + balance in pool == total deposited + accrued interest
Value per share never decreases (except on liquidation or bad debt)The first uses “less than or equal,” not equality, to allow fees and rounding dust. Rounding must favor the protocol, as T28 explained; here it becomes an automatically checked assertion.
Second: permission invariants. Who is allowed to do what?
Only the administrator can change parameters
Parameters always remain within their declared ranges
While paused, no function changing balances can succeed
No call path lets a non-liquidator take another user's collateralThird: state-machine invariants. Which transitions and states are legal?
A position is either healthy or liquidatable; there is no third state
A closed position cannot be operated on again
Each order can be filled only once
A position below the health threshold cannot borrow moreThe common mistake is to call an implementation detail an invariant. “Internal array length equals user count” is true of one design; a different implementation may violate it while remaining perfectly safe. Use one question to tell them apart:
If this statement fails, does someone lose money or control? If not, it is not a security invariant.
3. Four tool layers and their boundaries
Compare tools by what they can detect and what they require from you:
| Layer | It can find | It cannot find | Your effort |
|---|---|---|---|
| Compiler and type system | Syntax, types, obvious uninitialized values | Logic errors | Almost none |
| Static analysis | Known patterns: reentrancy structure, unchecked returns, dangerous low-level calls | Logic unique to your protocol | Install, then triage false positives |
| Fuzzing | States violating invariants you declared | Properties you did not state | Writing invariants—the main cost |
| Formal verification | Whether a property must hold under a specified model | Errors in the model itself | High; reserve for critical functions |
Fuzzing offers especially strong value for its cost because the hard work is defining invariants. Those definitions are already assets: documentation, regression tests, and safety claims integrators can inspect.
Use static analysis as a filter, not a verdict. It produces false positives; triage them quickly instead of treating each as an argument.
Do not reach for formal verification first. It fits a small set of critical, concise functions with precise properties, such as whether share-to-asset conversion can ever harm earlier depositors.
4. Classify findings in three ways, not just by severity
Audit reports grade severity. When reviewing AI or tool findings, another grouping is more useful:
- Real finding
- False positive
- Omission
- Real finding: the issue exists and needs a fix.
- False positive: a tool or model claims an issue that is absent; identify it quickly.
- Omission: a real issue nobody found. You cannot count these directly; look for whole attacker classes absent from the threat model.
The opening team had a textbook omission. All 17 findings could be real, with no false positives, yet “arbitrageur with nearly unlimited borrowable capital” was outside the scope.
What It Is Called
A document stating who may attack, what they want, what they can do, and what you explicitly do not defend against.
It is an input to an audit, not merely an output. Auditing without a threat model asks someone to inspect your door locks without knowing whom you expect to keep out.
A statement about state that must remain true regardless of what happens and can be checked automatically.
One test distinguishes a safety invariant: if it fails, will someone lose money or control?
Scanning source or bytecode for known patterns without running it. It finds issues with recognizable shapes, such as reentrancy structures, unchecked returns, and dangerous low-level calls.
Use it as a filter, not a final verdict; false positives are common.
Generate many random inputs and call sequences, seeking states that violate invariants.
Stateful fuzzing, which calls multiple functions while retaining state, is much stronger than isolated single-call fuzzing. Real flaws often hide in sequences of calls, not one call.
Use mathematical methods to prove a property must hold in a specified model.
That is stronger than testing, but the result only applies to the written model: a wrong model yields a wrong proof. Reserve it for narrow, critical logic.
Observe onchain state continuously after launch and notify people when anomalies appear.
It reduces the time from incident to detection rather than stopping the incident itself. For a protocol with a pause switch, that interval may closely determine the loss.
A public offer of payment for finding and responsibly reporting a vulnerability.
It works only if the maximum reward is competitive with attack proceeds and you can repair the issue quickly.
Hands-on
Use a protocol you wrote for T22 or T19. If you have neither, the deposit-and-withdraw contract from T7 works too.
First, answer the threat model's four questions. Do not skip straight to invariants; derive them from the threat model.
Write three to five lines for each: who might attack, what they want, what they can do, and what you explicitly do not defend against. Give at least two answers to the fourth question.
Choose from all three classes to reach five invariants. A useful mix is two accounting, two permission, and one state-machine property.
Write each as an assertion and add what happens if it fails. If you cannot name a consequence, cross it out and rewrite it; it is probably an implementation detail.
Turn the five statements into assertion functions. Use one function per property. It should only check state, never change it.
For the two accounting properties, check whether equality or an inequality is appropriate given fees and rounding dust. Reversing the direction should make fuzzing fail immediately—which is useful feedback.
Connect stateful fuzzing. It must call several functions in sequence while retaining state, instead of resetting before every call. Many real flaws live in call sequences.
Run a short pass and confirm it actually invokes your functions, perhaps with a call counter. Then run a longer pass.
Deliberately break one property and confirm the checker catches it. Do not skip this step.
Reverse a rounding direction or comment out a permission check and rerun fuzzing. If everything still passes, the invariant is not truly active: the assertion may never run, or the fuzzer may never reach that path.
Before restoring the code, save the failing call sequence. It is a ready-made regression test.
Record three numbers: fuzzing iterations, functions covered, and length of the shortest failing sequence.
The last is especially revealing: a shorter failure sequence is easier for a real attacker to encounter.
The result is a safety asset that continues with the repository. It is also a deliverable for stage five of the capstone project.
AI Lab
Give the model your contract code and two tasks.
First, ask it to infer properties:
Here is my contract. Infer its implicit invariants: properties that must
remain true regardless of what happens.
For each, give four fields:
- Assertion stated in terms of state, not procedure
- Relevant function and line in the code
- Consequence if the assertion fails
- Your judgment: safety property or just a fact of this implementation?
Mark uncertainty explicitly; do not guess.Second, ask it to critique its own list:
Review your list and identify which items are implementation details rather
than safety properties. Explain each judgment.The second step is often more valuable than the first. When inferring properties, models tend to call a fact of today's code an invariant—“array length equals user count,” or “mapping keys are nonzero.” Such claims can be true without protecting any funds.
Review the list yourself and calculate what proportion are genuine safety properties. That proportion is worth recording: it tells you the tool's limits on this task.
The last verification point matters most. Compare its list with your threat model. If you include “arbitrageur with unlimited borrowable capital” but no invariant covers an extreme state in one transaction, that is an omission. The model sees code, not your threat model.
Verify these points yourself after using AI
- For each claimed safety invariant, identify who loses money or control when it fails
- For each implementation detail, confirm another implementation could change it without making the protocol unsafe
- Check every cited function and variable actually exists in your code
- Check whether accounting comparisons use equality or inequality correctly given real fees and rounding dust
- Check whether it treats “the current code happens to do this” as “this must always hold,” the commonest error
- Compare with your own threat model: is an entire attacker class missing from its invariants?
Real-World Case
A protocol completes an audit, fixes every finding, and launches. It then loses substantial funds when its price source is manipulated. The attack uses no code vulnerability; every call is valid.
The postmortem debate centers on whether economic assumptions were in scope. Often the answer is printed near the start of the report, which the team had not read closely.
The lesson is not that audits have no value. An audit's scope is its capability boundary, and you define that scope with the auditors. Without a threat model from you, it may default to code correctness alone.
Every unit test for a vault passes with high coverage. Once stateful fuzzing is connected, it finds a seven-call sequence that violates the invariant “value per share never decreases.”
Each function looks fine in isolation, but rounding accumulated in that particular order harms an earlier depositor.
Unit tests rarely find this class of bug: the code author often writes the tests too, so the sequence they did not imagine never becomes a test.
A team has onchain monitoring, and its alert fires when an anomaly occurs. But the alert goes to a noisy channel, and no one is on call overnight.
Several hours pass before anyone notices, though the protocol's pause switch was available throughout.
The lesson: monitoring effectiveness depends on who will see an alert and when, not merely on deployment. Grade alerts and assign a clear on-call owner and response time to high-severity ones.
Some protocols set a fixed bounty cap while much more money is reachable through a flaw.
That presents the discoverer with simple arithmetic. Moving toward rewards based on a share of funds saved can make reporting the better choice.
It is the same table as T29's attack-cost calculation: increase reporting reward until it exceeds attack proceeds.
Change One Variable
You define the audit scope deliberately instead of letting it default to “correct code implementation.”
Reviewers can test the attacker capabilities you stated and challenge what you explicitly chose not to defend against. Those challenges may be the most valuable part of the report, because they test your assumptions rather than just your code.
The cost is almost zero: a document you should write anyway.
They move from test-only checks to runtime enforcement. A violating transaction reverts, stopping the attack onchain.
The cost is Gas for a global check on every transaction. In practice, teams layer them: enforce one or two critical accounting invariants at runtime and leave others in fuzzing.
This is the same kind of tradeoff as T8's storage costs: safety often has a Gas price.
Your code has not changed, but your safety assumptions may have: interface behavior, fees, and reentrancy protection could differ.
This directly illustrates that an audit is a snapshot of dependencies as they existed then.
Write key dependency assumptions as invariants too, and alert when a dependency's implementation address changes.
That one fact bypasses much of the work above. Invariants, fuzzing, and reports cannot stop an account holding unrestricted authority.
It is the attacker role easiest to skip in the threat model's first question: your own administrator. Multisignatures, timelocks, and least privilege belong here and often cost less than another audit.
Takeaway Questions
Who bears risk? Audit reports usually disclaim liability for losses. Risk remains with the protocol team and users; an audit reduces probability, not guarantees safety. Treating “audited” as a safety guarantee is one of the industry's costliest misreadings.
Why use a blockchain? Because code and state are public, anyone can independently check your invariants. That brings pressure and opportunity: publish checks anyone can run, which are more credible than a PDF alone.
Will users stay if subsidies stop? In safety terms, ask: will the protocol remain safe if your team disappears? A system that needs people watching dashboards cannot answer yes. One supported by invariants and sound permissions might.
Chapter Check
The threat model and invariant list.
Findings say “this was wrong and is now fixed.” Their coverage starts decaying on delivery as code changes. A threat model defines boundaries, while invariants can keep running with the repository.
Ask whether violating it would make someone lose money or control.
“The sum of user balances does not exceed assets the contract holds” is a safety invariant: if it fails, somebody cannot withdraw. “Internal array length equals user count” may cease to hold after a harmless redesign; it is an implementation detail.
Real flaws often hide in sequences of calls, not in one call's parameters.
Each function can be correct alone while a specific order accumulates rounding errors or reaches an illegal state. Stateless fuzzing resets every time and cannot reach those combinations. The person writing unit tests may never imagine them either.
A check that can never fail is as ineffective as no check, but creates false confidence.
The assertion might be in an unreachable location, or fuzzing might never exercise the path. Only seeing it fail proves the checker is live.
This is the same principle as writing a failing case first in T12.
There is no universal answer. Check three things:
- Did you actually write it down instead of pretending the risk does not exist?
- For each boundary, did you say who bears the consequence if it is crossed?
- Does one boundary involve your own team—administrator keys, multisig members, or upgrade authority?
The third is most often skipped, yet it can bypass every other defense.
Key idea
The real output of an audit is a threat model and invariants, not a PDF.