Static Analysis, Formal Verification & Auditing

Formal verification proves that properties hold for all possible inputs and states (within a model).

36.1 Static analysis

Slither (Trail of Bits) fast static analyzer with ~100 detectors (reentrancy, uninitialized storage, shadowing, unchecked calls); printers for inheritance, call graphs, storage layout Aderyn (Cyfrin)

Rust-based static analyzer producing Markdown reports Mythril (Consensys) symbolic execution of bytecode; finds assertion violations, reentrancy, integer bugs linter for style and security rules Semgrep (Decurity rules) treat as errors; read every warning

pip install slither-analyzer
slither .                                  # analyze a Foundry/Hardhat project
slither . --print human-summary
slither . --print inheritance-graph
slither . --detect reentrancy-eth,unchecked-lowlevel
slither-check-upgradeability . BoxV1 --new-contract-name BoxV2
pip install mythril
myth analyze src/VulnerableBank.sol --solv 0.8.24

36.2 Formal verification

Formal verification proves that properties hold for all possible inputs and states (within a model).

SMTChecker (built into solc) checks asserts, overflow, division by zero, out-of-bounds, and unreachable code:

(In Foundry: [profile.default.model_checker] with engine = "chc" and targets = ["assert"].)

Certora Prover (open-sourced in 2025): write rules and invariants in CVL (Certora Verification Language):

Other tools: Halmos (a16z, symbolic testing of Foundry tests), hevm symbolic mode, Kontrol (Runtime Verification, K framework), SolCMC.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract Monotonic {
    uint256 public x;

    function inc(uint256 d) external {
        uint256 old = x;
        x += d;
        assert(x >= old);       // SMTChecker proves this (overflow would revert first)
    }
}

solc --model-checker-engine chc --model-checker-targets assert,overflow Monotonic.sol

// Bank.spec (CVL)
methods {
    function balances(address) external returns (uint256) envfree;
}

rule withdrawZeroesBalance(env e) {
    withdraw(e);
    assert balances(e.msg.sender) == 0;
}

invariant solvency()
    nativeBalances[currentContract] >= sumOfBalances;   // using a ghost sum (defined with hooks)

36.3 The audit process

freeze code, documentation and specs, NatSpec, threat model, full test suite with high coverage, run static analysis, fix known issues auditors estimate effort from nSLOC and complexity manual line-by-line review, architecture review, tool runs, PoC exploits in tests findings by severity (Critical / High / Medium / Low / Informational / Gas) team fixes, auditors verify; publish final report bug bounty (Immunefi), monitoring, incident response plan, re-audit on changes

Audit options: traditional firms (Trail of Bits, OpenZeppelin, ConsenSys Diligence, Spearbit/Cantina, ChainSecurity, Sigma Prime, Zellic, Cyfrin, Certora), competitive audits (Code4rena, Sherlock, Cantina, CodeHawks), and independent researchers. An audit reduces risk; it does not guarantee safety — defense in depth is essential.

36.4 Self-review checklist

[ ] All external/public functions: access control intended? input validation?

[ ] External calls: CEI followed? reentrancy guard? return values checked?

[ ] Arithmetic: rounding direction, precision, downcasts, unchecked justified?

[ ] Oracles: staleness, manipulation, decimals?

[ ] Tokens: fee-on-transfer, rebasing, ERC-777 hooks, non-standard returns, decimals ≠ 18?

[ ] Upgradeability: storage layout, initializers, upgrade authorization?

[ ] Signatures: nonce, deadline, domain separation, malleability?

[ ] DoS: unbounded loops, push payments, external dependencies that can revert?

[ ] Events emitted for all state changes? Admin functions behind timelock/multisig?

🧪 Part III Exercises

Write a Proxy + LogicV1/LogicV2 from scratch using ERC-1967 slots, then reproduce the storage-collision bug with a naive layout and fix it.

Implement the same sum(uint256[]) function in Solidity and Yul; fuzz-test that both always return the same result and compare gas.

Reorder a contract's state variables to minimize slots; verify with forge inspect <Contract> storageLayout and gas reports.

Write a from-scratch ERC-20 and run it against an ERC-20 property test suite (e.g., a16z erc20-test or your own fuzz tests).

Build an ERC-721 with a Merkle-tree allowlist mint phase and a public phase, with per-wallet limits.

Implement an EIP-712 "meta-transaction" voucher system; write Foundry tests that sign with vm.sign and test replay, expiry, and wrong-chain cases.

Reproduce the reentrancy attack on VulnerableBank in a Foundry test, then show that SafeBank defeats it.

Write an invariant test suite (handler + ghost variables) for an ERC-4626 vault: total shares ↔ total assets, no free shares, rounding favors the vault.

Run Slither and Aderyn on your Part II and III code; fix or justify every finding in comments.

Upgrade a UUPS proxy from V1 to V2 using the OpenZeppelin Upgrades plugin, then attempt an upgrade that breaks storage layout and observe the validation error.