Perri Adams on Proof Engines, LLMs, and the New Era of Verifiable Code

From Three Buddy Problem by Security Conversations

May 26, 2026 · 40 min

About this episode

Perri Adams discusses the relevance of proof engines and formal methods in the context of LLMs and AI security.

( Presented by TLPBLACK : A cybersecurity intelligence platform focused on sharing curated, high-sensitivity threat insights and research with trusted security professionals. ) Three Buddy Problem x Ekoparty Miami : Perri Adams of DARPA AIxCC fame joins the show to chat about proof engines, formal methods, and why LLMs just made a once-niche corner of computer science suddenly essential. We get into why verifiers and proof engines are the key to effective AI, why vulnerability research is so far ahead of threat intel, and the case for baking security checks directly into code generation tools like Claude Code and Codex. Plus, designing a multi-million dollar challenge that's allowed to fail, the Mythos "too dangerous to release" debate, and musings on every LLM-discovered bug being a public bug by default. Cast: Juan Andres Guerrero-Saade , Ryan Naraine and Perri Adams . Timestamps: 0:00 — Introductory banter 1:09 — Why LLMs just made formal methods relevant again 4:03 — Proof engines, explained 8:43 — Can a layman grab this fire? The calculus problem 11:58 — Vuln researchers are scrappy kids with a trust fund 14:55 — Pitching AIxCC inside DARPA: hard sell or easy sell? 18:00 —…

People in this episode

Hosts: Juan Andres Guerrero-Saade, Ryan Naraine

Guest: Perri Adams

Topics covered

proof engines
LLMs
verifiable code
AI security
vulnerability research
formal methods

Keywords

proof engines
LLMs
verifiable code
AI security
vulnerability research
formal methods
DARPA AIxCC

Mentioned in this episode

Organizations: DARPA AIxCC

Products: Claude Code, Codex