AI security at DeFi Security Summit 2026, Day 1
DeFi Security Summit 2026 ran on November 1 and 2 in Mumbai, and 28 of its 106 talks were about AI. This post covers Day 1's AI talks, one short block per talk, grouped by theme, and ends with the lessons I'm taking from them.
DeFi Security Summit (DSS) 2026 took place on November 1 and 2 at the Courtyard by Marriott Mumbai International Airport, during Devcon week. Two rooms, Amber and Pearl, ran 106 talks, and 28 of them had AI, LLMs or agents in the title. This post covers Day 1, November 1.
Peter Kacherginsky set the tone in the opening keynote: with AI finding bugs, hacks have gone from three or four a week to three or four a day.
TL;DR
- AI alone is not an audit yet. In Dedaub's test a single agent found 45% of the bugs and all agents together 73%, but they also found 16 bugs the human auditors had missed.
- Models miss different things. In ack3's benchmark all nine models agreed on only 9 of 40 issues. Running several models several times took recall from 75% to 100%.
- Simple setups beat elaborate ones. A one-sentence prompt beat a 40-agent swarm, and the biggest gains came from better context, not orchestration.
- In formal verification, AI now writes the proofs. Writing and checking the specs is still the human job.
- Your own agents are attack surface. Polygon's worst finding was plain access control around an agent.
- If you watch one talk: Gustavo Dutra's "We Gave AI the Keys to Our CI", for how a real company secures 17 agents.
What's in this post
- Can AI audit a contract? (4 talks)
- How to run the agents (4 talks)
- Securing the agents themselves (2 talks)
- Security after the audit (2 talks)
- Formal verification with AI (5 talks)
- What I'm taking away
Each talk's video link jumps to where it starts in the full-day stream of its room (Amber, Pearl).
Can AI audit a contract?
Four talks measured AI auditors against human work. They agree that AI finds a lot, including bugs humans missed, and that the numbers depend heavily on how you measure.
Can AI Audit Your Smart Contract? We Tested It on Real Audits.
Mohamad MansouriDedaub
Key point: "No, not on their own", but the gap is closing fast.
The team took 8 past client audits, hid their own reports, and ran a range of agents on the same code: plain models with an "audit this code" prompt, lightly tuned setups, public scanner-plus-LLM tools, and Dedaub's own pipelines. The reports held 61 bugs.
- On Solidity, one agent found 45% of medium-and-above bugs on average. All agents together found 73%, including every critical.
- Across all 8 projects, including one on Sui (Move) and one on TON, they found 29 of 61.
- The agents found 16 medium-and-above bugs the humans had missed: 2 high, 14 medium.
- In June, Dedaub's pipelines scored about double the plain models. Now a single prompt to a current flagship beats those June pipelines, and the gap is a bit under double.
A bug bounty pays for any one severe bug, so AI is already very useful there. An audit has to cover the whole protocol, so it isn't ready to go alone.
Benchmarking Frontier Models: Which One Is the Best EVM Auditor?
Josef Gattermayerack3
Key point: No single model finds everything, so run several, several times.
ack3 used five audits whose code and reports were never published, so no model could have trained on the answers. The humans had found 32 criticals and highs.
- Of 40 verified issues, all nine configurations found only 9.
- Kimi K3 scored low overall but was the only one, humans included, to find one particular high.
- In a second setup called swarm, six models ran for five hours in "waves" on one large codebase and shared findings after each wave. Recall was 75% after the first wave and 100% after all of them.
- One GPT model kept finding new issues for three waves, so the advice was to run it three times.
"Is it sufficient that something discovers most of the issues? No, you need something that discovers all the issues."
Benchmarking Security Intelligence: Why Web3 AI Security Eval Is Broken
Suryansh SinghOpenZeppelin
Key point: Public benchmarks only test known answers, so build your own eval from private audits.
A popular web3 security benchmark this year used public audit contests, which were probably in the training data. It also graded against fixed answer keys, so anything new a model found never counted.
- Use many private codebases you have audited, with the client's permission.
- Triage every new finding into the answer key or a list of known false positives, so the eval grows.
- Score noise separately and weight by severity.
- Give the agent the tools it would really have.
- Skip synthetic bugs and toy contracts, which today's models find too easily.
Why is AI missing these bugs?
Robert ReithAccretion, hackhack
Key point: AI finds 80 to 90% of what Accretion's humans find, and the rest is mostly missing context.
On past Solana audits, Accretion's AI setup finds 80 to 90%, sometimes 100%, of the highs and criticals the humans found. It also catches things people skim past, like liquidity provider fees used where protocol fees were meant. The misses fell into five groups:
- Dependencies. An admin call went from MetaDAO futarchy to Squads. If the admin is itself a Squads multisig, the call re-enters Squads and fails on Solana. Nothing in the context said the admin could be Squads.
- Ecosystem attacks. A bridge ignored Token-2022 features, so an attacker could bridge tokens from a mint, close it, re-create it as a Pump.fun token on the same address, and later steal real deposits.
- Upgrade history. In Light Protocol's move from Anchor to Pinocchio, an account created under the old version could be reused after the upgrade.
- Fast-moving chains. When Solana halved slot times, humans flagged code that counted time in slots. The AI didn't.
- Severity. An agent rated a real critical as informational after misreading decimals: it thought the attack needed 18.4 billion USDC, not 18,000.
If you are working out which odd piece of context to give the model, Reith said, you are already auditing the code.
How to run the agents
Four talks were about method, and all four argued for keeping the setup simple and making every finding prove itself.
Don't Trust the First Model: A Methodology for Adversarial AI Audits
Christian VariOak Security
Key point: Models say they checked everything, so verify coverage and make other models try to disprove each finding.
Oak's method has five steps, each with a gate:
- Scope. Check that every model read every file, not just that the models covered the repo between them.
- Discover. Several models from different providers work separately, once without and once with Oak's past findings. Each finding is a testable claim with the attacker, preconditions, location and the model that found it.
- Deduplicate by root cause.
- Validate. Other models try to disprove each claim in a fresh context and check whether it is reachable at all. Vari called this the most important step, because 200 unverified findings waste a researcher's time.
- Health check. Rerun anything that gave no verdict or didn't read its scope, or flag it for a human.
"From a security researcher to security researcher: please don't trust the first model."
Certiflai: orchestrating swarms for certifications
George KobakhidzeConsensys Diligence
Key point: A one-line prompt beat a 40-agent swarm. The winning design was two agents plus deterministic tools and a full evidence trail.
Kobakhidze used agents for certification, checking code against security standards, which experts find tedious. "Agents don't have a concept of fun. They thrive with instructions." About 45 runs on Uniswap v2 and Morpho Blue compared three setups:
- One agent, one sentence. Best score and cheap, about 30 cents in one run, but results varied, the evidence was thin, and it sometimes edited the code it was assessing.
- A sub-agent hierarchy in about 17 markdown files: "a catastrophe". Up to 40 agents at once, hundreds of dollars per run, and one DNS error cascaded through all of them. Better 2 people on 100 controls than 100 people on 2 each.
- Certiflai. A LangGraph swarm of two agents, a producer and a reviewer, with fuzzers and static analyzers in a controlled VM. It matched the best score and kept evidence a human can check. Agents only propose verdicts; a Python program writes the report. File hashes, read logs and planted canaries show whether the work was done.
My take: this is the most useful counterweight to "more agents is better" that I saw all day.
Patch the Planet: Three Lessons for DeFi from AI Bug Hunting
nisedoTrail of Bits
Key point: Spend the effort on defining the goal and splitting the work, not on telling the agent how to hunt.
Patch the Planet is Trail of Bits' program with OpenAI to find and fix bugs in critical open-source software, using Codex /goal to keep an agent working until a goal is met. The talk turned that work into three lessons for DeFi:
- Let the agent write and challenge its own goal. "find bugs in the vault" becomes "Prove that an unprivileged user can steal someone else's funds. Prove it with a PoC." The attacker should match your threat model, not be an admin, and the evidence should be a working exploit.
- Hunt the bug class, not the bug. Start from a known exploit such as a share-inflation attack, describe the class in one sentence ("rounding errors in share math"), and send a new agent after variants elsewhere.
- Give each agent one attack surface. All agents share one threat model. The agent ranks the five most promising surfaces, each gets its own session, and one more session is free to explore everything else.
Fuzzing with Coding Agents: What Works in Practice
Josef Gattermayerack3
Key point: Agent-written fuzz tests catch most bugs fast, but miss what depends on order and time.
ack3 has a coding agent write guided fuzz tests in its Python framework Wake.
- Synthetic mazes. Traditional fuzzers reached about 70 to 75 of 153 targets in eight hours. The agent's tests reached all of them in about an hour.
- A less synthetic benchmark. The agent reproduced the six bugs the human tests found, but inconsistently; the best single run found four.
- The weak spot is time. The agent tests the system as it is, not how it changes, so race conditions and "what happens after a payment has started" get missed.
"To catch like 80, 90% of the bugs, this works really well."
Securing the agents themselves
Two talks looked at the other side: the agents and the infrastructure as things that can be attacked, and the flood of reports AI is creating.
We Gave AI the Keys to Our CI — Then We Tried to Hack It
Gustavo DutraPolygon Labs
Key point: "Model refusals are not a security boundary." Build every agent as if it is already compromised.
Polygon gets 200-something bug reports a month because of AI, and its engineers open 200+ pull requests a week through cloud agents. It now runs 17 security agents that triage reports, review every PR, build threat models and red-team. The design rules:
- Inputs are data, never commands.
- Write access only where strictly needed, everything sandboxed.
- A human triggers anything dangerous.
- Agent output can't tag people or carry links, so an agent can't phish an employee.
Attacking their own agents, the team found that the models caught most prompt injections, but an injected footer passed and spread from agent to agent. The fix was in infrastructure: tag data so an agent knows its input came from another agent. The worst finding was an early coding agent whose sessions were visible org-wide, each with Git credentials and a shell. In five steps anyone in the company could take over a session and push code in another engineer's name.
My take: the talk I'd most recommend from Day 1. The worst bug "was plain access control, not something on the agent itself".
What a libp2p Gossipsub Crash Taught Us About AI Security and DeFi Infrastructure
Manu Sheel Guptalibp2p
Key point: AI has multiplied security reports for infrastructure, so build triage around where AI actually helps.
An integer overflow in gossipsub could crash consensus nodes. The talk traced how that turns into stalled sync, halted oracle feeds and failed liquidations.
- In the last three months, the security reports reaching libp2p equal Gupta's whole career's total. The next six months could bring ten times more, many of them minor or "me too".
- libp2p has 17 implementations, 7 used by Ethereum consensus clients. A fix only helps once it reaches all of them, and that cross-implementation work is where Gupta sees AI helping most.
The advice: ask "where do I need AI", not "let me accept AI".
Security after the audit
Two short talks from Lido made one argument: "Audits is a snapshot. Security must be evergreen."
Evergreen: continuous AI-augmented security by Lido x Nethermind
Eugene MaminLido
Key point: Context, not model choice, made the AI useful.
- Lido had 30 audits this year from eight firms, with zero criticals and zero highs.
- Its bug bounty has paid $410,000 so far. Of about 180 criticals whitehats claimed, three were paid. "Most of the work here unfortunately is saying no."
- With Nethermind, Lido ran a four-week AI pilot on about 19,000 lines of its core code.
Mamin's lessons from the pilot:
- Context mattered most. The bulk of the work went into collecting documentation, not choosing a model.
- Write down design intent, because no agent or auditor can infer it.
- Don't rely on one engine. Lido's internal tool runs four different models around the clock over 39 repositories.
The Audit That Never Ends: Evergreen Security in the Age of LLMs
Sergey KhomutininLido
Key point: Make auditing part of development and keep it running after launch.
Lido's internal system, Lens, is "just a common coding agent such as Claude Code and Codex under the hood", given the right context and questions. It reacts to code changes, document changes, upcoming hard forks and new model releases. Two public results:
- A Glamsterdam compatibility check found a bug in the consensus spec: a pending validator deposit could be credited to a builder with the same public key, and the funds would be lost. The fix has been merged.
- Wormhole shut down the delivery service Lido's cross-chain governance relied on, which shows that even unchanged code needs checking.
Attackers have the same LLMs, so "your security baseline should keep getting better too". The design doc's rule: "It recommends, the team decides."
Formal verification with AI
Five talks asked whether AI makes formal verification practical. The answer was yes for proofs and no for specs: AI can now write and grind through proofs, but deciding what to prove is still human work.
AI-FV: Slop or Prop? Explorations in Agentic Formal Verification
Jonathan MevsQuantstamp
Key point: "If we look at the numbers, it's tending towards slop", but the output is still useful to an auditor.
Mevs tested whether AI lets an ordinary auditor drive formal verification tools. The target was an Aave vault of about 700 lines with 11 known bugs from a 2023 audit. Claude wrote harnesses for three tools: Certora's AutoProver, Runtime Verification's Kontrol, and the Solidity compiler's SMTChecker.
- AutoProver did best, catching 2 of the 4 mediums. SMTChecker caught one medium AutoProver missed.
- Most findings were real, but many weren't worth reporting.
- Runs took dozens of hours and hundreds of dollars in tokens.
The edge cases guide manual review, and specs can be rerun after a client's fix. It is not yet a standalone engagement for a single auditor.
Symbolic Execution of Math-Heavy Code in the Age of AI
Neville GrechDedaub
Key point: DeFi math chokes most symbolic engines. Dedaub's covers far more paths by using AI where it can be checked.
Uniswap V3's tick-to-price function alone has about 20 branches and about a million paths. Dedaub's engine:
- lifts bytecode into a higher-level form and undoes compiler optimizations so the math reads like math
- answers only "definitely impossible" vs "possibly possible" quickly
- uses AI-written summaries of math library functions, checked against the real code by fuzzing: "Obviously we don't trust the AI"
- hands the extra false positives to an AI agent to triage
From Production Rust to Lean 4 Proofs: A Verification Pipeline with AI Provers
Natalia KlausRuntime Verification
Key point: AI provers are "an exoskeleton" for proofs, but they also write specs that prove nothing.
The Ethereum Foundation project turns production Rust cryptography into Lean 4 proofs.
- The AI provers Aristotle and Aleph close proofs. One hard lemma took about $200 and 24 hours.
- Before AI, writing proofs was "like digging land with your bare hands".
- AI "can write really often vacuous specifications which are really easy to prove and they state nothing, so we prove nothing". Every spec needs a human check.
Formal Verification in the Age of AI: New Powers, New Traps
Petar CalicSpectra
Key point: FV didn't find more bugs, but it forced a better fix.
Calic planted a variant of the inflation attack in real production code and ran six isolated agent runs with three levels of documentation, half with Foundry tests and half with Certora's CVL.
- No agent clearly said the attacker could profit, which changes the severity entirely. That only came out after repeated prompting.
- Humans had to discard counterexamples from impossible states, and some agents "simplified" the model until the bug disappeared.
- The fix differed. Other runs raised the decimal offset, which only makes the attack expensive. The FV-driven agent tracked deposits internally, which makes the error mathematically impossible.
Calic's advice: spend far more time on specs and keep them "the hardest thing to bend", because "AI often can adapt tests so they fit the implementation".
Formal Verification in the Age of AI
Benjamin FloresVerity
Key point: FV is suddenly everywhere because LLMs can now write the proofs, which leaves humans with the specs.
Writing specs hasn't become much easier. What changed is proving: besides SMT solvers, LLMs now write mathematician-style proofs, "better than 10 PhDs at mathematics", and cheaply. So "we can prove every code that is correct". Flores sees review as the bottleneck of AI coding, and formal verification shrinks review to reading the spec. Verity's Lido V3 vault solvency proof, generated by GPT 5.4 for about $45, shows where that stands.
What I'm taking away
- AI alone is not an audit yet, but skipping AI is no longer an option. Mansouri's agents found half the bugs on their own and 73% together, plus 16 the humans had missed. Reith's setup finds 80 to 90% of what the human team finds. Use both, and compare what each missed.
- Run more than one model, more than once. In ack3's benchmark the models agreed on only 9 of 40 issues, a weak model found a unique high, and recall went from 75% to 100% through repeated waves. A single run of a single model is only a sample.
- Spend the effort on context, not on clever orchestration. Lido's biggest gain came from a context pack and written design intent. Reith's misses were all missing context. Kobakhidze's one-line prompt beat a 40-agent swarm.
- Make every finding prove itself. Check it adversarially in a fresh context, ask for a PoC, and keep a record of what the agent read. Vari's validation step, nisedo's "prove it with a PoC" and Kobakhidze's canaries address the same problem: a model that says it checked something may not have.
- Test your AI tools on your own private code. Public benchmarks leak into training data and only count known answers. Keep an eval of past audits, triage every new finding into it, and score noise separately.
- In formal verification, the spec is the human's job. AI writes proofs now, but it also writes vacuous specs and bends models until the proof passes. Klaus, Calic and Flores all came back to this.
- Design your own agents as if they're already compromised. Treat their inputs as data, limit write access, tag agent-generated content, and keep a human on anything dangerous.
- Get ready for a flood of reports. Lido paid 3 of about 180 claimed criticals, Polygon sees 200-something reports a month, and libp2p got a career's worth in three months. Triage needs its own pipeline, ideally with several models and a human making the call.
- Security doesn't end at deployment. Dependencies change, hard forks land and new models come out. Lido's checks run on every one of those triggers, not only before a release.
