I want to see a future where software is actually good, and the only path forward is being rigorous. The best way to be rigorous I know of is the use of formal methods. I want to see the software industry adopt better practices.

The prevalent framing of formal verification that I see:

Formal verification is mathematical proof that your code matches the spec.

Garbage spec in, garbage guarantees out. Writing the spec is the difficult part.

Only the scholars with arcane knowledge might write a spec worth a dime.

This framing does not encourage the adoption of formal methods in the industry. It invokes a mythical artifact called “the spec”. The CXOs have never seen a spec, and they don’t know anyone who can make or scrutinize the spec. The only success stories they’ve heard of are from teams of Ph.D. researchers, or megacorps investing millions of dollars. It relies on the authority of renowned scholars to produce such a thing, and the results are not even guaranteed.

To ease buy-in, we need to show an adoption path with clear, incremental steps, each with costs and benefits. We need to be able to show how to apply formal methods to a small part of a system, and the guarantees that provides.

Here is my proposed framing of formal verification:

Today, you don’t have a way to ask questions about how your software behaves on all inputs. Formal methods allow you to ask questions about your program, and get verifiable answers. The more questions you answer about your software, the more certain you are that it does the right thing. This process has compounding gains — the more questions you answer, the easier it is to answer more. To get to a fully verified system, you need to ask the right questions. Figuring out the right questions is an iterative process.

Here’s a proposed process that comes out of that framing:

1. Describe a part of your system in a language capable of formal reasoning. (Lean/Rocq/Isabelle)

It could be an AI translation from prose or code, or a hand-rolled or reused model. A target could be a parser, a synchronization protocol, or a state machine for an item in the shopping cart. This step forces you, or the coding agent, to express your system in a mathematical way. A way that can be mechanically reasoned about. It’s OK if the model is not perfect. The differences can be reconciled later.

Benefits: this step uncovers ambiguities, and possibly some bugs. Most importantly, it unlocks the following steps. It gives you the capacity to ask questions about your model, and get verifiable results.

2. Reconcile the differences with differential testing.

Once you have an executable model, you can check it by running an existing test suite. Write a differential fuzzer between the model and the original code. You will find a lot of bugs. In my experience, mostly bugs in the original code. It’s extremely valuable to find bugs before your adversaries do.

Benefits: you now have a powerful bug-finding tool, and some reassurance that the model correctly represents your system.

3. Write down and prove some theorems about the model.

Ask an important question about the system, and formulate it as a theorem. You can pick any theorem that exercises a sizable portion of your system. Take a test and replace a concrete value with a ∀-quantified variable. Prove that a parser returns success iff the input conforms to the BNF grammar. Prove that decompress(compress(x)) = x or deserialize(serialize(x)) = x. Prove that an item in the shopping cart is never both checked out and removed. Prove that a synchronization protocol is free of data races, and doesn’t lose events. These used to take Ph.D.-months to years. Now your AI subscription can write proofs in hours to days. It’s OK if your theorems are not comprehensive. Just asking some questions will give you reassurance about those properties. You will find bugs, and the bugs you find will likely be more subtle than the bugs found in step 2. Treat your theorems as more powerful tests.

Benefits: you have some proofs about your model. It’s not clear if those proofs cover your requirements. Once you have some proofs, a whole new world opens up, which allows you to answer more questions faster.

4. Prove the correspondence between the model and the original code.

This is an active area of research, and there has been some success recently, with proofs about real compiled code (ant-1, alphaproof-1). At the moment, doing this for existing production code is available mostly to megacorps and well-funded labs, and people are actively working on making it more viable. We will get better toolchains and better processes, likely in the near future. This level of proof gives remarkably high confidence that your model corresponds to your system.

Benefits: now the proofs you wrote previously apply to your actual code. Maybe they even apply to the binaries you ship. Previously, proving any deep property about the runtime behavior of a program was practical only for a handful of heroic projects.

5. Actively work on finding more theorems about security properties of your system.

If you’ve arrived at this step, your software provably has the properties you have listed.

As time goes on, we will discover more security properties that a given system should satisfy. I expect there to be well-curated, comprehensive libraries of theorems about different kinds of systems that security or compliance would require you to prove.

In this framing, the spec is merely a set of theorems you chose for your system. The spec is no longer a mythical artifact nobody can produce. Yes, you need to be very careful about the theorems you choose. Yes, you will likely miss some properties your system should have. That’s where the specialists come in and work with you to show you which properties are missing. This contribution is incremental, and doesn’t gatekeep you from other benefits. We don’t yet know all the qualities that your system should satisfy, but we will do our best to discover and document them.

Benefits: you can prove that your system satisfies a well-curated list of requirements. When combined with whole-system modeling, this is the highest level of assurance I know of.

---

This concludes my proposed framing of formal verification. I believe the prevalent framing and the proposed framing have the same end state. That state is a well-thought-out, curated, comprehensive spec of the system, with a formal proof that the system implements the spec.
The crucial difference is that the original framing doesn’t provide an incremental path to get to that state. It discourages people from even trying.
In contrast, each step above gives more benefits than the previous one. The new framing is much easier to sell to the industry.
Doing formal methods is worth it, and it’s worth doing badly, and incrementally. It will move you to a better place.

I view formal methods through the lens of the scientific process. “Here’s my understanding of the system. I will ask questions. I will perform experiments. I will update my understanding.” Through this lens, formal methods allow me to get answers in a very reliable way.

I view the spec through the lens of a software engineer. We don’t know all the security properties our system needs to have. We need to have a process that allows us to prove more security guarantees, and reconcile our software with them. We need to have a way to curate, discuss, and reuse the theorems that show important properties.

Let’s make software better.

Recently, Casey Muratori has implemented a proof-of-concept terminal, which is designed around fast input processing and rendering. This is an important and commendable effort, since the vast majority of software performs tens to thousands of times slower than it can.^{[citation needed]}

One of the design choices of refterm is to use a hash table to cache glyph rendering. The key in this table is the UTF-8 string of a single glyph. To avoid string allocations, the hash value of the glyph bytes is used as a key instead.

When Casey got asked about the possibility of hash collisions on stream, he responded with a claim that the hash function used in refterm is “a strong hash”, and the complexity to find collision is about 2^64 operations. After analyzing the code for the hash function used in refterm, a few flaws were found in the hash function, and O(1) attacks were discovered.

I wanted to know what data Oculus Runtime sends home. To do that, I’ve implemented a custom tool to extract TLS keys from a running Oculus Runtime instance.

You can find my findings below.

I want to be able to inspect the traffic of programs running on my computer. I don’t really trust those programs and ideally I’d like to put nearly all of them into a high security jail.

One of those programs is Oculus software. There are a few reasons why I want to be cautious about Oculus software.

This post is heavily inspired by Tom Stuart: Programming with noting, William Byrd on “The Most Beautiful Program Ever Written”, Guowei LV – The Most Beautiful Program Ever Written, John Tromp – Binary lambda calculus.

When I first learned about Lambda calculus, I was amazed by a strong mathematical basis for anonymous functions used in many languages.

Then I wondered: what’s the simplest way to represent lambda functions as data?