Deductive Interception
A technical paper on automating formal verification across a whole smart contract codebase, tested against published audits (128 of 188 findings reproduced) and real exploits from 2025 (49 of 50 surfaced on pre-attack code).
The dragonfly doesn't chase its prey. It intercepts it.
A dragonfly reads the fly’s trajectory and flies to the point where the two will meet, instead of trailing behind it. The paper applies the same idea to smart contracts: rather than searching every path a contract could take, the engine solves for the paths a vulnerability has to occupy.
Onchain, a defect is permanent.
An attacker needs to be right once. The code has to be right every time, across every path a user or an adversary can reach.
Surfacing the failures that look likely isn't enough. Likelihood is an estimate, and an estimate that misses one reachable state isn't partially correct. Security for an irreversible system means knowing that specific properties hold under every reachable execution, and being able to show it.
80%
of Rekt-catalogued exploits with a recorded audit status involved audited code in 2024, up from roughly a quarter in 2021.
~20
person-years of proof effort for the seL4 microkernel, against roughly 2 person-years to build it.
$42.6M
drained from Hedgey Finance on Arbitrum in April 2024, from code audited by Consensys Diligence.
From sampling a contract to proving it.
The paper builds its case in six steps, from why current tooling falls short to how the engine performs on real code.
01
The gap · Sections 1 to 3
Today’s tools can only report what they happened to find
Fuzzing samples inputs, static analysis is bounded by its detectors, and AI review infers intent from patterns, so none of them can show that a property holds on every reachable path.
02
The cost · Section 2
Formal verification works, but by hand it doesn’t scale
seL4 took about 20 person-years of proof for under 10,000 lines, and proof size grows quadratically with the specification, which is why the discipline stayed in aerospace and rail.
03
The shift · Section 6
Stop searching everywhere a bug could be and solve for where it has to be
A contract’s reachable state space is finite and mappable, so inferred signals can mark the classes of paths a vulnerability must occupy before anything is attacked.
04
The methods · Section 6
Two methods attack the same code from opposite directions
Bounded Adversarial Verification works inward from signals with known attack strategies, while Counterexample-Guided Invariant Refutation infers the rules the code never states and tries to break them.
05
The boundary · Section 7
AI proposes, and only a counterexample decides
AI suggests invariants and guides exploration, while a deterministic engine settles every finding with an executable trace. The paper is explicit about what the method cannot guarantee.
06
The evidence · Sections 6 and 8
Tested against published audits and real exploits
128 of 188 published audit findings reproduced automatically, 49 of 50 exploits from 2025 surfaced on pre-attack code, and two real incidents traced step by step.
Two real incidents, traced end to end.
Both are backtests: the engine ran on the code as it stood before the incident, with no knowledge of where the bug was. The paper walks through every step, from the first signal to the failing test.
Hedgey Finance · ClaimCampaigns
Token theft after approve
A token-claim contract, audited and used by over a hundred projects. A surplus token approval was exploited in April 2024. From the pre-fix source, with one strategy and no human in the loop, BAV reached the same flaw.
127 min
to find the flaw when run on the pre-attack code
~$44.7M
lost across two chains in the real exploit
Morpho Vault V2 · MetaMorphoAdapter
An invariant the code never stated
The vault depended on an accounting rule that was never written in the code. CEGIR inferred the rule, then found a four-step sequence that breaks it and leaves unconnected depositors absorbing the loss.
4 steps
to break a rule nobody had written down
Medium
engine rating; ChainSecurity rated a Critical in the same class via a different adapter
The paper is explicit about its limits: both studies were run by Olympix, results are bounded by transaction depth and by which properties are inferred, and nothing here claims soundness over a whole system.
Written by the team that built the engine.
Olympix brought together formal methods and cybersecurity researchers and spent its first two and a half years as a research lab, running the engine against real systems before it became a product.
Measured against expert auditors, and against real hacks.
Olympix was benchmarked against two hard baselines: what professional auditors found on 15 already-audited protocols, and every 2025 EVM hack caused by a smart contract bug. Both are backtests on the original code, run with no hints and no human in the loop.
128 of 188
issues that professional auditors had found in 15 protocols, which Olympix also found when run on the same code.
$240M
in 2025 code-level losses Olympix could have prevented, backtested on the pre-attack code of those 50 hacks.
49 of 50
2025 smart contract hacks where Olympix, run afterward on the pre-attack code, flagged the bug that was exploited.
Both studies were run by Olympix, and the whitepaper lists every protocol and commit so the numbers can be checked.
Nine sections, two worked examples, two benchmark studies.
01 Introduction: What it takes to secure a smart contract
02 What mission-critical industries already use
03 Work in this direction
04 The requirement: Formal methods and AI, automated
05 The foundation: Four years of empirical research
06 The Olympix approach: Deductive Interception
07 Inside the engine
08 Evaluation
09 Conclusion: What Deductive Interception is for
Download the whitepaper.
Benchmark the engine against your own external audit.
