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]

The Real Danger in SignalGate

No, it's not just the risk of hacked devices

 Posted on March 27, 2025  |  Toby Murray

There has been much heat and light written in the wake of (what is now being called) SignalGate. I, myself, wrote in The Conversation about what this incident teaches us about the dangers of shadow IT, and the need for usable security. But this post is not primarily about that. Many people have noted that this incident was dangerous not because Signal was being used (as opposed to any other end-to-end encrypted messaging platform). [Read More]

On the rise of Machine Learning through the lens of Music Source Separation

 Posted on January 17, 2025  |  Toby Murray

Douglas Adams famously quipped that we treat with skepticism any technology invented after our 35th birthday, but anything invented before is unremarkable. It happens that I joined University of Melbourne mere weeks after I turned 35. I am ashamed to say that up until that time (and for a little while after) I had been far too skeptical and dismissive towards machine learning research and technology. Since then, I’ve come to repudiate much of my ignorance about ML (which, naturally, was the source of my skepticism); though I remain an ML novice. [Read More]