Formal Verification for Java: Acceptance Rules for AI Code

Formal Verification for Java: Acceptance Rules for AI Code

Explore a small step toward a software factory, with repeatable checks and clear limits on what has been proved.

Markus Eisele

Nov 3

Formal verification lets us check a precise claim using mathematics. In an inventory system, that claim might be that stock never becomes negative. First, though, we have to define what is being checked. We can describe a model and explore the states it can reach. Or we can prove that an operation keeps a rule true for every allowed input. In both cases, we need to say exactly where that rule applies.

I’m interested in learning this because I want coding agents to do more of the implementation. I also need a clear way to decide whether their changes can be accepted. An agent can write the code, tests, and explanation in one conversation. I still have the burden or pleasure to decide whether those tests ask the right questions. Some of that decision needs to be turned into checks we can run again, after the conversation is gone.

The amount of code being generated adds another problem. An agent can produce a large change while we’re still reviewing the previous one. And the blast radius can reach beyond the files that were changed. An edit to a shared class may affect callers across the application. Loose guardrails and Markdown instructions tell an agent what to aim for. On their own, they don’t tell us whether the code follows those rules. We need checks that can reject a change when a rule is broken.

This gets us closer to the idea of an agentic software factory. And by that, I mean a repeatable process for taking a request through implementation and checks. An agent is given a request with a clear scope. It proposes code and runs the agreed checks. If a check fails, that result can be used to prepare another attempt. People still decide the requirements and review changes that need judgment. Before more responsibility is handed to the process, we need to understand what its checks actually tell us.

Why not just use TDD?

But we can already build that loop with test-driven development, right? Write a failing test, implement the behavior, and refactor while the tests stay green. Yes, and those tests should stay. Writing them first doesn’t make them complete, though. A passing suite tells us about the cases and execution paths it actually exercised. A different order of concurrent operations may still break the rule.

Formal verification lets us check a chosen rule beyond those test runs. A model checker such as TLC can explore every reachable state of a small, configured model. That includes orders of operations we may not have thought to test. A proof in Lean can establish a rule for every input allowed by its assumptions. Those assumptions and the rule have to be stated precisely, of course. Requirements we leave out are still left out.

My goal is to give a few important rules stronger checks that can be run after every change. The tests exercise the Java code. The model and proof check the formal definitions. We still have to review whether those definitions match the code and what the application is supposed to do. For a software factory, that gives the next agent more precise conditions for accepting a change. It doesn’t give us a proof of the whole application.

So I sketched a small Java experiment and asked the coding agent to build it. We have one item in stock and two callers trying to reserve it. The rule is short: inventory must never become negative.

I also asked the agent to prepare the formal models and proof. That let me try these tools alongside Java code I already understand. Definitions were written in each language, and the tools could check them. Those definitions still need to be read, of course. The same misunderstanding can appear in the code, the model, and the theorem. Having the agent write all three doesn’t remove that possibility.

Giving the specification somewhere to go

In Why AI Makes Software Engineering Harder, Not Easier, I wrote about turning what people want into code that does it. That is still difficult when the code is generated quickly. Somebody has to decide what it is allowed to do.

I came back to this in Spec-Driven Development Needs an Exit Strategy. A change brief can guide the implementation and then be allowed to expire. The rules that remain need a home in something the team keeps checking. A schema, a test, or a policy can provide that home.

The inventory example lets me try this with one rule. A planning document can explain why we need concurrent reservations. Once the code exists, the rule about stock still needs to survive the next change. I want the next agent working on this class to find that rule through the build. It might never read the conversation that produced the class, after all.

Formal methods give us another place to keep some of these rules. We do have to look closely at what is being asked, though. “Stock never becomes negative” would also be satisfied by a reservation method that always returns false. We need a little more than that. Available stock must be reservable. A successful reservation must use one item. And two callers must not both get the last one.

So, one safety property was chosen for this example. The Java tests cover the other things we expect. A proof can show that this one rule holds. It still leaves other behavior open, though.

One item is enough to get this wrong

The project I use for the example uses plain Java 21. There is one production class, Inventory, and stock is stored in an AtomicInteger. A negative starting value is rejected. The reserve() method returns whether a reservation succeeded. The first and simple implementation looks like this:

if (available.get() <= 0) {
    return false;
}

available.decrementAndGet();
return true;

You can probably recognize every operation here. Stock is checked, and the decrement is atomic. With one caller, the last item can be reserved and stock reaches zero. So far, this gives us the result we expect. With two callers, the operations can happen in this order:

Stock starts at 1.
Caller A reads 1 and passes the check.
Caller B reads 1 and passes the check.
Caller A decrements stock to 0.
Caller B decrements stock to -1.

Each operation on the AtomicInteger is atomic. The check and the decrement are still separate, though. Caller B was allowed to continue when stock was 1. By the time it decrements stock, the value is already 0.

I wanted this failure to happen every time the test runs. So the broken implementation, which lives only in the tests, has a hook after the check. A CountDownLatch holds both callers there until both have passed it. Then the callers are released and both decrement stock. The test checks that the final value is -1. It passes when the bug has been demonstrated. We can run that same sequence again. There is no need to run the race a thousand times and hope for the right timing. I asked for a specific failing sequence, and the test forces it.

The arithmetic can be right while the protocol is wrong

The local rule is quite small. If stock is positive, return one less. Otherwise, leave it as it is:

static int nextAvailable(int current) {
    return current > 0 ? current - 1 : current;
}

I used Americium to generate a thousand stock values between zero and ten thousand. The Java method is called with each value. The property test checks that stock stays at or above zero and never increases. The exact result is checked too. Positive stock must go down by one, and zero must stay zero. Ordinary JUnit tests also cover zero, one, and the largest Java integer.

That gives us checks against the Java method with generated inputs. I also wanted a proof of the rule itself. Lean is a programming language and theorem prover. We can write a definition and a proof about it, and Lean checks the proof. Here is the definition and proof from the project:

import Lean.Elab.Tactic.Omega

def reserve (available : Int) : Int :=
  if available > 0 then available - 1 else available

theorem reserve_preserves_nonnegative
    (available : Int) (h : 0 <= available) :
    0 <= reserve available := by
  unfold reserve
  split
  · omega
  · omega

The theorem says that available can be any integer at least zero. If we pass it to reserve, the result will also be at least zero. The definition is opened, and the proof is split into the two branches of the if. Lean’s omega tactic handles the integer arithmetic in each branch. The proof it produces is then checked by Lean’s kernel. The proof validation documentation explains that process.

So the theorem covers every non-negative integer in the Lean definition. Americium checks a selection of inputs against the actual Java method. There is a difference in the number types. Lean’s Int has no fixed size limit. Java’s int is limited to 32 bits. This operation cannot overflow, though, because one is subtracted only when the value is positive.

The broken concurrent code can still oversell. Lean’s reserve receives one value. That value is checked, and the result is calculated from the same value. The broken Java code reads shared stock and checks what it read. Later, it decrements the shared stock. Another caller may have changed it by then. This is why I wanted both a theorem and a concurrency example. The arithmetic can be proved correct. We still have to check how the operations are put together when callers run at the same time.

Letting the model explore the order of operations

TLA+ is a specification language. We use it to describe states and the actions that move between them. The TLC model checker then explores the model we configured. Here, the model contains a stock value and a program counter for each worker. The counter tells us where the worker is. It can be checking stock, waiting to decrement it, or finished.

In the broken model, the check and decrement are separate actions. After a successful check, the worker moves to decrement. Stock hasn’t changed yet. The decrement action then subtracts one and marks the worker as done. Well, that leaves room for the same failure we saw in Java. Both workers can finish checking before either decrements. TLC can explore that sequence.

The rule is written as an invariant. That means it must hold in every state the model can reach:

NoOversell == stock >= 0

TLC finds two successful checks followed by two decrements. Stock ends at -1, just as it did in the Java test. The sequence was forced in JUnit. For TLC, I described the allowed actions and asked the checker to explore the model. It found the failing sequence from those actions.

In the corrected model, the reservation is handled by one action:

Reserve(w) ==
    /\ pc[w] = "reserve"
    /\ stock' = IF stock > 0 THEN stock - 1 ELSE stock
    /\ pc' = [pc EXCEPT ![w] = "done"]

The prime in stock' means the value in the next state. Stock is checked and its next value is chosen in the same action. A worker can no longer wait between those two steps with permission to decrement later. TLC checks the states reachable with two workers and one item. No negative stock value is found in this corrected model.

The Java code uses compare-and-set, or CAS. The update succeeds only if the value read earlier is still there:

public boolean reserve() {
    while (true) {
        int current = available.get();
        if (current <= 0) {
            return false;
        }
        int next = nextAvailable(current);
        if (available.compareAndSet(current, next)) {
            return true;
        }
    }
}

Suppose both callers read 1. Only one can change it to 0 with a successful CAS. The other caller’s CAS fails. It goes around the loop, reads again, and finds no stock left. The concurrent Java test checks the result. Exactly one reservation must succeed, and stock must finish at zero.

I also asked for changes that should fail

I wanted these checks in the normal build. ./mvnw test runs JUnit and Americium. With ./mvnw verify, the fixed model is also checked by TLC. The Lean proof is built with Lake, Lean’s build tool. If either formal tool fails, Maven fails too.

Then we deliberately broke each layer. First, the stock guard was removed from the fixed TLA+ model. Every reservation could now decrement stock. TLC found a negative value, and Maven failed. In Lean, the decrement was changed from one to two. Starting with one item would now produce -1, so the theorem was false and the proof failed. The same change in Java failed both the ordinary tests and the generated-input properties.

The correct versions were then restored. These failures give the kind of feedback I want an agent to receive. A rule has been broken, and there is a failure to look at. The agent can change its proposal and try again.

An unfinished proof needs to be caught as well. Lean lets you write sorry as a placeholder while developing a proof. Here, warnings are treated as errors by Lake. Replacing the proof with sorry fails the build too.

There is still something I have to review, though. Passing the TLA+ model does not prove that Inventory.java implements it. And passing the Lean theorem does not prove that the Java method implements the Lean definition. In the fixed model, the whole CAS loop is represented as one atomic reservation. The Lean theorem covers the local arithmetic. Some of the expected behavior is checked against Java through our tests. Proving the full connection between the code and the formal definitions would be another project.

An agent could change the Java code and leave both formal files alone. The formal checks could keep passing. So the Java tests stay in the build. I also need to review whether the model and the code still describe the same behavior before accepting the change.

What I want a software factory to retain

The code has been written, and the rule is still there in a form we can check. The next change can start from that same reservation rule. An agent can try a different implementation and run the checks we already have. It doesn’t have to find the rule again in my original prompt. That is one thing I want a software factory to keep for us.

The rule itself still has to be chosen by people. We decide that stock must stay at or above zero. Then we check whether the formal statement says that, and whether the modeled actions describe the behavior we care about. A proof checker can check the theorem it is given. It cannot decide whether we asked for the right thing. That decision stays with us.

I also want changes to the acceptance rules to be clear. If the task is to repair reserve(), the agent must not weaken NoOversell just to get a passing build. A changed business requirement can lead to a changed rule, of course. That change needs its own review. The same goes for deleting a test or skipping the formal checks in Maven. Those changes affect what we are prepared to accept.

For a future factory, I can see a repeatable process here. The agent is given a change with a clear scope. It proposes code and runs checks that have already been reviewed. A failure is returned to the agent for another attempt. There needs to be a limit on those attempts. Once it is reached, a person decides what happens next. A proposed repair that changes a requirement also needs that decision. For now, the demo provides the checks. An automated repair process could be the next experiment.

I expect this to fit small parts of an application first. With this reservation rule, the number of possible states is small enough to follow. More workers and more state can make model checking expensive. Larger proofs also need someone who understands the assumptions and can maintain them. Choose a rule where a failure has a clear consequence. Keep the model small enough that you can still read and question it.

This brings me back to the exit strategy for specifications. Once the change is understood and implemented, the brief can leave the agent’s active context. The lasting rule stays close to the code. It has an owner, a reason, and a check. The formal files need care too. When the Java behavior changes, their connection to the code needs to be reviewed. Writing a rule in mathematical form makes it precise. We still have to keep it in line with the application.

Try the small version

The companion project and setup instructions contain the Java example, both TLA+ models, and the Lean proof. Lean is installed through elan. The scripts download the TLA+ JAR and check its checksum.

With the prerequisites installed, run these commands separately from formal-java-demo/:

./mvnw test
./scripts/run-broken-tla.sh
./mvnw verify

The broken-model command is meant to fail. It shows a counterexample ending at stock = -1. The normal verify command uses the corrected model and completes successfully. You can then change the decrement or remove the guard. Run the checks again and see which one catches the change.

I want to keep trying this with rules I can understand. Here, the rule can be stated, the broken protocol can be found, and the repair can be checked again by the build. That gives me a step toward the software factory I want. More of the implementation can be handed to agents. The conditions for accepting a change are kept where they can be checked. People still decide what those conditions mean.

Thanks for reading The Main Thread! Subscribe for free to receive new posts and support my work.

Subscribed

Thank you for reading.

If this piece was useful, sharing it is the simplest way to support the work and help others find it.

Thoughts and corrections are always welcome. I read every comment.

If this email was forwarded to you, you can subscribe to receive future issues directly.

Write boring code. Ship exciting systems.

Subscribed

© 2026 Markus Eisele
🇩🇪