Don't Use Ordinary Software to Contain Software-Hacking Agents

Why the Hugging Face-OpenAI incident was foreseeable

 Posted on July 24, 2026  |  Toby Murray

On 21 July, OpenAI disclosed that two of its models—GPT-5.6 Sol and an unreleased, apparently more capable one—broke out of the sandbox they were being evaluated in, reached the open Internet, and compromised Hugging Face’s production infrastructure. Their apparent goal was to steal the answers to ExploitGym, an offensive-security benchmark built by outside researchers that OpenAI was running internally to test their models’ hacking capabilities. Much of the discussion since has been about what this tells us about frontier model capabilities and what happens when “AI goes rogue”. [Read More]

Does the Random Seed Undermine Certified Robustness?

Not if you train for what you certify

 Posted on July 21, 2026  |  Toby Murray

Formal guarantees about programs come with fine print: they are only as solid as the assumptions and mechanisms behind them. Formal robustness guarantees about neural networks are no exception. Much of my recent work seeks to understand how those guarantees can be undermined, and what it takes to make them solid, as described in my Verified Certified Robustness series of posts. That series explains how robustness guarantees can be undermined by bugs in the mechanisms that check them, which we addressed with formal verification, and by floating-point rounding that the theory behind them ignores, which our recent work accounts for with new theory. [Read More]

Fighting Floating Point with Floating Point

Verified Certified Robustness for Neural Networks - Part VI

 Posted on July 14, 2026  |  Toby Murray

This post is the sixth in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent papers A Formally Verified Robustness Certifier for Neural Networks that appeared at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The series so far comprises the following posts: Part I: Verified or Certified Robustness? [Read More]

From Real Arithmetic to Reality

Verified Certified Robustness for Neural Networks - Part V

 Posted on March 24, 2026  |  Toby Murray

This post is the fifth in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent papers A Formally Verified Robustness Certifier for Neural Networks that appeared at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The series so far comprises the following posts: Part I: Verified or Certified Robustness? [Read More]

Formal Verification in the Age of AI

 Posted on March 5, 2026  |  Toby Murray

For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle. The triangle captures a trade-off between three desirable properties: Automation – the verification tool runs largely without human guidance Scalability – the technique works on large real systems Precision – the method can prove interesting properties, such as functional correctness Historically, verification techniques could reliably achieve two of the three, but not all three simultaneously. [Read More]

The Formal Verification Triangle

The Scalability, Automation, Precision Trilemma

 Posted on October 21, 2025  |  Toby Murray

This post is a quick introduction to a concept that I have been using in talks since 2015, to help explain the landscape of formal verification methods and the inherent trade-offs between them. I originally came up with it as a way to contextualise my research to folks outside the formal methods community. However, it may have value beyond that. Formal methods, and the methods for verifying softwarea in particular, are myriad. [Read More]

Breaking a Verified Certifier

Verified Certified Robustness for Neural Networks - Part IV

 Posted on September 17, 2025  |  Toby Murray

Note: this post was heavily updated on March 22, 2026 with the inclusion of the counterexamples against the adversarially-biased MNIST model. It was updated again on July 14, 2026: the counterexample numbers throughout now match the latest version of our paper, in which counterexamples are judged against a fully IEEE-754-compliant execution of each model (see the aside on execution semantics below). This post is the fourth in a series on the topic of Verified Certified Robustness for Neural Networks. [Read More]

Formally Verified Certified Robustness

Verified Certified Robustness for Neural Networks - Part III

 Posted on July 21, 2025  |  Toby Murray

This post is the third in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The series so far comprises the following posts: Part I: Verified or Certified Robustness? [Read More]

When "Verified Robust Accuracy" Isn't, Actually, Verified

Verified Certified Robustness for Neural Networks - Part II

 Posted on June 27, 2025  |  Toby Murray

This post is the second in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The series so far comprises the following posts: Part I: Verified or Certified Robustness? [Read More]

Verified or Certified Robustness? Why don't we have both?

Verified Certified Robustness for Neural Networks - Part I

 Posted on June 5, 2025  |  Toby Murray

This post is the first in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The series so far comprises the following posts: Part I: Verified or Certified Robustness? [Read More]