A $475 Million Typo
How a flaw in a chip's arithmetic, a recycled line of rocket code, and a hidden timing glitch reveal why testing alone can never make software safe.
Read on SubstackPosts
Everything I write in one place: technical posts published here on this site, and plain-English explainers about formal methods on Substack — why software fails in expensive ways, how we can prove that it won't, and what any of that means for AI.
Highlights
Putting Your Google Scholar Stats on Your Own Website
How to keep a citation count, h-index and publication list current on your own site without touching them — by letting the site scrape your Scholar profile for you.
Read on SubstackGoogle Scholar Orderer: A Research Tool
A browser plug-in that sorts Google Scholar results by citation count and badges venues by ranking — and the story of building it.
Read on SubstackWhy Formal Methods?
-
Welcome — or, Why I'm Trying to Explain Formal Methods to You
I work in a small, jargon-heavy corner of computer science called Formal Methods. This is an attempt to make it make sense to someone who doesn't.
-
How a flaw in a chip's arithmetic, a recycled line of rocket code, and a hidden timing glitch reveal why testing alone can never make software safe.
Foundations
-
Transition Systems: The Hidden Grammar of Everything
A thermostat, a vending machine, and a traffic light all turn out to be the same kind of thing, and once you see it, you can reason about almost any machine on Earth.
-
Model Checking: Every Possible Future
A machine that plays out every way your system could behave, and when something breaks, hands you the exact sequence of steps that broke it.
-
Mathematicians trust other mathematicians to catch their mistakes — but what if a small, utterly reliable program checked every step instead?
-
Proofs vs Testing: The Caveats
A proof can guarantee a system never misbehaves, but we are really speaking about its model, only against a specification, and that fine print is important.
Solvers & Tools
-
How a problem proven to be among the hardest to solve is one of the most useful tools we have.
-
SMT Solvers: SAT That Learned Arithmetic
When true-or-false isn't enough, we can hand the problem to a solver that understands numbers, enabling powerful results.
Verifying Neural Networks
-
How invisible noise can turn a confident, accurate AI into a confidently wrong one and why that should change how you think about "accuracy."
-
What Would It Mean to Prove an neural network Is Safe?
If "99% accurate" isn't a guarantee, the alternative is a promise that covers infinitely many inputs you never tested — here's what that promise actually says.
-
How Do You Prove Something About a Million Images at Once?
You can't run a neural network on infinitely many images — so instead of tracking every input, you track a shape that contains all of them and push the shape through the network.
AI & Reasoning
-
Today's image-reading AIs can describe a photo, pass exams, and write you a sonnet — so why do they fall apart on a number puzzle a ten-year-old can finish?
-
Neuro-Symbolic AI: Eyes and a Rulebook
The fix for an AI that can't solve a puzzle isn't a bigger AI. It's to chose specialized systems for specialized jobs.
-
An AI Solver That Catches Its Own Mistakes
Given a messy handwritten puzzle one may occasionally misread a digit. But we can use logic to notice, point at a culprit, and fix it.