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

(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 — Designing a challenge that's allowed to fail 22:06 — Inside Team Atlanta's 150-page winning system 24:00 — Why this is bigger for defense than for offense 31:49 — Mythos, safeguards, and "every LLM bug is a public bug"