In past work we explored early attempts to model and verify transactional programs, building compositional TLA+ specifications of MongoDB’s distributed transaction protocol. With the rapid advances in LLM capabilities over the past 6-9 months, though, we have seen entirely new formal specification and verification abilities emerge in frontier models. In particular, the ability to not only write well-formed TLA+ specifications but also promising results on writing complete, machine-checked correctness proofs for those specifications in the TLA+ proof system (TLAPS). As a grounding historical data point, the original transactions modeling work was done over a year ago (~ February 2025), at which point the latest frontier models we had access to were Claude 3.7 Sonnet and GPT-4.5, and Claude Code was still in its relative infancy.

These new LLM capabilities have opened up a lot of new opportunities for how to potentially apply formal methods in the design and verification of our systems. If we can truly generate proofs “on demand” this lets us consider a variety of new use cases that were previously infeasible. One interesting use case is for workload-specific transaction analyses. Specifically, the problem of checking the robustness of a given transactional workload. That is, given a specific transactional application, if we run it under an isolation level weaker than serializable, will it still provide serializable guarantees? There is some great past work on how to formalize and check this problem in certain cases, but for arbitrary workloads this might be very challenging to prove. With the advent of proof-capable frontier LLMs, though, we can try to do this automatically.

Modeling Workloads and Robustness

In Checking Robustness Against Snapshot Isolation, from 2019, they looked at a small set of transactional workloads that they established robustness properties for under snapshot isolation. We can use these as a starting test bench to see if we can automatically re-establish robustness for some of these workloads using TLA+ and the TLA+ proof system.

They originally look at several workloads, but we can start with two basic ones, TPC-C and Auction, which they claim to be robust under SI. We will see if it is possible to automatically establish robustness of these applications under snapshot isolation without doing tedious manual analysis and proof effort. Note that, for TPC-C, the robustness question under SI was also previously established formally in the affirmative by Fekete et al. in 2005. For most of these prior techniques, though, the proofs often require heavyweight and detailed technical machinery, something that would be out of reach for a new, arbitrary workload given to us on the fly e.g. or for a workload that was tweaked or modified by an end user. We want to explore if we can effectively generate these proofs “on demand”.

To start, we need the ability to formally reason about both (1) a given transactional workload and (2) an underlying database/KV-store providing a given isolation level. We first start with an abstract formal model of a snapshot isolated key-value store itself, which we luckily have versions of lying around in TLA+. On top of this, we can then build an abstract formal spec of the TPC-C workload itself. Thankfully, it’s also easy to get LLMs to build most of the skeleton for this as well. Note that, under snapshot isolation, we can think about transactions as each getting their own private copy of the database when they start, and execute locally against this private workspace of data before trying to commit. So, from the perspective of other transactions, the specific order and timing of operations within a transaction are mostly irrelevant. Therefore, our specification works within a model where transactions and their read sets and write sets are chosen and written in one atomic step before commit.

Our workload specification, TPCC.tla, instantiates an instance of the underlying SnapshotIsolation module, which it uses as its backing KV store. Within that module, we also define the correctness property we are concerned with, which is serializability. In this context, this is defined as conflict-serializability i.e. are there any cycles in the multi-version serialization graph. Once these specifications are written, this allows us to express our robustness property formally as a simple invariant i.e. does our TPCC.tla spec satisfy the Serializable invariant.

\[TPCC!Spec \Rightarrow \square Serializable\]

We could try to model check this property for small parameters using TLC, to find counterexamples if TPC-C was not robust under SI. Since we expect the workload to be robust under SI, though, we can try to generate a TLAPS proof of this fact. We can give this a go with a simple prompt to Claude Code, with the assumption we have the appropriate TLAPS toolchain installed locally, along with some TLAPS-specific toolchain guidance in our agents file:

Go ahead and try to write a complete TLAPS proof for the `SerializableViaPath` 
invariant in @TPCC.tla. Don't look at past proofs or other proof files or commit history.

Using Opus 5.5 in Claude Code, we were able to generate a complete TLAPS proof of the serializability invariant for the TPC-C workload spec in around 1 hour. The proof is approximately 2000 lines of TLA+, and can be re-checked from scratch using TLAPS in a few minutes. We created a spec for the Auction workload as well and ran this same proof experiment. It similarly took about an hour to generate a complete TLAPS proof of Auction serializability under SI, in around 1000 lines of TLA+. The proof can also be re-checked from scratch in a few minutes.

There are some caveats to consider here, including the fact that, in general, there are some “known” proof techniques for some of these workloads out there in the pre-existing literature, which may be leaked into the LLM’s training data. Regardless, though, it seems a strong data point on the capability strength of the LLMs. Furthermore, we expect it may be possible that proofs for a class of properties like these robustness questions may generally follow a similar shape, and so LLMs carrying out many of these proofs may derive helpful structural and strategic hints from past attempts. It is also worth noting that these TLAPS proofs are dense technical artifacts, so it is important to check that there is no “cheating” going on with the LLMs writing these proofs. In particular, addition of unrealistic or overly strong assumptions that are being relied on for the proof to go through. It is still important to understand as a human exactly what is being proven, even if you may not understand all the details of how the proof is exactly constructed.

Reflections and Future Directions

This experiment is a relatively minimal proof of concept, but there are a broad class of extensions we could imagine exploring, backed by automated proof generation. For example, checking whether standard program transformations like SELECT FOR UPDATE achieve appropriate serializability guarantees for a non-robust workload. There has also been exploration into how to safely promote certain operations within a workload to ensure it executes serializably. Other work has also looked at a generalization of the above problem, referred to as allocation, potentially also assigning different isolation levels to different transaction types. This effectively tries to determine the weakest possible isolation level against which a given workload is robust, letting a database enforce the weakest necessary guarantees for correctness of a given workload.

This overall approach takes some of the other ideas from tools appearing across the space. Namely that of abstracting given code/systems into an abstract “simulation” substrate over which to reason about. In our case, we are using TLA+ as this abstract modeling substrate, which gives us a mechanism to both potentially look for bugs (via model checking) and also write proofs about correctness. The fluidity with which we can now move between programming language representations is opening up many new possibilities, and significantly expands the capabilities of on-demand program analysis and verification tasks. Translating a system or code into a suitable format for analysis is approximately free in many cases, and so we can start to think about any one representation as just one view on an underlying source of truth. Evals like TLAPS bench are also starting to explore the boundary of how well LLMs can complete machine checked proofs for a variety of practical system specifications.

As with many LLM capabilities today, this also serves as a concrete upper bound on the speed and cost of this task going forward. That is, we can only expect intelligence and its cost to continue dropping by orders of magnitude over time, and so what might be a multi-hour long agent session today costing tens or hundreds of dollars, may eventually be something that can be done extremely cheaply in a few seconds.