Building Confidence in Systems Written with AI

In a conversation with someone at a private equity firm, we got onto the subject of how AI would change work. His view was that work would become harder for the humans still doing it. As AI takes on the easy stuff, more of our time will be spent on the problems that require difficult decisions and a deeper understanding of what we are trying to achieve.

I agree with him. There is freedom in no longer spending our days writing CRUD applications and boilerplate code. But that leaves us with more of the work that I find both interesting and demanding: thinking through designs, understanding how a system actually behaves, and deciding whether that behavior matches what we need. An afternoon spent working through failure semantics can be harder than an afternoon spent implementing another API endpoint.

We’ve been using TLA+ to model our Rust services since late 2025. This year, that work has grown into a broader effort to build evidence that our systems behave as intended: implementation proofs, deterministic simulation, fuzzing, and continuous performance testing. Each helps answer a different question about the software we are building.

Together, they have also given us better tasks to set our agents than simply asking whether the code looks correct.

The Systems We Are Building

We build services that help AI agents find and use information across large organizations, subject to the organization’s access rules. We call this an executable context layer: agents can discover the information they need and work with it through existing services, APIs, and database connections.

Much of the underlying engineering will look familiar to anyone who has built trading infrastructure. State machines, ordered operations, replay, and sequencer-like capabilities remain useful ways to manage complexity. I carried those approaches over from my previous work because they make the behavior of a system easier to reason about when something fails.

Our ontology server shows what this looks like in practice. It scales horizontally using a single writer and multiple readers, with object-store-based leader election. It supports strong reads as well as reads with bounded staleness, typically in the region of one second behind the leader.

Each of those choices introduces obligations. A process that has lost leadership must not continue committing writes. A replacement writer must recover the correct state. A reader must have enough information to provide the consistency it promises. If a reader cannot establish that it is within its staleness bound, continuing to return data as though the bound still holds would violate the contract.

Rust removes a substantial class of memory-safety and data-race problems from this work when we stay within safe Rust and sound library abstractions. Coming from Java, that is a meaningful improvement. But a memory-safe program can still acknowledge a write too early, lose track of a reservation, deadlock, or serve a read from a process that is no longer entitled to answer it.

Those are the problems our verification and testing work needs to address.

Start with the Protocol

TLA+ is a good fit for reasoning about the system before getting lost in the implementation. We can describe the state of the participants, the operations that change that state, and the properties that should hold as those operations interleave.

Consider a writer that pauses long enough for another process to take over. The original writer then resumes. From its local perspective, it may still believe it is the leader. What prevents that stale belief from becoming an accepted write? Our April design put enforcement at publication: a fresh leadership check, a conditional compare-and-swap on the object-store manifest, and term-scoped data keys that prevent an old writer from overwriting a newer term’s objects.

Answering it forced us to describe the authority to write, where that authority is checked, and what the object store actually guarantees. The atomic conditional update in the model must correspond to an operation the object store actually supports. Assuming that a paused process conveniently stops acting would remove exactly the failure we need to investigate.

The same approach applies to replication and reads. We need to distinguish a record being received from it being durable, and being durable from being applied to a reader’s state. Collapsing those steps into a single transition can make a model pleasantly small while hiding the behavior that matters.

We also need to separate safety from progress. Preventing two writers from committing conflicting histories is a safety property. Eventually making progress after a failure is a different obligation, dependent on assumptions about scheduling, communication, and recovery. A system that never accepts another write can preserve safety while being of little use to its customers.

Model checking explores the configured state space for violations of these properties.

A Model Can Know Too Much

A model can also make decisions with information no participant has. An early revision of our ontology server’s leadership model had a global clock, and some of the conditions for acquiring, renewing, and publishing depended on that clock. A running process does not have that view of the world. It has its own clock and the leadership state it has managed to observe.

In April, we revised the model to base those decisions on node-local time and observed lease state, with explicit clock-skew assumptions. Lease expiry was calculated from the acquiring or renewing node’s clock. The model’s global time still described the environment, but it could no longer quietly make decisions on a process’s behalf.

This is an easy mistake to make when modeling. We know the whole system, so we write a rule using information that no individual participant actually possesses. The resulting model can be reassuring for the wrong reason. Having to ask what a node can know at each step exposed assumptions we needed to resolve before implementing the design in Rust.

The Gap Between the Model and the Code

The most persistent difficulty is connecting a correct protocol model to the Rust that implements it.

In a model, an operation may be one state transition. In the service, it may involve several function calls, an allocation, a lock, an asynchronous write, and a task that can be cancelled while awaiting completion. Each intermediate state creates another opportunity to break an assumption made at the protocol level.

A write-ahead log illustrates the problem. The protocol needs a clear account of which writes survive a failure and which writes may be acknowledged. The implementation must make that account true through its append, persistence, recovery, and error-handling paths. A model that treats durable append as an indivisible operation leaves those details to us.

We have not fully solved this gap. Our current approach is to overlap verification at several levels:

Verus allows us to express specifications and proofs alongside supported Rust code. Aeneas, using the representation extracted by Charon, provides another route: translating supported Rust into a form we can reason about in a proof assistant such as Lean.

For smaller pieces, Kani lets us check critical accounting and cancellation-related state transitions. We isolate the bookkeeping and check the relationship between resources reserved, consumed, and released. One of our first experiments showed why that was worth doing.

The One Extra Byte

Kani found a bug in the spool quota accounting on its first run. This was a small calculation: remove a session’s previous reservation from the total, add its replacement, and reject the request if the result exceeds the quota.

The code used saturating arithmetic:

let released = ledger.total.saturating_sub(old);
let new_total = released.saturating_add(bytes);
if new_total > self.quota_bytes {
    // Reject the reservation.
}

There was even a reassuring comment describing the saturating subtraction as “defense-in-depth.” The addition used the same idiom. No wraparound, no arithmetic panic, and an explicit quota check at the end. It is the sort of code that is easy to read past.

But saturation loses information. If the sum exceeds u64::MAX, it is capped at u64::MAX. If the quota is also u64::MAX, the comparison says that the new total fits. We accept the reservation and record an incorrect total.

The failure reduces to four inputs:

total = u64::MAX
old   = 0
bytes = 1
quota = u64::MAX

We are already at the limit, ask for one more byte, and get permission. The quota could reach that value because its conversion from megabytes also used saturation: quota_mb.saturating_mul(1024 * 1024). The same apparently cautious choice appeared on both sides of the comparison.

The harness compared the production calculation against a wider, u128 calculation. With actual holding the helper’s optional accepted total, the core checks were:

kani::assume(old <= total);
let exact = u128::from(total) - u128::from(old) + u128::from(bytes);
assert_eq!(actual.is_some(), exact <= u128::from(quota));
if let Some(accepted) = actual {
    assert_eq!(u128::from(accepted), exact);
}

The first assertion checks the admission decision; the second checks that an accepted total is exact. The assumption states that the old reservation was already included in the total. That was enough to expose the defect without constructing a running service or filling a disk.

This was an extreme arithmetic boundary, not an observed production outage. Once the counterexample is in front of you, the bug is straightforward. Finding that combination in an ordinary review or workload test is the harder part. Kani did not need to judge whether the input looked realistic; it checked whether the property we had stated was true.

A Better Task for an Agent

“Review this code for correctness” is a broad request with a surprisingly low bar for completion. An agent can produce a coherent description of the intended behavior without ever establishing whether the implementation has that behavior under failure.

Asking it to write a specification and a proof or model-checking harness requires more concrete decisions. What is allowed at entry? What must hold at exit? Which intermediate states are valid? Can an operation fail after changing state but before reporting success?

In the quota example, the contract required accepted accounting to match the mathematical total. Kani disproved that property, giving the agent a counterexample to work from.

Our review effort moves toward the specification: does the postcondition express the requirement, and do the assumptions admit the failures we care about? The agent’s job is to satisfy that contract; ours is to make sure it is the right one. In the Kani spike, we also restored the original saturating-addition defect in a temporary copy and confirmed that the proof failed an assertion, so we knew the harness could catch the bug it was written to prevent.

These bugs can often be captured in regression tests once we understand them. The difficulty is discovering the particular combination of state, failure, and timing that needs to be tested. Formal methods give us another way to reach those cases.

Running the Service Under Controlled Failure

The next question is how the components behave together, with asynchronous tasks running and failures occurring between operations. Deterministic simulation lets us investigate those executions and replay them when something goes wrong.

Our ontology server uses Tokio extensively. Taking inspiration from FoundationDB’s simulation approach, we made the service controllable in deterministic tests. We can manipulate time and introduce network and disk pauses, dropped communication, partitions, and corruption through the test environment.

This takes work in the service itself. If a component bypasses the controllable clock or performs I/O outside the test abstraction, the harness loses control of that part of the execution. Determinism has to be supported by the architecture.

We use Torment to help manipulate execution in Tokio and Hegel for property-based testing. Alongside this, concurrent fuzzing and Jepsen testing exercise other aspects of the system’s behavior. Each approach gives us a different view of failures: an invalid state transition, a problematic schedule, or an externally observed history that violates the expected consistency model.

We saw the value of connecting these layers early in the ontology server’s development. Our first TLA+ model described entity lifecycles, validity windows, and semantic relationships. We translated its invariants into Rust guards and a separate reference model for simulation. A live relationship needed live endpoints; their validity windows had to cover the relationship’s window; certain contradictory relationships could not overlap.

Simulation then found a bug in the mock store used by the harness. At that point, the production graph-store adapter did not run this validation path; this was a defect in the test implementation, not an observed production rejection. When replacing an existing relationship, the guard checked the proposed replacement against a collection that still included the old version of that same relationship.

A BROADER_THAN relationship says that one concept is more general than another. Reversing one could therefore look like a two-node cycle: the old and new directions appeared to coexist, even though one was replacing the other. The check rejected a valid transition. Excluding the relationship being replaced corrected the comparison.

That was a simulation finding, with the TLA+ work supplying the rules and reference behavior. It also reminded us that correctness includes allowing valid operations. A guard that rejects too much can preserve an invariant while implementing the wrong service.

Once a failing execution can be reproduced, an agent can investigate a specific sequence of events, make a change, and rerun it. Without that, we risk spending the investigation trying to recreate the symptom. We are still extending the harness to cover more CPU stalls and operating-system-level freezes.

Correctness and Performance Over Time

The evidence also needs to stay relevant as the code changes. A service can return the right answers and still become unusable under its expected workload. Shared scheduling, allocation, locking, and background work mean that improving one capability can slow another without touching its immediate implementation.

For the ontology server, pull-request checks include intensive deadlock checks, property-based tests, multi-node replication tests, and latency tests. A result beyond the configured threshold fails the PR and starts an agent investigation. The agent reruns measurements and examines the changes to distinguish a software regression from a slow CI machine, giving us evidence we can act on while the change is still in review.

A sequence of individually acceptable regressions can also add up to a substantial deterioration. Nightly stress and performance tests track latency, memory consumption, concurrency, and CPU time across a longer window. When a metric crosses a statistical threshold, an agent can provision a CI runner, repeat tests, and make small experimental changes to test an explanation. It opens a ticket with the reproduction and supporting evidence.

That division gives us feedback fast enough to use during a PR, with more expensive investigations running overnight. The harnesses are part of how we maintain the service’s guarantees as agents continue changing its implementation.

What the Fuzzer Didn’t Find

Other components need a different balance. For our in-house sandbox, we run nightly fuzzing soaks lasting eight hours. During the first few runs, finding a crash report in the morning was not unusual.

In one session, an agent hit a failure with an entirely ordinary command:

date +%s%3N

It wanted a timestamp with millisecond precision. Our date builtin passed a format through to Chrono that our translation did not support correctly. Formatting returned an error, and converting that formatted value to a string turned the error into a panic.

That would have been bad enough on its own. The panic also poisoned the mutex used to serialize Bash invocations. Subsequent commands tried to acquire that lock and panicked too. Even echo hello failed. The agent kept retrying; every attempt hit the same poisoned lock.

We fixed the format handling and the recovery of that serialization lock. But the broader question was how many other apparently harmless inputs could panic inside our builtins. The follow-up fuzzing and hardening work exposed related formatting failures, including excessive precision in printf’s %g conversion and awk’s OFMT setting. Fixing the date reproducer had not established that formatting was safe elsewhere.

One ten-minute campaign reported no crashes even though, for part of the run, the awk precision bug was still present. Random byte mutation had not reached the combination of directive and value that triggered it. We added format directives and boundary values to dictionaries and retained the failures as regression seeds. For arithmetic, we also added a target that builds expressions from structured pieces so the fuzzer can reach meaningful evaluator behavior more reliably.

The captured inputs become permanent regression cases and give an agent a concrete starting point for checking a repair. A green fuzzing run means much more when we understand what inputs it can actually reach.

Where the Effort Pays Off

The strongest return so far has come from choosing specific guarantees and following them through the system. Leadership must confer the right to commit. Acknowledgement must mean something precise about recovery. A cancellation must leave accounting consistent. A performance improvement must survive contact with the rest of the workload.

We treat every result as evidence with a stated scope. A proof establishes a property under its assumptions; a model checker explores its configured domain; a test records what happened in the executions it exercised. Passing results do not automatically compose into a proof of the deployed service, and replaying a fixed crash does not establish that its whole bug class is gone. Our responsibility is to keep those scopes explicit and examine the gaps between them.

I keep coming back to that conversation with the private equity firm. Having agents take on more of the implementation gives us the freedom to spend longer on these questions. It also asks more of us. We have to understand the behavior we want well enough to describe it precisely, and the behavior we have well enough to recognize where the two differ. The agent can help with that reasoning, but we still own the decisions about what the system promises and what evidence is sufficient to trust it.

I am happy to spend less time writing boilerplate. I also find that the work filling that time demands more concentration and more willingness to question my own understanding. The models and harnesses give us practical ways to do that questioning and evidence we can return to as the code changes.

After a year of doing more of this, I find the question I keep giving agents is also one I keep asking myself: what, exactly, must remain true if this operation stops halfway through?