Manual review, automated tools, and formal verification
A professional smart contract audit is not a single activity but a layered combination of several distinct techniques, each catching a different kind of mistake. Manual code review is the foundation: an experienced auditor reads the contract line by line, comparing its logic against a mental catalog of known vulnerability classes like the ones covered earlier in this course, reentrancy, arithmetic edge cases, and access control gaps, while also thinking about the specific business logic of that particular protocol, since most serious bugs live at the intersection of correct-looking code and an incorrect assumption about how the system as a whole is supposed to behave. This is slow, requires deep expertise, and doesn't scale automatically to larger codebases, but it's the only technique that reliably catches logic errors that are specific to what a given contract is actually trying to do.
Automated static analysis tools complement manual review by scanning code for patterns that match known-bad constructs, an external call before a state update, a function missing an access control modifier, unchecked arithmetic in unexpected places, flagging them for a human to examine. These tools are fast and consistent, and they're good at catching the kind of well-understood, mechanical mistakes that are easy for a tired human reviewer to skim past, but they don't understand what a contract is trying to accomplish, so they produce both false positives, flagging patterns that are actually fine in context, and false negatives, missing bugs that don't match any known pattern. Formal verification sits at the far end of the rigor spectrum: for the specific, highest-value invariants in a contract, properties like 'the total supply of a token can never exceed some cap' or 'the sum of all user balances always equals the contract's total recorded balance', formal methods mathematically prove that the property holds for every possible input and execution path, rather than merely testing a sample of cases. It's expensive and typically reserved for a small number of critical properties rather than an entire codebase, but where it's used, it provides a categorically stronger guarantee than review or pattern matching.