Toby's Blog

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.

Formal guarantees about programs come with fine print: they are only as solid as the assumptions and mechanisms behind them.

This post is the sixth in a series on the topic of Verified Certified Robustness for Neural Networks.

This post is the fifth in a series on the topic of Verified Certified Robustness for Neural Networks.

For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle.

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.

Note: this post was heavily updated on March 22, 2026 with the inclusion of the counterexamples against the adversarially-biased MNIST model.

This post is the third in a series on the topic of Verified Certified Robustness for Neural Networks.

This post is the second in a series on the topic of Verified Certified Robustness for Neural Networks.

This post is the first in a series on the topic of Verified Certified Robustness for Neural Networks.

There has been much heat and light written in the wake of (what is now being called) SignalGate.

Douglas Adams famously quipped that we treat with skepticism any technology invented after our 35th birthday, but anything invented before is unremarkable.

Yesterday, CrowdStrike released a post that contained a preliminary analysis of the technical causes of last week’s outage.

Updated: 2024-07-21 08:45 AM AEST: Clarifying that the Microsoft Azure outage in its Central US region began before the CrowdStrike update was pushed and so, despite claims in The Conversation from an Australian academic to the contrary, that outage was s…

Readers of my recent post, which tried to shed light on the use of LLMs to generate fuzzers, may have caught my undisguised skepticism towards the use of LLMs for static code analysis, especially for security vulnerability detection.

LLMs seem surprisingly good at many things.

On Thursday Australia’s second-largest telecoms company, Optus, announced it had suffered a major data breach that had compromised sensitive customer information.

If you’ve read my recent posts, you’ll know I’ve been thinking a fair bit about Wordle.

Programmers love to set each other challenges, particularly ones that involve writing small programs whose jobs are seemingly simple but turn out to be quite difficult to write without making any mistakes.

Semester starts next week.

tl;dr This post is about a recently published paper that takes a critical look at formal proofs as a means to assure the security of software systems, which I authored with Paul van Oorschot.

Academia is sometimes portrayed as a noble pursuit.

When I was a Computer Science undergraduate, at the turn of the millennium, by far the least engaging subjects that I studied were those on Software Engineering.