Solidity Audit

When to use

• Auditing or reviewing a Solidity contract or .sol file
• Checking a DeFi protocol, token, staking pool, vault or factory
• Running Slither or Mythril
• Asking whether a contract is safe
• Wanting a security report

What it does

1. Environment setup
2. Compile and size check
3. Static analysis and lint
4. Symbolic execution
5. Foundry test suite
6. Coverage and mutation testing
7. Manual review
8. Economic review
9. HTML report

Files in the skill

• references/environment.md — Toolchain blockers: blocked compiler CDN, dependency conflicts, per-tool solc paths, running long jobs detached
• references/invariant-testing.md — Handler design, ghost variables, and detecting invariants that pass vacuously
• references/manual-review.md — The manual review checklist
• references/report-structure.md — How the HTML report is organised
• assets/HostileTokens.sol — Token mocks reproducing USDT, USDC, PAXG, rebasing, false-returning, zero-decimal and reentrant behaviour
• assets/foundry.toml — Foundry configuration
• assets/report.css — Report styling
• scripts/setup_toolchain.sh — Installs the whole toolchain

SKILL.md

Skill description: Run a complete smart contract audit — static analysis, symbolic execution, Foundry test suite construction, stateful invariant testing, coverage measurement, mutation testing, manual review, economic modelling, and a professional HTML report. Use this whenever the user mentions auditing, reviewing, testing, verifying, or checking a Solidity contract, .sol file, smart contract, DeFi protocol, token, staking pool, vault, or factory — and also when they ask to "run Slither", "run Mythril", "check this contract for bugs", "is this contract safe", or want a security report. Use it even for a quick look at a contract, because the phases are optional but the honesty requirements are not.

The principle that shapes everything

Static analysis finds known patterns. It does not find wrong logic that executes correctly. Assume the most dangerous bug in the contract will pass every detector cleanly, and structure the work so something else has a chance of catching it.

This is not hypothetical. On the run this skill was built from:

The critical bug was an ordinary-looking subtraction inside otherwise coherent accounting. No pattern-matcher was ever going to find it.

Expected yield, highest first: invariant testing → manual review of the accounting → coverage → mutation testing → static analysis → symbolic execution. Run them in whatever order is convenient, but weight attention accordingly.

Phases

Phases 1–3 are cheap and fast. Phases 4–6 are where bugs are found. Phase 7 applies only to contracts with incentives. Skip phases when the user wants something quicker — but say which ones you skipped.

Phase 0 — Environment

Read references/environment.md first. It contains blockers that will otherwise cost significant time: a blocked compiler CDN, dependency conflicts between tools, per-tool solc path conventions, and the fact that long-running jobs exceed the tool timeout and must be launched detached.

scripts/setup_toolchain.sh installs the whole stack. Run it and report every version.

Phase 1 — Compile

• SHA-256 of every source file. Record it; it scopes the entire report.
• Compile with the matching pragma. If it fails with "stack too deep", retry with --via-ir and report that the default pipeline does not build. That is a finding, not a footnote — a build performed without it produces no artifacts at all.
• Deployed bytecode size against EIP-170 (24,576 B), with remaining margin. Factories embedding type(X).creationCode couple their size to the child.
• Every compiler warning. Zero is the target.

Phase 2 — Static analysis

• Slither, all detectors, grouped by impact/confidence. De-duplicate: findings repeat when several files compile together. Save raw JSON.
• Slither printers — not detectors, and worth running: vars-and-auth (per-function authorization — use it to verify or refute any access-control claim the contract makes), modifiers, human-summary, entry-points.
• solhint with solhint:recommended.
• slither-check-erc if the contract is a token. If it isn't, run it once anyway and report "not applicable" as a measured result rather than an assumption.
• Triage every finding. State true positive / false positive / intentional, and why. An untriaged detector dump is not analysis.

Phase 3 — Symbolic execution

• Mythril per contract explicitly: myth analyze File.sol:ContractName --execution-timeout 900. If the contract needs viaIR, put it in the --solc-json settings.
• halmos for arithmetic properties, when the maths is non-trivial.
• A timeout is not a pass. Report proved / timed-out / counterexample separately. Nonlinear integer arithmetic frequently will not close — say so rather than omitting the attempt.

Phase 4 — Foundry test suite

Write the tests. Don't ask the user to.

Read references/invariant-testing.md for handler design, ghost variables, and — most importantly — how to detect invariants that pass vacuously.

Cover:

• Unit and fuzz: happy paths, every revert condition, boundaries, and the specific property the design claims to guarantee.
• Stateful invariants: random sequences of every state-mutating function, several actors, random time jumps, hostile actions in the action set.
• Real-token compatibility: plain ERC20s do not exist in production. Copy assets/HostileTokens.sol into the suite — it reproduces USDT's missing return value and approve-race guard, USDC's blocklist and pause, PAXG's live transfer fee, rebasing shapes, false-returning tokens, zero-decimal tokens, reentrant tokens, and a catch-all-fallback token.
• Mainnet-fork tests: write them regardless. If no RPC is reachable, say so explicitly and warn that fork tests which self-skip report PASS while executing nothing. Never present those greens as coverage.

Phase 5 — Measure the tests

A green suite is not evidence. Two independent checks:

Coverage. forge coverage --ir-minimum, then parse lcov for uncovered lines. Report line, statement, branch and function coverage. Name every external function with zero coverage. Report branch coverage alongside line coverage rather than behind it, and note that Foundry counts revert paths as branches, so the figure understates.

Mutation testing. Inject defects and confirm the suite goes red:

• Manually, targeting the accounting: remove a decrement, delete a bounds check, swap two arguments, invert a comparison.
• Automatically: slither-mutate <file> --test-cmd <fast subset>. Exclude slow invariant runs from the test command or the campaign will not finish.
• Report every surviving mutant. A survivor is a real gap. Fix the test, re-run, and record it in the report.

Phase 6 — Manual review

Tooling supplements this; it does not replace it. Read references/manual-review.md for the checklist. The single highest-value item: write the contract's core accounting identity down as an equation, then verify every function preserves it.

Phase 7 — Economic review

Only for contracts with incentives. Model numerically and show the tables: where rewards come from; whether yield is real or dilution; capacity and sustainability at realistic parameters; recovery and exit costs; adversarial strategies (whale capture, self-staking, tier arbitrage, MEV); fee model and price sensitivity. Distinguish token-denominated returns from real returns.

Phase 8 — Report

Read references/report-structure.md. Produce a single self-contained HTML file, print-friendly, graphs embedded inline. Use assets/report.css.

Honesty requirements

These override any impulse to make the output look better than the work was.

• A self-assessment is not an audit. If you wrote the contract, the tests and the report, say so on the cover. A test suite cannot test for a misunderstanding it shares with the code.
• Clean tool output is not a clean audit. State plainly what the tools cannot catch in this specific contract: business-logic errors, wrong rules correctly executed, economic assumptions, integration behaviour.
• Report your own errors. If you introduced a bug and later found it, say which phase introduced it. If you overstated something earlier, correct it in writing rather than quietly revising.
• Timeout ≠ proof. Skip ≠ pass. Line coverage ≠ tested.
• Distinguish found by tool X from found by manual review for every finding.
• List what was attempted and failed, not only what succeeded.
• If the user asks "are you sure?", re-derive the answer from evidence. Do not manufacture new findings to appear responsive, and do not simply repeat the previous answer either.

Deliverables

• Source files with hashes recorded
• The full Foundry suite, runnable
• Raw tool output: Slither JSON, Mythril, coverage lcov, mutation log
• Graphs as SVG
• The HTML report
• A short plain-language summary of what blocks mainnet deployment

Scope

This skill is for reviewing contracts to find defects. It does not write exploit code or weaponise findings. Proof-of-concept tests demonstrating a bug belong in the Foundry suite as regression tests, framed as verification rather than as attack tooling.