How Smart Contracts Are Audited: The Methodology

Search “how are smart contracts audited,” and most of what you find is either a marketing checklist or a post-mortem of the latest hack. What is genuinely rare is a practitioner-grade account of how the work is actually done: what a senior auditor looks at first, how automated tooling and manual reasoning divide the labor, and what a rigorous review actually does with the source a project hands over. This article walks through that methodology as Dedaub practices it.

A smart contract audit is a structured, point-in-time security review of the code that will govern user funds and protocol logic onchain. When done well, it combines expert human review with large-scale automated analysis and treats the contract not as a document to be read but as an adversarial system to be broken.

Who does the work, and why that matters

The single biggest quality differentiator in an audit is who is reading the code. At Dedaub, every engagement is run by senior security researchers, with the methodology structured around “constant challenging between the two senior auditors” who continuously probe each other’s understanding and are challenged to explain difficult elements of the code.

That depth is not incidental. Dedaub’s founders come from a program-analysis research lineage, and both still teach it. Yannis Smaragdakis is a Professor at the University of Athens’ Department of Informatics and Telecommunications, described as bringing “20-yr world-leading research expertise” in “Program analysis, systems, security.” Neville Grech lectures in Computer Science at the University of Malta, where his teaching includes Blockchain and Smart Contracts, and is a “white hat hacker with 15 years in software engineering, security, and program analysis” and lead author of MadMax. Most of the team holds relevant PhDs. The reason this matters for an audit is that the hardest bugs are not pattern matches. They are emergent behaviors that only surface when someone who understands the machine at a deep level reasons about how independent components interact.

How smart contracts are audited: two adversarial mindsets

A rigorous review is not a single linear pass. Dedaub’s published methodology describes two distinct phases. In the first, auditors work to understand the code as it is meant to function through “legitimate use,” building a precise mental model of intended behavior. In the second, the same auditors switch mindsets entirely and “attempt to subvert the system’s assumptions,” approaching the contract as an attacker would.

This split matters because most exploits do not violate a rule the developer wrote. They violate an assumption the developer never wrote down. Reentrancy, price manipulation, rounding drift, access-control gaps, and cross-function state confusion all live in the space between what the code says and what the developer assumed. You only find them by first mapping the assumptions, then deliberately attacking each one.

Reviewers examine both isolated components and “complex combinations of different parts that may result in unexpected behavior,” and they extend scrutiny to how the contract behaves against the outside world, reviewing “integrations with external protocols and dependencies, such as AMMs, lending platforms, and Oracle services.” Composability is where a locally correct contract becomes globally exploitable, so integrations are treated as a first-class attack surface.

Static analysis at scale

Manual review is essential, but it does not scale to every code path, so it runs alongside heavy automation. Dedaub’s published methodology pairs the two senior auditors with “over 100 static analysis algorithms, AI, and automated fuzzing” run against the codebase under review. These sweep for known dangerous patterns and control-flow anomalies across the whole codebase, surfacing candidates far faster than a human could and letting senior reviewers spend their time on the findings that require judgment.

Automation and human review are not competing approaches here. The tooling widens coverage; the auditors provide the reasoning. The automated pass narrows a huge space of possible states down to the handful that deserve a human’s full attention, and everything it flags is then examined by the people who understand why it matters.

Fuzzing and verifying invariants

Reading the code establishes what it is meant to do; testing establishes whether it holds up under inputs no one anticipated. Automatic fuzzing throws large volumes of generated inputs at the contract to drive it into states a hand-written test suite would miss, and it runs directly on contracts that the static analysis stage flags.

Beyond fuzzing, a mature audit reasons about invariants: the properties that must always hold no matter the input sequence, such as “total supply never exceeds the cap” or “no user can withdraw more than they deposited.” Formal verification of these critical invariants is a capability an audit can bring to bear on the properties that matter most, providing mathematical assurance for the handful of guarantees whose failure would be catastrophic. It is a technique applied to the highest-stakes parts of a system, not a certification stamped on the whole.

What happens after the audit

An audit is point-in-time. It certifies the code as reviewed on a given date, but protocols upgrade, dependencies change, and attackers keep probing. A rigorous engagement, therefore, ends with a remediation round in which fixes are re-verified rather than taken on trust, and any material upgrade after release is a reason to bring the auditors back: new code paths mean new assumptions to attack.

The short version

A smart contract audit, done well, is neither a scan nor a checklist. It is senior human reasoning, run in two adversarial phases, amplified by static analysis at scale, stress-tested with automatic fuzzing, and reinforced with formal verification of the invariants that matter most. To see how this maps to a full engagement, read Dedaub’s Web3 audit methodology, or request a scoped audit.