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 to verification outsiders. I don’t claim it as a unique invention; however I’ve not seen it documented elsewhere. Methods for verifying software in particular are myriad, and the landscape can be confusing to non-verification folks. We have model checking, abstract interpretation, symbolic execution, auto-active verification, static analyses (including type systems), as well as interactive proof. [Read More]

Breaking a Verified Certifier

Verified Certified Robustness for Neural Networks - Part IV

 Posted on September 17, 2025  |  Toby Murray

This post is the fourth 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 appeared at CAV 2025, and the broader research agenda that that paper initiates. The series so far comprises the following posts: Part I: Verified or Certified Robustness? Why don’t we have both? Part II: When “Verified Robust Accuracy” Isn’t, Actually, Verified Part III: Formally Verified Certified Robustness Part IV: Breaking a Verified Certifier (this post) In the previous posts I explained the formally verified robustness certifier that we built, which implements a provably sound method for efficiently checking the robustness of neural network outputs. [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 broader research agenda that that paper initiates. The series so far comprises the following posts: Part I: Verified or Certified Robustness? Why don’t we have both? Part II: When “Verified Robust Accuracy” Isn’t, Actually, Verified Part III: Formally Verified Certified Robustness (this post) Part IV: Breaking a Verified Certifier In the first post I explained the scalability challenges faced by much prior work on verified robustness for neural networks, and how approaches instead based on certified robustness might provide a way to circumvent those challenges. [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 broader research agenda that that paper initiates. The series so far comprises the following posts: Part I: Verified or Certified Robustness? Why don’t we have both? Part II: When “Verified Robust Accuracy” Isn’t, Actually, Verified (this post) Part III: Formally Verified Certified Robustness Part IV: Breaking a Verified Certifier In the previous post I explained the scalability challenges faced by much prior work on verified robustness for neural networks, and how approaches instead based on certified robustness might provide a way to circumvent those challenges. [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 broader research agenda that that paper initiates. The series so far comprises the following posts: Part I: Verified or Certified Robustness? Why don’t we have both? (this post) Part II: When “Verified Robust Accuracy” Isn’t, Actually, Verified Part III: Formally Verified Certified Robustness Part IV: Breaking a Verified Certifier This first post gives a high-level overview. [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]

What really happened at CrowdStrike and why their proposed plan won't guarantee this can't happen again.

 Posted on July 25, 2024  |  Toby Murray

Yesterday, CrowdStrike released a post that contained a preliminary analysis of the technical causes of last week’s outage. That post finally sheds some light on how this incident occurred. More importantly, it lays out how CrowdStrike is planning to make sure this can’t happen again. CrowdStrike’s plan is totally inadequate in my assessment. In this post, I make sense of CrowdStrike’s explanation of what happened here and explain why their plan going forward is insufficient and what they should be doing instead. [Read More]

Clearing the CrowdStrike Confusion

 Posted on July 20, 2024  |  Toby Murray

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 seemingly not caused by the CrowdStrike update. Updated: 2024-07-21 07:08 AM AEST: in the wake of blog posts from Microsoft, and CrowdStrike. In the last 24 hours there has been much written about the massive outage currently affecting Windows computers worldwide. [Read More]

A CTF Challenge for LLMs for Code Analysis

 Posted on March 19, 2024  |  Toby Murray

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. In this post, I wanted to share a small CTF challenge that I wrote, which I designed to teach students to be similarly skeptical. (Or, if you prefer a more objective framing, let’s say I built the CTF challenge to teach students about the strengths and weaknesses of using LLMs for code analysis and understanding. [Read More]