This post stems from a recent conversation with Heidi Howard where we talked about the changing role of TLA⁺ & finite-state model checking in both research and industry. For a long time, users of TLA⁺ (or other formal specification languages like Quint) had a classic 80/20 payoff/effort choice available to them: they could either put in a large amount of effort to formally prove their system properties correct with 100% confidence, or for 20% of that effort they could model-check their system and get perhaps 80% of that confidence. This economic calculation might no longer hold. The summer of 2026 has seen fairly astonishing improvements in the field of automated theorem proving. System correctness theorems are generally shallow but broad, eschewing deep math knowledge but requiring many tedious steps. Thus people formally specifying their system have a new option, where they can pay some amount of money to various companies in exchange for a decent chance of getting an incomprehensible auto-generated correctness proof for their system properties. Assuming you trust your proof system the incomprehensibility is not such a drawback, but anyway. That isn’t what this post is about: I am interested in examining what role finite-state model checking can still play in this new world.
Finite-state model checking until now
We should start by acknowledging that finite-state model checking has been technically obsolete since the mid-1990s, when symbolic model checking roared onto the scene. Last year I attended ETAPS 2025 - a very academic conference - and did not see a single talk on finite-state model checking. Finite-state model checking works by simply exploring every possible system state, using either breadth-first or depth-first search. This has two problems: first the system state space has to be finite (difficult when dealing with monotonic counters!), and second you often see a combinatoric state explosion where slightly increasing the model size (for example, simulating a five-node distributed system instead of a three-node one) causes an intractably large growth in the possible state space. Symbolic model checking instead reasons about the system as a set of logical formulas to satisfy. It can handle very impressive model sizes, far beyond what is possible with finite-state model checking. At ETAPS 2025 I spoke with some industrial model checker users who work in computer processor design, and the idea of using finite-state instead of symbolic model checking was considered laughable.
And yet finite-state model checking is still used! Why? Because it’s understandable. Any software engineer of any education can understand breadth-first search. If your model runs for too long you can estimate its state space and tweak it to reign in the combinatoric explosion while ensuring you still explore interesting states. Finite-state model checkers are so simple that ordinary software engineers can write their own just for fun, and they do. I myself wrote a guide on how to build your own finite-state model checker for TLA⁺. So finite-state model checkers occupy that very sparsely populated space of formal methods that don’t require graduate-level education to use & understand. In contrast, very few people exit undergrad knowing how to write even a basic SAT solver or would consider spending their weekends reading an introductory text on the field like the Handbook of Practical Logic and Automated Reasoning. Symbolic model checkers also infamously exhibit “performance cliffs” where a simple change in your formula turns a sub-second validity check into one that times out. They are, in a word, opaque. This is not to demean their usefulness! There is simply value in using tools that you understand, which may or may not outweigh the value given by the power of incomprehensible tools.
Finite-state model checking going forward
“Understandable validity checking” is a very niche application, and not - I predict - sufficient to maintain the relevance of finite-state model checking itself or tools & languages for which it is the main selling point. Finite-state model checkers do have two other applications I know of: test case generation, and test oracle. Both of these require exiting the nice domain of modeling an abstract system and dealing with the very messy domain of testing whether an actual software artifact - a program! - running on a real computer does what it is supposed to do. It isn’t a great place to end up. Software testing, to the extent it’s invested in it at all, is a back-alley knife fight of competing & overlapping methodologies.
The two test methodologies that finite-state model checking can help with are called model-based testing (MBT) and trace validation. In the former, the model functions as a test-case generator that pushes the system-under-test (SUT) around the state space and checks that it upholds various properties. In the latter, logs & traces are collected from the SUT, perhaps as it is subjected to a chaos testing workload. These logs are then compared with the model to check that the SUT performed a valid system execution. The model is used as a test oracle, distinguishing good behavior from bad.
The problem with these test methodologies is that they are a gigantic pain in the ass to implement. Essentially no systems in existence (excepting FoundationDB and TigerBeetle) were written with a mind to being tested in this way. If you’re dealing with a completely new project then great, incorporate it from the start. But I have absolutely no clue how I would go about integrating MBT into the systems I deal with at work. Trace validation also requires a large investment in execution trace post-processing and faces surprising complexity in the question of when to emit a trace event.
We must control system execution
As a user, I think the only compelling application here is deterministic simulation testing, where the execution of the SUT is fully controlled in a reproducible way. Test case generation & functioning as a test oracle just do not move the needle. So basically, we need to do what Antithesis does. If you’re well-resourced you should just hire them to do it, but I am naturally drawn to think about methods available to your average open source project, with its concordant interest in (plausible) technical sovereignty - so even if Antithesis launches a generous credit program for open source projects, it is worth building the proverbial cobbled-together open source self-hostable alternative. Unfortunately a full end-to-end story for this does not yet exist. It needs the following:
- A method of specifying what actions your system can take in any given state
- A method of specifying what properties your system must uphold (its invariants)
- A method of reliably & reproducibly pushing your system around the state space
- A method of snapshotting & returning the system to a specific state so each test does not need to start from the initial state
- A way of abstracting all of this so you don’t need to modify the SUT
Formal specification languages that use finite-state model checking give us 1 and 2, but 3-5 are the really hard ones that don’t yet exist and - I believe - are required to make 1 and 2 matter at all. There are only two approaches I know of that get us the fifth desired property: deterministic CPU emulation, and a deterministic hypervisor.
I should also expand a bit more on the value of point 4. Brandon Falk puts it best, within the context of fuzzing:
In modern fuzzing, coverage guidance is pretty much mandatory. This means when new code is hit, to save off the input such that it can be built upon. At a very simple level, this means a problem which is 256^4, turns into a 256*4, as all requirements do not need to be satisfied simultaneously, as long as the previous requirements cause new code to get hit they can be built upon.
If you repeatedly have to restart from the initial state then it becomes very unlikely you’ll ever reach interesting states deep in your system, because you’ll spend all your time exploring the same set of states branching off from the origin. Igor Konnov has written a nice post on the difficulty of using random walks to fully explore state spaces that you can read here.
Existing attempts
I’m not aware of any publicly-available deterministic CPU emulators, although I do know Microsoft-internal project tkofuzz forked the Bochs x86 CPU emulator to make it deterministic - so that path is known to be viable! Unfortunately it induces a 100x slowdown compared to native execution. Note also that deterministic CPU emulation seems to be the only possible way to get deterministic simulation testing of true multicore execution, the sort you need when testing lock-free algorithms that make various assumptions about CPU cache coherence behavior. Hypervisor-level solutions like Antithesis serialize all execution onto a single core so cannot test this. Bochs doesn’t properly simulate x86 cache coherence behavior. Writing a deterministic multicore x86 CPU emulator that implements x86-TSO would be an extremely cool project. I don’t think I’m the person to do it, because I can’t even begin to estimate how much effort it would take. Maybe that naivete is a good reason to try! Worst case scenario I become cursed with a lifelong special interest in CPU cache coherence.
For hypervisor-level determinism, there are actually a decent number of projects floating around! All of these require baremetal execution on x86-64 (and rarely also arm64), generally on Linux:
- rr, aka record & replay, a time-travel debugger initially created by Mozilla for work on Firefox. This isn’t exactly what we want, but it’s by far the most mature project out there so it’s worth mentioning. This records the actual memory of a program during execution, so it can later be replayed exactly if a bug was found. You can repeatedly time-travel to different program states as you trace the bug. However, because it isn’t really re-running the program (just a recording of it) you can’t modify execution to explore behavior that branches off from the original execution.
- hermit, a deterministic Linux hypervisor Meta released in 2022 and then stopped actively developing shortly thereafter. I’ve done some light experimenting with the current open source release and it works, sort of? I ran into issues which might have been hermit being incomplete or me just not knowing what I was doing when setting up network calls. PRs are still being merged, anyway.
- deterministic-vmm: a self-described “toy” KVM-based virtual machine monitor written as a personal project by Josh Snyder as described in this blog post.
- Bedrock, another one-person project written by Niklas Gögge (assisted by LLMs) as described in this nicely detailed blog post.
- dhyve, a project based on FreeBSD’s bhyve for a change (similar to Antithesis, actually!) which is the bachelor’s term project of Peter Graugaard and Nicholas Kristiansen at the Technical University of Denmark.
Those are all the projects I know of. Interesting that the last three were all released within the past few months! Deterministic execution must be in the 2026 zeitgeist. I’ve not yet evaluated any of them, but inspiring to see individuals or pairs of people taking a crack at this problem.
Conclusion
That was my attempt at product-level thinking for lightweight formal methods like TLA⁺, Quint, and any other homebrewed finite-state model checking systems. It was also an attempt to put into writing my ruminations on what I should spend the next part of my career working on. My prediction is we are leaving the cozy 80/20 world where these tools were a relatively easy choice. The future looks like a split between formal proofs and a fleshed-out story for deterministic simulation testing to ensure conformance between spec and code without huge integration effort. Ultimately more is now being asked of lightweight formal methods. Of course, for those for whom just thinking about your system design clearly is important, these tools will always retain their value. I saw a nice talk on this theme from Marianne Bellotti at Software Should Work conference last month!