How Modern Smart Contract Auditors Use AI and Security Tooling

Each Technique Sees a Different Slice of the System

Modern smart contract auditors combine manual security research with static analysis, fuzzing, symbolic execution, formal verification, and carefully controlled AI-assisted workflows. Slither and Aderyn can surface known Solidity patterns and support codebase navigation; Mythril explores EVM paths through symbolic execution; fuzzers probe inputs and transaction sequences; and formal methods test explicit properties against a model. Each technique sees a different slice of the system, so strong researchers use the outputs as evidence and hypotheses rather than treating a tool result as a validated vulnerability.

The table below summarizes what each class of technique is good at and where it stops. No single row covers a whole protocol, which is why serious audits layer them and then put a researcher in charge of the conclusions.

Static Analysis and Symbolic Execution: Fast Signals, Not Verdicts

Static analyzers read source code or its compiled representation without executing it. Slither ships a large set of detectors for known Solidity issues and printers that map inheritance, call graphs, state variable access, and function summaries. Aderyn, written in Rust, parses the Solidity AST and produces a report of detected patterns. Researchers use both for two different jobs: catching familiar mistakes early, and getting oriented in a large codebase quickly.

Symbolic execution treats inputs as symbols and asks a solver whether a dangerous state is reachable. Mythril analyzes EVM bytecode this way, and Halmos applies symbolic reasoning to Foundry-style tests. When a solver finds a path, it returns concrete inputs, which makes the result easy to check. When the path is too deep or the state too large, the tool times out or gives up, so silence is not evidence of safety.

Both techniques produce noise. A detector cannot know that a low-level call is intentional, that a role is held by a timelock, or that an unchecked value is bounded elsewhere. Triage is part of the work: every warning is either confirmed with a reproduction, explained and dismissed, or turned into a question for the development team.

• Run analyzers on the exact audited commit so results map to the reviewed code.
• Use printers and call graphs to find privileged paths and external calls worth manual tracing.
• Record why each dismissed warning is safe, so later reviewers do not repeat the analysis.
• Treat a timeout or an empty result as unknown, not as proof that a path is safe.

Fuzzing and Invariant Testing: Searching for the Sequence That Breaks the Rules

Fuzzers generate large numbers of inputs and transaction sequences and check whether a property ever fails. Echidna and Medusa are property-based fuzzers built for smart contracts, and Foundry provides fuzz tests and stateful invariant tests directly in the Solidity test suite. The value comes from the properties: a fuzzer can only find what someone has expressed as a rule.

Auditors therefore spend real effort writing invariants. Typical examples are solvency (assets held cover what users can withdraw), conservation (total shares match the sum of balances), monotonicity (an index never decreases), and authorization (only a defined role can change a parameter). Handlers constrain the fuzzer to realistic calls, and ghost variables track expected values so the test can compare intent with actual state.

Fuzzing is especially effective at finding rounding drift, ordering problems, and edge cases that only appear after several calls. It cannot prove that no counterexample exists, and a poorly bounded handler can hide real paths or generate impossible ones. Results still need manual reproduction and an impact assessment.

contract VaultInvariants is Test {
    Vault vault;
    VaultHandler handler;

    function setUp() public {
        vault = new Vault(asset);
        handler = new VaultHandler(vault, asset);
        targetContract(address(handler)); // fuzz only realistic user flows
    }

    // Must hold after every generated call sequence.
    function invariant_vaultCoversIssuedShares() public view {
        uint256 owed = vault.convertToAssets(vault.totalSupply());
        assertGe(asset.balanceOf(address(vault)), owed);
    }
}

Formal Verification: Proving Explicit Properties Against a Model

Formal methods attempt to prove that a property holds for every behavior within a model of the system, rather than for the inputs a test happened to try. Tools such as the Certora Prover and the Solidity SMTChecker check written rules against the contract logic. When a proof succeeds, it gives strong assurance about that specific property.

The limits are equally specific. A proof says nothing about properties nobody wrote, about behavior outside the model, or about assumptions such as an oracle always being honest. Writing good specifications is skilled work, and a vacuous or incomplete rule can pass while the real risk remains. Formal verification is most valuable for narrow, high-impact properties such as solvency, access control, accounting conservation, and message uniqueness.

A passing proof is only as strong as the property and the model behind it. Specification review belongs in the audit scope.

Reusable AI Security Skills Are Becoming Part of the Toolkit

Reusable security skills are also becoming part of researcher-led AI orchestration. Public examples include Pashov Skills, Plamen, Trail of Bits Security Skills, OpenZeppelin Security Skills, and Cyfrin Solskill. These repositories can encode repeatable tasks such as threat-model generation, invariant discovery, focused review passes, or test scaffolding. An auditor may run several independent passes, compare their outputs, and move only well-supported candidates into manual reproduction. Teams should still review each skill's code, dependencies, permissions, license, update history, and data-handling assumptions before using it on sensitive repositories.

The public repositories differ in purpose. Some focus on audit-style review, some on pre-audit preparation, and some on helping AI coding assistants write safer contracts in the first place. The descriptions below reflect what each project publishes about itself.

What Researcher-Led AI Orchestration Looks Like in Practice

In a researcher-led workflow, AI does not decide what goes into the report. The researcher defines the scope and the threat model, chooses which passes to run, and decides what each output is worth. Independent passes are useful precisely because they disagree: a candidate that appears in several unrelated passes and survives manual tracing deserves attention, while a single unsupported claim usually does not.

The practical safeguards are the same ones a team would apply to any third-party code that touches a private repository. Pin the skill version that was reviewed. Run it in a workspace without production keys, deployment secrets, or unnecessary network access. Check what data leaves the machine and under which provider terms. Keep a record of which passes ran on which commit, so a later reviewer can tell how a candidate was produced.

The Researcher Remains Responsible for the Judgment

Tools increase coverage and generate hypotheses. The security researcher remains responsible for architecture understanding, reproduction, exploitability, severity, false-positive filtering, and final judgment. That responsibility includes deciding whether a result is reachable in the deployed system, whether protocol economics change the impact, and whether a remediation addresses the root cause. Kann AI is one optional analysis capability in this broader tool-assisted landscape; it is not presented as a substitute for an expert-led audit or as an automatic part of every engagement.

This division of labor matters for the people who read the report. A finding should describe a real path, with evidence, an accurate severity, and a remediation that was checked against the root cause. A list of unvalidated tool warnings looks thorough but shifts the verification work back onto the protocol team.

“A tool result is a hypothesis. A finding is a hypothesis that a researcher has proven.”

How Kann Audits Uses Tooling in an Engagement

Kann Audits Expert Security Audits are led by security researchers who read the code line by line, trace privileged actions and state transitions, and test the assumptions behind the protocol's economics and integrations. Tooling is chosen for the codebase in front of them, whether that means static analysis on a Solidity repository, invariant suites for an accounting-heavy vault, or symbolic checks on a narrow critical function.

Teams that want automated analysis on its own can use the AI Security Scan, which applies Kann AI to a codebase as a separate service. When teams are choosing between providers, our 2026 smart contract auditing companies comparison explains how different firms combine manual review, tooling, and formal methods.

Questions About AI and Security Tooling in Audits

Short answers to the questions teams most often ask about how auditors use tools and AI.