Where to check an AI agent's workThe aggregate boundary and Rice's theorem

In short: what a person checks and what the agent does

Three zones of work with an agent: where it is free, where the check sits and where a person decides.

Inside the aggregate the agent works. It writes command handlers, database queries, data storage and tests. The agent can rewrite the whole internal structure: split a table in two, change queries, rework the processing. As long as the border holds, a person doesn't need to read every line.

The check sits on the aggregate border. This is where it is written which commands the aggregate accepts, which events it hands to neighbours and which rules always hold. A machine checks this border. A Quint model is a record of the system's rules in a special language, from which a program tries every possible order of commands and looks for one that breaks a rule. Database constraints are rules the database checks on every write, refusing to save anything forbidden. A person reviews only edits to the border itself.

A person holds the context border. Which aggregates live together and where word meanings change can't be computed from code: it depends on future changes. So a person sets this frame and moves it based on edit history and plans; more in “The first frame”.

Why you can't check all of an agent's code: Rice's theorem

The point. However clever the check of an agent's code, there is code on which it is wrong. Henry Gordon Rice proved this in 1951.

• What can't be checked: a program's behaviour, what it does when it runs. For example, “never charges money without an order”.
• The theorem's condition: some programs have the property and others don't. If all or none have it, the answer is known in advance.
• In detail, with the proof: “Rice's theorem in plain words”.

Two kinds of questions about a program. Mathematicians call a yes-or-no question a predicate. The theorem rules out an exact answer only for the second kind.

A practical move: rewrite the code so that an important rule becomes a question of the first kind.

A similar distinction exists between the imperative and declarative approaches. Imperative code describes steps, and in general you can't tell the result from them. A simple declarative notation, such as a database constraint, states what the result must be, and the database enforces it.

The code is the same. A question about the text is settled by reading a finite text; a question about behaviour requires going through every run.

Why a behaviour question can't be answered for every program follows from one construction. Take any program $P$ and any input $w$ for it; $P(w)$ means “program $P$ run on input $w$”. Build a new program $Q$: first it runs $P(w)$, and when that finishes it takes a step $B$ that breaks the rule, such as charging money without an order. If $P(w)$ never finishes, step $B$ is never reached and the rule is not broken. So a check of the rule for $Q$ has to know whether $P(w)$ finishes. The diagram below shows this construction, with the formulas and the conclusion right under it.

The proof in one diagram: checking the rule for $Q$ would tell whether $P(w)$ halts.

Step $B(x)$ breaks the rule, while a program that runs forever does not. So $Q$ reaches the breach only if $P(w)$ ever finishes:

If a check of the rule existed for every program, then given $Q$ it would also answer whether $P(w)$ halts. That question, the halting problem, no program can decide: Alan Turing proved it.

Three ways to make a check finite

Since there is no exact check for every program, the check is limited so that it no longer covers every program. There are three ways to do that: shrink the world being checked, narrow the language the code is written in, or let the check honestly answer “don't know”. The diagram puts all three side by side.

Left, trying a small world in full; centre, one write path into the database; right, three answers of the check, the third going to a person.

The table gives the same three ways in more detail: how each works, which condition of the theorem it removes and why the answer is then exact, and what is lost. What each way looks like for the rule “bookings of one room never overlap” is shown below, under “What it looks like in practice”.

More, with the proof of why each way lifts the ban, in “Rice's theorem in plain words”.

What it looks like in practice: one rule, three checks

Take the rule “bookings of one room never overlap in time” and an agent writing the booking code. Below, for each way: what exactly is written, what is run and what comes out.

Narrow the world: a Quint model. The rule and the system's actions are written as a short description, without real code. A state is a snapshot of the data at some moment: which bookings exist, for which room, from when to when. The actions are “book” and “cancel”. The rule is one line: for any two bookings of the same room, one ends before the other starts.

The rule in a Quint model

val noOverlap = bookings.forall(a => bookings.forall(b =>
  a == b or a.room != b.room or a.end <= b.start or b.end <= a.start))

The program then tries every sequence of actions for a small world: 3 rooms, up to 5 bookings. If the rule breaks anywhere, it prints the chain of steps. For example: two clients book room 2 for 10:00–11:00 at the same time, both “is it free” checks pass before either write, and the database ends up with two bookings for the same slot. That chain is the finding: the design error shows up before the agent writes any code. A small world is enough because such errors appear with just two or three bookings.

Narrow the language: the rule in the database and a single writer. The rule moves to where the database itself holds it, not the agent's code. In PostgreSQL this is one constraint on the bookings table: the database refuses to save a booking whose time overlaps another booking of the same room.

A PostgreSQL constraint

CREATE EXTENSION IF NOT EXISTS btree_gist;
ALTER TABLE bookings ADD CONSTRAINT no_overlap
  EXCLUDE USING gist (room_id WITH =, tstzrange(starts_at, ends_at) WITH &&);

The second half is a single writer: only one module may write to the bookings table. This is checked by searching the code text on every agent edit. The command below finds every file that writes to the bookings table except the allowed one; an empty result means “no bypass”.

The “single writer” check by code search

grep -rl "INSERT INTO bookings" src | grep -v src/booking/repository.ts

The question “can the agent's code create overlapping bookings” has turned into two questions about text: is the constraint in the database schema, and is there no write around it. Both get an exact answer.

Allow “don't know”: three verdicts on an agent's edit. The check on an agent's edit is built from the previous two and returns one of three answers. “Proved”: the Quint model passed, the database constraint is in place, the search found no bypass writes. “Broken”: the search found that the agent added a write to the bookings table from the reports module. “Not sure”: the agent builds the database query from strings on the fly, and a text search can't tell which table it writes to. Then the edit gets a “needs a person” label and a developer reviews it. The person spends time only on the third case.

Each of the three answers is exact only within its limits. The search proves the rule holds in a model with 3 rooms and 5 bookings, not in the production database with thousands of bookings. The code search proves there is no write around the rule, not that the database constraint itself is written correctly. A “holds” answer is exact, but some edits still go to a person. So the ways are used together: the model checks the design before code, the constraint and the search check the code itself, and a person looks at whatever is left with a label.

There is also a fourth option, the one most common in practice: always answer, but sometimes be wrong. Example tests and code review by another model work this way. It is an acceptable choice too, but a deliberate one: fine where an error is cheap, not for money and access. A similar fork is known from the CAP theorem about distributed systems: during a partition a server either waits or answers from a stale copy. They share one thing — while an event hasn't happened yet, you can't tell whether it will happen later or never, however long you wait — but the reasons differ; details in “Rice's theorem in plain words”.

The aggregate as a checkpoint: what event storming gives you

Event storming is a workshop format where a team lays out the business domain as events. Afterwards every aggregate has four things: commands that change it, events it sends, read models used to look at it, and invariants, the rules that hold in every state.

These four things form the boundary where a check fits well. Every change goes through commands, everything neighbours see leaves as events, and the rules live in one place. This is exactly the second way from the previous section: only the aggregate writes to its table, so no other code can break the rule, and only one thing remains to check: that nothing else writes to that table.

The checkpoint sits where commands enter and events leave. Inside the border the agent is free.

The table goes row by row: which of the aggregate's four parts sit on the border and are checked by a machine and a person, and which stay inside and are done by the agent without line-by-line review.

How to size a bounded context: by checkability

Going from a business domain to bounded contexts is the hardest part of DDD. The usual signs of a border: a word starts to mean something else, the team changes, rules no longer have to hold at the same time.

How to apply the criterion to your project. Take a part of the system you consider a candidate context, such as “booking”, and check it in five steps.

1. List the rules and actions. Rules are what must always hold: “bookings of one room never overlap”. Actions are commands that change data: “book”, “cancel”.
2. Write them as a Quint model. The state is which bookings exist; actions are how they change the state; rules are checks after each step. It's tens of lines, no real code.
3. Pick small numbers. 2–3 objects of each kind: 3 rooms, 5 bookings, 2 clients. Usually that is enough for the typical nasty combinations to appear: two bookings of one room, two clients in the same minute. There is no guarantee: an error that needs more objects will slip by.
4. Run the search with a time limit, say 10 minutes.
5. Read the result with the table below. The search finished with no breaches: the size fits. It finished and showed a breach: the size fits, but the rules or actions have an error to fix. It didn't finish within the limit: there are too many states, and the candidate is split.

Running the search for the booking model

quint verify booking.qnt --invariant=noOverlap --max-steps=10

How to split if the search didn't finish. For each rule, write down which data it touches. Rules with no data in common go into different parts: “bookings never overlap” touches only bookings, “an invoice is never paid twice” touches only invoices. Between the parts, leave events such as “BookingCreated”. Then check each part with the same five steps.

If a context's model answers “not sure”, the context is split, and only events remain between the parts.

How to use this sign: write the context's rules as a Quint model, set small numbers and run the search. The result falls into one of the table rows, and the last column says what to do next.

The first frame: why it will be wrong and how to make it cheap

The frame was drawn around bookings and rooms. If an edit about bookings and rooms comes next, the frame fits. If an edit about bookings and invoices comes, it crosses the border and the frame has to move. Which one will come can't be known now: that is the open question.

What remains to be found out:

• whether choosing a frame can be stated strictly as a problem of missing information, as was done for CAP, or the resemblance is only verbal;
• how well the history of past edits predicts future ones: there are no measurements, only observations from individual projects;
• what length of review cycle for the frame works: the two weeks below are an example, not a tested number;
• how two questions relate: how big a part should be (Rice's theorem helps here) and where to draw its borders (this needs information about the future).

Choosing a frame runs into a different ban from Rice's theorem. A code check has all the information, the whole code is in front of it, but the answer can't be computed from it. A frame lacks the information itself. A good frame is one where future changes will live, and there is no data about the future in the code or anywhere else. This is exactly the position of the server in the CAP theorem: it doesn't know what happens at its neighbour beyond the broken link, and here nobody knows which edits will come next month.

So the ways out are the same as in CAP. Waiting until the future becomes known isn't possible: the work happens now. What remains is to answer now with what is available and be ready to be wrong. “What is available” is two approximations of the future: the history of past edits, which shows what usually changes together, and your plans, which only you know. And the third way out of CAP, bounding the time, turns into agile's short cycles here: set the frame for two weeks, watch how edits live in it, and move it. Since the frame will be wrong anyway, what matters is that moving it is cheap.

Rice's theorem still takes part in this section, in a different role. It doesn't help guess the future, but it gives a check of a frame already chosen: if a Quint model of a part's rules can be searched to the end, the part is small enough; if not, it should be split. That sign was covered in the section on context size.

Where the first parts come from

You don't need to know the parts in advance: the first cut comes from what already exists, and a person only names the parts and fixes the disputed spots.

How gluing by rules works. List the data rules, for example “a closed epic has no open report”, “a token sees only its own projects”. If a rule mentions two tables, they go into one part. The resulting groups are the first cut.

The groups of glued tables are the first cut. A table everyone needs becomes a shared core.

Where a rule ties almost everything together, like a report status needed by both epics and the board, that table becomes a shared core with one owner. The other parts reach it only through that owner. Only the core writes to the status table, so neither epics nor the board can break the status rule.

Where Gödel fits: only as an analogy

The link between Gödel's incompleteness theorem and this topic is my own assumption; I haven't found sources that draw it. The reason for it: both Gödel's and Rice's proofs rest on the same trick, a program or formula that talks about itself. But Gödel's first theorem concerns formal systems in which elementary arithmetic can be carried out, and says nothing about the borders of a business domain. For the argument about checking an agent, the exact result is Rice's theorem.

The second theorem is useful as an analogy: such a system cannot demonstrate its own consistency. Translated to agent work: an agent can't confirm on its own that it did the job right; it needs a checker outside its frame. This is an image, with no mathematical conclusion behind it.

Frequently asked questions