'Trust but verify'; or, 'the correctness ratchet'

The name of the game in agentic development is figuring out how to clearly tell agents what you want– and then how to be sure they follow through. Lately I’ve been tinkering with an interesting technique around this that I’d like to share.1 I call it “trust but verify”2.

The basic idea is that sometimes you have things you want to “verify” but they can’t really be mechanistically checked. In that case, you let your agent do its best. But you also have it create an evidence file that contains the inputs it drew on to make that decision along with its rationale. Then you gate your CI on checking that these evidence files exist and that the inputs are accurate. Those checks are deterministic and cheap. The rationale itself is natural language and can’t be checked.

Doing this “trust but verify” technique on its own is helpful. It creates a kind of hill-climbing towards correctness that is stronger than (e.g.) tests alone. It helps to check meta-reasoning like “is the set of tests sufficient to show this requirement is true”. Documenting the input also means that if any input should change, the CI check will start to fail, and the agent will be forced to revalidate its reasoning.

What I find most interesting though is that “trust but verify” can be used to create a kind of correctness ratchet over time. The idea is that, now that the inputs + rationale are documented, you can have other agents come back and double-check that reasoning, even when the inputs have not otherwise changed. As agents naturally improve, or just due to the randomness inherent in how agents work, they will naturally find things the original rationale overlooked, and you’ll be able to address them.

Agents are none too smart, but they can be awfully dogged and persistent. If you ask them to climb a hill, they are going to find a way to do it. The tricky bit of course is that they don’t always climb that hill in the way you intended. Also, they may not exactly climb it so much as find a route to the top: they may be persistent, but they are also lazy f!@#kers4, and they love to take shortcuts.

The fact that agents are good at climbing hills has got a lot of people in the automated reasoning community5 very excited. After all, what better way could there be to make sure your program does what you expect than to formally prove that it is true? And we’ve seen that when you set a model loose with a Lean theorem, it can be quite adept at proving things6.

Myself, I’m quite excited about tools like Lean but also Verus, Aeneas, and Creusot. I think we’re going to be using them a lot more. And yet, I also think that proving propositions is not the end of the story.

Let’s start with the obvious problem. An agent may be good at proving a proposition, but who is actually writing it? Even when something can be formalized, doing that formalization is a fair bit of work. Consider this random example of a requirement from a project I am working on7:

A Fleet using Functionality A must be attributed to every Functionality reachable through any number of recorded deprecation steps, while being counted only once when routes converge.

This is part of a project that is analyzing fleets across Amazon and looking at how much DRAM they consume. Our goal is to make sure that every large fleet at Amazon has Rust versions of every library it would need to be rewritten into Rust. We want to be able to go to the maintainers of those libraries and say, “there are fleets accounting for X% of Amazon’s total DRAM consumption that use your library; you should make a Rust version”.

The point is, while the concept of this DRAM accounting is not complex, formulating it in a precise, mathematical way is not at all trivial. You have to have some notion of transitive closure, talk about the graph of dependencies, etc. There is no way that the lazy, spoiled programmers of the future are going to write a formula like that by hand.

Much more likely is that they are going to give high-level direction to the agent and ask it to connect the dots. After all, this is what agents are good for! And in this case, I would trust an agent to get it right. As I said, it’s not really complex, just… tedious.

And of course this leaves aside that there are many things that are just plain hard to formalize. Consider a requirement like, “a warning must be displayed on every relevant form in a prominent fashion”. Checking this requirement requires a notion of what is “prominent”, which is unlikely to be a mathematical property one can write down. And while I would not trust an agent’s judgment over an actual graphic designer, it is also the kind of thing where the agent can likely do a “good enough” job to catch many failures.

The other point is that while agents are good at authoring proofs, it still takes them tokens – and more importantly, time – to do it. And sometimes quite a bit. If developers have to wait a while for the agent to find a proof to a complex property, that better be worth it. If the property you are proving is key to your system, it probably is. But if the cost of a mistake is less than the cost of a proof, people won’t bother, so it’s worth thinking about leaner, easier ways to gain confidence.

One final point is that applying too much rigor too early in the process can be a real problem. This one is tricky because rigor can surface problems earlier, too. But it’s often helpful to start by defining your requirements and things at a higher level and gradually get more precise as you go, tolerating a bit of “looseness” early on when you know there are details you have to nail down, but it’s not important to do so yet.8

A key point for me is that just because you haven’t formalized your requirement all the way to a mathematical proposition doesn’t mean that you’ve got nothing at all. You can often phrase a high-level version of what you want, perhaps one that is overly simplified. In fact, it’s pretty useful to do so, because when you find that your rule doesn’t quite work, that helps you figure out how to refine it into the more precise rule you actually want.

The key idea of the “trust but verify” technique is that leaning on agentic reasoning is good, fine actually. But when you do so, you should have the agent explain itself and also have it lay out what inputs and evidence it used to reach that conclusion. Basically, leave yourself a trail so that you (or another agent…) can come back and audit what decisions were reached and on what basis.

Following this approach helps in two ways:

Probably the simplest example of this “trust but verify” technique is Habeas Codicem. This is a small project I made in part as an experiment. The idea is that you write requirements into your docs and then Habeas Codicem adds a test into your system that can only be passed if an agent has written an explanation of why each of those requirements is satisfied. Those explanations are recorded as evidence files that are committed into your repository along with the code.

The interesting bit about Habeas Codicem is that the evidence files contain not only the agent’s rationale and judgement, but also a list of the inputs it used to reach that conclusion. And these inputs have to have certain contents. For example, if you have a function that is labeled as part of the requirement’s implementation, or a test that is tied to a requirement, then the agent must include that function or that test in its evidence.

The final part of Habeas is some skills that instruct the agent to always check with you, the human, before editing requirements, and to confirm agreement on requirements before implementing.

Early in the post I mentioned an internal project I am working on at Amazon to analyze which missing dependencies might block fleets from migrating to Rust. This system involves a lot of agent-driven investigation. For example, perhaps there is a Rust version of a Java library, but it only handles some of the features (this is pretty common). Then we need to know whether the fleet’s code cares about those features that aren’t included.

My early attempts at gathering this data were pretty crude. I basically just sat there telling Amazon Quick “try harder, make no mistakes”. Not great. I didn’t really trust the result.

My newer attempts are much more thorough. I ask the agents to produce an evidence record of what data points they looked at and to include a written rationale for how those data points connect. I then test that the data points hold. For example, to determine if the method convertData in some library is called, the agent might register specific lines from .java files showing a call like value.convertData(). Or it might show the results from a grep that show no matches for convertData.

The interesting bit is that while the rationale from the agent can’t really be evaluated in an automated fashion, the evidence can be. So before we accept any agent-created conclusion, we run a deterministic checker that ensures the evidence is valid (those lines really do appear where the agent said they would) and then records a receipt that the check was done. So the agent cannot just hallucinate evidence.

Habeas Codicem does not prove your code obeys its requirements; nor does my inventory system prove that a given Java feature is used. But it does prove that the agent actually considered the question enough to write out some evidence + a justification. And assuming your agent is not actively malicious, that’s actually quite a bit.

One thing that we’ve seen is that agents often “lie” about what work they did. They’ll claim to have carefully read through a document when an examination of their tool invocations shows that they’ve just looked at a few random bytes.

One of the ideas I find most interesting in this space is the idea of revalidating rationale. Now that we have evidence files committed to git, we can absolutely have another adversarial agent that periodically pulls up those files and gives them another look. That agent can go looking for holes in the original logic and produce modified and improved proofs or counterexamples. I find this particularly compelling when you think about new and better models that might be more adept at finding holes.

I think this technique suggests how we can begin to tackle the problem of converting “high-level requirements” into formal theorems. Instead of expecting humans to write and review logical formulae, we can ask an agent to do the conversion – and to record its thinking process (with verifiable evidence). Then we keep that evidence around and we periodically revisit it, looking for potential edge cases. We wind up with a kind of ‘confidence score’ – the more reviews that have approved a given “requirement->formula” translation, the more likely it is to be accurate.

That said, I’ve not really put this into practice yet, and I anticipate it may be tricky to get it working right. People have told me to expect that agents may ping-pong a bit: for example, maybe one of them translates your plain English into logic, and then another says “that translation doesn’t look right” and takes a new approach. But then yet another agent reverts that and goes back to the original. This seems very plausible– I suspect it can be resolved by adding enough history to recognize that it actually reflects ambiguity in your original statement, and to surface the problem up to you.

I do not claim this technique is novel. I am quite sure people have been doing variants of