Smart contract security: static analysis vs dynamic testing

We have all met that version of “done”: the frontend is wired up, the happy path works, the vault accepts deposits — then an integration test discovers that a paused market can still accrue rewards, or a callback turns a balance update into an escape hatch.

That is why smart contract security cannot be reduced to running one scanner before a release. Static analysis and dynamic testing look at the same protocol from different directions. One reads code structure and flags suspicious patterns. The other drives the deployed logic through changing states, looking for a sequence of calls that violates a rule we care about.

Neither is a ceremonial CI checkbox. Used together, they create a much less fragile auditing workflow.

Static analysis: fast feedback on dangerous code shapes

Static analysis examines source code or its compiled representation without executing a transaction sequence. It is the earliest and often cheapest layer of smart contract vulnerability scanning: we ask the tooling to inspect inheritance, function visibility, data flow, external calls, and compiler-level hazards before a human reviewer has spent an afternoon following references across twelve files.

Slither is a strong default in Solidity and Vyper projects. It is a Python-based analysis framework that supports Solidity versions 0.4 onward, works with Hardhat and Foundry builds, and exposes an API for custom checks. That last detail matters more than it may sound. A generic detector is useful; a detector that knows our protocol’s internal conventions is where static analysis begins to feel like part of the engineering process rather than an external gate.

Out of the box, Slither can surface high-impact patterns including:

• arbitrary ERC-20 sends, where a caller-controlled destination or token flow may allow assets to leave a contract unexpectedly;
• abi.encodePacked collision risks, especially when variable-length values are packed and then hashed or signed;
• unprotected state variables, which can turn a missed access modifier into a protocol-wide permission issue;
• incorrect shift operations and other low-level expressions that are easy to gloss over during review;
• external calls made before accounting is finalized, which deserve a reentrancy review even when no Ether is transferred.

The value is speed and breadth. We can run a static pass on every pull request, categorize findings by impact and confidence, and stop repeated mistakes from becoming review noise. For an integration lead, this is also a UX concern in the broadest sense: defects found during development do not become broken transaction flows, confusing wallet prompts, or irreversible user losses later.

But static output needs interpretation. A detector can identify a pattern; it cannot reliably tell us whether the pattern is an exploit in our particular economic and authorization model. A low-level call may be intentional. A state variable may have protection enforced by a modifier inherited three contracts away. Conversely, a clean report means the scanner did not identify the patterns it knows how to model — not that our protocol’s behavior is secure.

A static scanner reads the shape of the code. It does not live through the consequences of state changing over time.

This distinction is where teams often create friction for themselves. They either suppress every warning until the report is green, or treat every finding as a confirmed vulnerability. Neither habit produces better security. The useful workflow is triage: understand the data flow, record why a finding is safe or fix it, and convert recurring protocol-specific risks into custom rules or tests.

Static analysis is especially good at making review smaller

Human audit attention is finite. Static analysis earns its place by narrowing the surface area that needs slow, contextual reasoning.

For example, consider a governance executor that can call arbitrary target contracts after a vote passes. “Arbitrary call” is not automatically a bug; that may be the executor’s purpose. The question is whether proposal creation, vote thresholds, timelocks, calldata handling, and upgrade authority constrain that power as intended. A tool can point us to the call. It cannot decide whether the governance system around it is sound.

That is a recurring theme in automated security auditing. Tools are very good at asking, “Is this code shape dangerous?” Auditors and protocol engineers must answer, “Dangerous to whom, under which state, and after which sequence of actions?”

Dynamic testing: make the contract survive hostile state transitions

Dynamic testing executes the contract. Instead of only inspecting code, we generate transactions, mutate arguments, change caller identities, advance time, vary balances, and chain calls together. This is closer to how protocols fail in production, where the exploit is often not a single bad function but a valid-looking sequence that moves the system into an invalid state.

Property-based fuzzing is particularly effective for this work. Echidna uses ABI-based grammar fuzzing to try to falsify predicates we define in Solidity or assertions embedded in the target. It generates randomized sequences of contract calls and reports the sequence that breaks an invariant.

That is a very different question from the one Slither asks.

Suppose we are testing a lending market. We could encode properties such as:

1. Collateral accounting remains coherent. A user’s debt must not exceed the protocol’s defined borrowing capacity after deposits, withdrawals, liquidations, interest updates, and parameter changes.

2. Unauthorized callers cannot change risk configuration. Calls from arbitrary addresses must not alter oracle sources, collateral factors, pause controls, or privileged implementation pointers.

3. Asset conservation holds where it should. A withdrawal, redemption, or emergency exit cannot transfer more tokens than the caller is entitled to under the protocol’s accounting rules.

4. Paused states really constrain state changes. If a market is paused, every mutating route that the specification says should be unavailable must remain unavailable — including indirect paths through helpers or batch functions.

5. Reward distributions do not create value from call ordering. Claiming, transferring receipt tokens, and updating indexes in different orders must not let a user capture rewards twice.

These are not generic security slogans. They are executable statements about what our protocol promises. Fuzzing turns that promise into something the EVM can challenge repeatedly.

Echidna can collect a corpus of interesting executions, use mutation and coverage guidance, produce source-level coverage reports, and minimize a failing case. The minimized reproducer is a quiet superpower. A fuzzer may spend hours wandering through state transitions; when it finds a break, we do not want a 400-call mystery. We want the shortest sequence that tells an engineer and reviewer what actually happened.

Stateful fuzzing catches the bugs happy-path tests walk around

A unit test usually starts from a carefully arranged state and makes one claim. That is appropriate for validating a feature. But attackers do not respect our test fixture boundaries.

They may deposit through one entry point, acquire shares through another, trigger a callback, alter a market condition, and finally withdraw through a route nobody considered sensitive. Stateful fuzzing lets us explore those transitions without writing every path by hand.

The key word is property. If we tell a fuzzer only to call functions randomly, it can find reverts and edge cases, but it has no clear definition of protocol failure. The quality of the campaign tracks the quality of the invariants.

A campaign that finds no failing invariant is encouraging, not conclusive. It means the configured campaign did not falsify the properties we encoded in the executions it reached. It does not prove that every path was reached or that every meaningful protocol rule was expressed correctly.

That limitation is not a reason to avoid fuzzing. It is a reason to treat invariant design as first-class engineering. If the property is vague, the assurance is vague. If the handler model excludes a critical external actor, the test world is too polite.

Fuzzing does not discover our intended protocol rules. We have to write those rules down before it can try to break them.

Fuzzing vs symbolic execution: related tools, different pressure

“Dynamic testing” can become an overloaded label, so it helps to separate fuzzing from symbolic techniques.

Fuzzers like Echidna execute concrete transactions with generated values. Their strength is that they run the real code paths and can exercise stateful interactions in a practical local environment. Coverage guidance and corpus mutation help them push deeper, but they are still exploring a vast search space.

Symbolic execution takes a different route. Rather than choosing one concrete input immediately, it represents inputs symbolically and asks whether constraints can be satisfied to reach a condition or violate an assertion. Tools often associated with the slither vs mythril comparison sit on different sides of this boundary: Slither is primarily static analysis, while Mythril is known for symbolic execution techniques aimed at exploring EVM execution paths.

Symbolic approaches can be excellent at deriving a concrete counterexample for a reachable condition. They can also struggle when path counts grow, storage is deeply interdependent, or external behavior becomes hard to model. Fuzzing may handle some practical, stateful behavior more naturally; symbolic execution may reason about branches a fuzzer has not stumbled into yet.

We should resist turning this into a tool-ranking contest. The more useful question is: what uncertainty do we have right now?

• If we need broad, fast pattern detection across a codebase, start with static analysis.
• If we need confidence that accounting and permissions survive messy call sequences, write fuzzing invariants.
• If a critical assertion or branch condition deserves exhaustive reasoning under a controlled model, bring in symbolic or formal methods.
• If the concern is economic behavior involving an oracle, a flash loan, governance latency, or a cross-contract dependency, model the actors and assumptions explicitly. No scanner can infer an omitted threat model.

Formal verification and the promise — with boundaries — of SMT solvers

Formal verification is often described as the next level after testing. That is directionally true, but it needs careful wording. Formal tools can prove that a specified property holds for every behavior covered by the model and its assumptions. They do not prove that we wrote the right property, included every relevant external contract, or captured the intended business behavior without gaps.

Solidity’s SMTChecker performs compile-time formal analysis using SMT and Horn-clause solving. Its targets can include assertions, division by zero, constant conditions, empty-array pops, out-of-bounds access, insufficient transfer balance, and arithmetic conditions.

There is a detail worth putting directly into a production checklist: for Solidity 0.8.7 and later, the SMTChecker does not enable arithmetic underflow and overflow checks by default. If those targets matter to the contract under review, they must be enabled explicitly through the model-checker configuration.

This is a good example of why tool configuration is part of smart contract security, not an implementation footnote. A team can say “we ran formal analysis” and still have omitted a category it expected the tool to cover.

Formal verification also depends on supported language features and the fidelity of the model. Assembly can be overapproximated, which may produce false positives. External calls, proxies, token quirks, and cross-contract state all demand modeling choices. In a richer verifier workflow, a rule passes when its assertions hold for all modeled cases satisfying its require assumptions. If those assumptions accidentally exclude the hostile case, we have proved a statement about a smaller and friendlier world.

That can still be extremely valuable. It just means we should read a proof as a precise engineering result, not as a magic seal.

Reentrancy shows why no one layer is enough

Reentrancy remains a useful case study because it crosses every layer of the workflow.

Static tooling can flag external calls, suspicious state-update ordering, and patterns adjacent to known reentrancy hazards. During review, that gives us a map of where to look. The Solidity guidance remains sound: apply Checks-Effects-Interactions — validate inputs, update internal state, then interact externally.

But the difficult cases do not end there. Reentrancy can arise from any external function call, not only from sending Ether. A token transfer may invoke behavior. A hook-enabled asset may introduce a callback. A downstream protocol can reenter through a path that appears unrelated to the original function. Multi-contract effects matter.

Dynamic tests then help us build hostile counterparties: a receiver that calls back during a transfer, a token that behaves in nonstandard ways, an integration that reenters through a public method we assumed was harmless. The invariant should focus on outcomes: no caller can withdraw twice, no share supply becomes inconsistent, no debt is erased without payment, no privileged state changes during an untrusted callback.

Formal reasoning can add confidence around a critical accounting assertion, provided we model the relevant calls and assumptions honestly.

The layered view is not academic. It changes how we respond when a scanner says “external call before state change.” We do not just move a line to silence a detector. We trace the user journey, identify all callback-capable boundaries, fuzz the sequence, and decide whether the invariant is actually protected.

Use standards as a coverage map, not as a stamp

A mature workflow benefits from a shared vocabulary for what has been examined. OWASP’s Smart Contract Security Verification Standard is useful here because it organizes areas that teams routinely miss when they focus only on Solidity syntax: reentrancy, arithmetic, gas behavior, access control, business logic, economic attacks, formal verification, and test-driven development.

The latest stable release identified by the project is version 0.0.1 from September 2024. That should be treated as a practical framework, not an immutable industry mandate. Its value is in making the audit conversation concrete: have we examined authority boundaries? What assumptions do our oracle and liquidation mechanisms make? Where are external calls? Which economic properties are tested, and which are only asserted in documentation?

For teams shipping quickly, a standard can prevent the familiar gap between “we audited the contracts” and “we audited the system.” The first may mean a Solidity-focused pass. The second includes upgrade paths, multisig governance, deployment configuration, trusted roles, off-chain signers, frontend transaction construction, and the integrations users actually touch.

A secure contract that the frontend calls with the wrong parameters is not a successful user journey. Neither is a secure implementation behind an upgrade key with weak operational controls.

A layered workflow that survives contact with a real repository

Let’s make this operational. We do not need to wait for a formal audit to start building useful security feedback into development.

1. Run static analysis continuously. Put Slither into CI alongside compilation and unit tests. Review findings by impact and confidence, but do not confuse suppression with resolution. Keep short written reasoning for accepted findings so the next reviewer is not forced to rediscover it.

2. Write invariants before the protocol becomes large. Start with authorization, asset conservation, solvency, pause behavior, and one or two rules unique to the business model. As new features arrive, add the property that would have caught the most plausible failure.

3. Fuzz sequences, not only individual functions. Deposit followed by transfer followed by withdrawal is more interesting than three isolated tests. Include hostile callers, unusual token behavior where relevant, and state transitions such as pauses, upgrades, epoch rolls, and parameter changes.

4. Turn every bug into a permanent regression. When a fuzzer finds a failure, preserve the minimized case and the invariant that caught it. The fixed issue should become a test the protocol can never quietly reintroduce.

5. Escalate critical claims to stronger analysis. For upgrade authorization, settlement logic, collateral accounting, or a bridge’s message validation, decide whether symbolic or formal verification is justified. Scope the model carefully and review its assumptions with the same skepticism we apply to code.

6. Audit the seams. The riskiest behavior frequently lives between contracts: proxy and implementation, vault and strategy, oracle and consumer, router and token, governance and executor. The seam is where state sync, assumptions, and privilege boundaries tend to fray.

The payoff is not that tooling lets us skip expert review. It gives expert review better inputs, catches routine defects earlier, and makes expensive audit time focus on the questions machines cannot settle for us.

Smart contract security works best when static analysis, fuzzing, symbolic techniques, and formal methods are treated as overlapping lenses. Slither can tell us where code deserves suspicion. Echidna can force our invariants through adversarial sequences. SMT-based tools can establish strong claims inside an explicit model. Human reviewers still have to decide whether that model describes the protocol users will actually encounter.

That is the work: not chasing a green dashboard, but building a system whose guarantees remain intact when the calls arrive in the wrong order, from the wrong contract, at the worst possible time.