Aengus Lynch, Ph.D

I'm a member of technical staff at Theorem in San Francisco, formally verifying software to prevent mass AI-enabled hacking. I completed my PhD in AI research at University College London in 2025, with the thesis The Persistent Vulnerability of Aligned AI Systems.

Essentially all of the misalignments we simulated in the Agentic Misalignment papers (2025, 2026) have now happened in the wild. We cannot reliably align AIs, our controls cost time and compute that companies racing each other struggle to sustain, and recursive self-improvement will make restraint hardest to afford just when we need it most. The AI safety stack is buckling under pressure, so we should build safety that scales.

Cyber is now in turmoil, and my latest post with Anthropic's Frontier Red Team offers a beacon of hope, because we can eliminate whole classes of bugs with proofs. I contributed to OSS Verify, which runs the same pipeline free for open-source projects. Our plan for the rest of the stack is Bootstrapping the Verified Software Stack.

To get up to speed on my work, read No More Warning Shots, then the formal verification post, then my PhD thesis, and here are the papers I'm most proud of:

• Automated interpretability. ACDC recovered a hand-found GPT-2 Small circuit automatically, selecting 68 of 32,000 edges (NeurIPS 2023 spotlight).
• Training on model internals. Targeted latent adversarial training beat the R2D2 jailbreak defense with orders of magnitude less compute.
• Automated jailbreaking. Best-of-N random prompt augmentations jailbroke GPT-4o 89% and Claude 3.5 Sonnet 78% of the time.
• Blackmail in LLMs. Across 16 frontier models in Agentic Misalignment, Claude Opus 4 and Gemini 2.5 Flash blackmailed in 96% of runs.
• More misalignment. In Summer 2026, Claude Opus 4.8 as a judge mislabeled 74.4% of transcripts when the true label would train against its refusals, and 3.3% when it would not.
• Formal verification. 239 entry points across 123 libraries proved crash-free, with hundreds of bugs found.

I told the UK Parliament's Business, Innovation, Science and Trade Committee that the biggest risks from AI come from building it very, very quickly, and recommended that governments mandate embedded evaluators who pre-commit to investigative claims (video, thread). I walked Scott Phoenix of 50Y through the blackmail research in The AI Researcher Who Caught Claude Blackmailing, and explained on MTS why automating alignment will be slow while we can barely measure it.