Verification & Observability

This is one of the biggest mindset shifts in harness engineering: you do not trust the final sentence because it sounds confident. You ask what external checks can back it up.

Verification: asking for receipts

For coding work the receipts are easy to name: tests run and pass, the build compiles, types check, lint is clean. For a presentation, it might be a browser screenshot with no overlapping text. For research, primary sources and a claim table. The shape varies; the principle doesn't — "looks good to me" is not a verification strategy.

Here's the telling detail: when an agent finishes a change and says "now let me run the tests" without being asked, people credit the model's intelligence. Some of that is real. But for a long time that behavior was a differentiating feature of specific harnesses — because the harness was engineered to steer the model toward verification as a step. The model does the checking; the harness made sure checking happened.

The bill moved to this layer

Why the cost landed here — on the checking rather than on the producing — is easiest to hear from someone with no stake in software.

Ken Ono is a number theorist, on leave from the University of Virginia and now the founding mathematician at Axiom Math. He was one of the professional mathematicians a Berkeley company, Epoch AI, hired to assemble very difficult problems for its Frontier Math program — a set built to measure what the models could do as they improved. The interview opens on the moment he could no longer write a question ChatGPT got wrong, and on the months he spent afterwards asking the wrong question about it, which was how do I stay ahead?

From the talk

"Nobody would be interested in watching Usain Bolt race against a motorcycle in the 1-mile run. It's not a fair race. But we still watch the Olympics."

"Information, knowledge is now cheap. But how you use it and how you verify it has become more expensive."

That second sentence is this sheet, said about knowledge in general rather than about a refund. Producing a plausible answer collapsed in price. Establishing that a particular answer is the answer did not — and it is now demanded of far more answers, far more often, by whoever is left holding them.

What got cheap, and what got expensive

Ono’s ordering — the talk publishes no measurement of either

1. 01Knowledge — what has been written downCheap
2. 02How you use it, and how you verify itMore expensive
3. 03The librarian — wrong, and you walk back to the shelf
4. 04The neurosurgeon and the air traffic controller, level with each other — wrong, and there is nothing to walk back to

Whose is whichThe two movements and the three roles are the talk’s, in its own words. The axis they are laid on is this sheet’s reading of them: he sorts the roles by where human judgment is important, and this reads that sorting as a question about reversibility. Neither register carries a scale, because the source published none.

His frame for what the model is: the most extraordinary librarian the world has ever seen. If it has been written down, the librarian has read it. Then the question that does the work:

From the talk

"Do you want your librarian to be your neurosurgeon? Do you want your librarian to be your air traffic controller, somehow keeping an eye on the hundreds of planes that are flying over North America or Korea? No way, because that human judgment is important."

Read as a harness question, the axis he is sorting on is not accuracy. A librarian and an air traffic controller can be wrong at exactly the same rate; what separates them is what a wrong answer does before anyone notices. The librarian's mistake costs an afternoon and is undone by walking back to the shelf. The controller's is not undone at all.

That axis is the one this layer is built along, and it sets the shape of everything below. Where a wrong answer is reversible, the receipt can be cheap and late — run the suite, read the trace, try again. Where it is not, the check has to sit before the act, and be made of something the model cannot talk its way past. Instructions are how you brief a librarian. They are not how you clear an aircraft.

No eyes

That leaves the question of why the bill cannot simply go unpaid. Plenty of trust gets extended every day without a receipt, and it mostly works. Understanding why that option is closed here takes a second witness, and the best one is not talking about software at all.

Po-Shen Loh is a Carnegie Mellon mathematician who describes himself as having been distracted by the real world; his subject now is what people are still for once the machines are good at things. He gets to the point through a car.

From the talk

"An EV is basically a computer with four wheels. … Many of the electric vehicles get constant software updates. What would happen if somebody hacked into the software update system? Next week, one particular brand of EVs at 5:30 p.m., they all accelerate to full 100%."

"And if you ever tried editing code, you know that it's actually possible to make weird things happen without even fully understanding, especially if the code was written with AI. So the car which was supposed to help you can change into the car that was supposed to hurt you. You have absolutely no way of knowing because it has no eyes."

The last four words are the ones to keep, and they only land because of what he says next about people:

From the talk

"The beautiful thing about humans is that you can tell when you talk to someone, this person cares about the big picture more than just about themselves. You will never be able to get that confidence looking at a robot's eyes."

Take that at face value and it is a claim about when the evidence exists. With a person, intent is legible before the act. You read it off a face, continuously, at no cost, using equipment you did not have to install — and most trust between people is this and very little else. No suite, no ledger, no trace. A channel that is simply on.

A system has no such channel. Nothing is readable before the act, so nothing can be trusted in advance, and everything that might be trusted afterwards has to be manufactured out of whatever the harness thought to keep.

When the evidence exists

Loh’s asymmetry — the before/after axis and the decoy are ours

1. 01A PERSONBefore — Intent is legible before the act — continuous, free, no instrumentAfter — Still legible. The channel does not close.
2. 02A SYSTEMBefore — Nothing. There is no channel to read, and no eyes to read it in.After — Only what was recorded. Anything not written down did not happen.

Which changes what this layer is. A trace is not diagnostics you bolt on once the thing is in production and the incidents get embarrassing. It is the channel — the only one — and a run that went unrecorded is a run nobody is entitled to an opinion about.

It also names the misread this sheet opened on. The most eye-like thing an agent produces is its narration. Now let me run the tests arrives in the voice of someone telling you what they mean to do, at precisely the position on the plate where a person's intent would sit, and it reads as a signal because we have been reading that signal our whole lives. It is a prediction about a plausible next sentence. Whether a test ran is decided somewhere else entirely — which is exactly why one of the two is free and the other is not.

So the receipt is not a nicety, and the rest of this sheet is about what happens when you go looking for one and find that it does not exist.

The receipt that does not exist

Tests work because code has a truth you can execute. Point the same instinct at an agent that handles orders and the receipt evaporates. There is no test suite for this customer has already been refunded.

Three failures, from a support agent wired to a real ledger:

• It issues a second refund on the same order. The order was refunded last week; the customer says otherwise; the agent believes the customer.
• It sends a payout to the support desk instead of the buyer. The rep's id is the one in the thread, because the rep did all the talking.
• It sets an order status to "probably shipped." Hedging under uncertainty is exactly what a probabilistic system does.

Every one of these passes a type check, passes a lint, and would pass any test you thought to write — because you would have had to think to write it. Every one is a sentence a reasonable person would sign off on. And every one moves money or lies to a customer.

The reflex is to write the rule down. Never refund an order that has already been refunded. But instructions are the first harness layer for a reason: they are passive, and forty turns into a conversation a line in the system prompt is one suggestion weighted against everything else in the window. English is not a constraint. It is a preference expressed in the same medium as the mistake.

Probabilistic inside, logic outside

Frank Coyle's diagnosis is blunt: this is not a prompt problem, and no amount of prompt engineering closes it. A language model reasons probabilistically over a domain it only half understands. Hallucination is not a defect to be trained out — it is the mechanism. The same machinery that imagines a plausible refund also imagines a plausible refactor. You do not want it gone. You want it fenced.

The name for the fence is old. Neurosymbolic — a neural system doing the probabilistic work, a symbolic one holding the rules — puts the two lineages of AI back in the same room. Agents descend from McCarthy and Minsky and the 1956 summer that named the field: things that perceive, decide, and act. Ontologies descend from Aristotle's categories of being, by way of Quine, and land on Tom Gruber's 1993 definition, which the talk relays as the useful one: a formal specification of a shared conceptualization.

That is what an ontology gives an agent — your conceptualization of your domain, written where the model cannot argue with it.

What an ontology actually is

Strip the word of its weight and it is a graph: entities, the relationships between them, and the properties they carry. Orders, customers, support reps, payments — and the fact that an order is placed by a customer. It is a graph rather than a table because a table resists change. Add a fact to a relational schema and you add a column and migrate everything; add a fact to a graph and you attach it.

You build one from the top down or the bottom up. Top-down is the expert-systems move: get the people who know the domain in a room and name the entities, the properties, the relationships. Bottom-up is mining what already flows through the system — these are the things customers do, so these are the entities we have. Both are legitimate, and neither is a weekend.

Much of it you should not build at all. schema.org has fifteen years of terms for commerce and content. FOAF models people and their connections; Dublin Core models documents; Wikipedia's structured half is DBpedia. Reusing a taxonomy someone else has already argued about is not a shortcut — it is the difference between a vocabulary and a private dialect.

The constraints are the part that earns its keep, and there is less of it than the vocabulary suggests:

:Customer    a owl:Class ;
             owl:disjointWith :SupportRep .

:placedBy    rdfs:domain :Order ;
             rdfs:range  :Customer .

:hasRefund   a owl:FunctionalProperty ;
             rdfs:domain :Order .

:OrderStatus a owl:Class ;
             owl:oneOf (:paid :shipped :refunded) .

Eight lines. They say a customer and a support rep are different kinds of thing, that an order has at most one refund, and that a status is one of exactly three values. Those are the three failures above, refused in advance.

The schema does more than refuse

A constraint that only says no would still be worth having. But RDFS and OWL sit beside the graph and derive — the same declarations that reject a bad write also produce facts nobody stored.

Declare that :teaches has a domain of :Teacher and a range of :Student, and one asserted triple — Bob teaches Scooter — tells you Bob is a teacher and Scooter is a student. Add that every teacher is a person and Bob is a person too. You wrote one line; the ledger holds four.

Two more axioms do most of the remaining work. Transitive properties chain: if Sue is an ancestor of Mary and Mary of Ann, Sue is an ancestor of Ann. Functional properties mean at most one — one father, one mother, one refund. That second one has a sharp edge worth understanding, because it is how the reasoner catches the duplicate refund. Assert a second value on a functional property and OWL does not warn you. It concludes the two values must be the same individual — and if you have declared them different, what comes back is a contradiction.

Pydantic at the door, ontology at the ledger

Now put it in the loop. An agent is a while True around a model call: propose, act, observe, repeat. Loops are what make the thing Turing-complete, and they are also how it goes wrong — a loop can spin forever, drift as agents talk to each other, and bill you the whole time.

The model itself cannot act. It reads the tools, decides this one, with these arguments, and stops with a reason. Everything after that stop is the harness's, and it is where two checks go — one on the shape of the request, one on the meaning of the result.

while True:
    resp = client.messages.create(model=MODEL, messages=msgs, tools=TOOLS)
    if resp.stop_reason != "tool_use":
        break                              # talking, not acting

    call   = get_tool_use(resp)
    args   = RefundArgs(**call.input)      # ← the door: types, or raise
    result = run_tool(call.name, args)     # still no side effect

    verdict = ontology.check(result)       # ← the ledger: meaning, or contradiction
    if verdict.ok:
        commit(result)                     # only now does anything happen
    else:
        msgs.append(bounce(call, verdict)) # or hand it to a human

00Well-formed01Wrong type02Second refund03Wrong payee04Bad status

Door✓ clears

Ledger✓ clears

Committed — the side effect runs

The model proposes

set_status(order="A-1041", status="shipped")

The happy path, so the machine is legible before it starts refusing things.

The ledger

• :order-A1041:placedBy:cust-77
• :order-A1041:status:paidretracted
• :order-A1042:placedBy:cust-77
• :order-A1042:status:refunded
• :order-A1042:hasRefund:refund-9
• :refund-9:amount79.00
• :cust-77a:Customer
• :rep-17a:SupportRep
• :order-A1041:status:shippedwritten

At the door ▸Both arguments parse. A-1041 matches the id pattern, and status is a string — which is all the door was ever asked to know.

At the ledger ▸“shipped” is one of the three declared members, so the write is legal. Because :status is functional, the reasoner retracts :paid rather than stacking a second status beside it. Functional does not mean frozen — it means one at a time.

At the door · Pydantic

• ⚑order: OrderIdmust match ^A-\d{4}$
• ⚑amount: Decimalpositive, two places
• ⚑status: strany string — the door has no opinion about which
• ⚑to: PartyIdan id that exists in the ledger

At the ledger · RDFS & OWL

• ⚑:hasRefund a owl:FunctionalPropertyat most one refund per order
• ⚑:status a owl:FunctionalPropertyone value at a time — a new one retracts the old
• ⚑:OrderStatus owl:oneOf (:paid :shipped :refunded)three members, and no fourth
• ⚑:payTo rdfs:range :Customerwhatever sits to the right of :payTo is a Customer
• ⚑:Customer owl:disjointWith :SupportRepnothing can be both

The ordering is the whole design, and the talk compresses it into a line worth keeping: Pydantic at the door, ontology at the ledger. Types catch the malformed call cheaply, at the boundary, before anything runs. The reasoner catches the well-formed call that is wrong about the world. And the tool runs pure — it computes what would happen and hands it over, so the side effect waits behind the verdict rather than racing it.

Where the reasoner stops working

A reasoner is not a second opinion. It knows exactly what you modelled and nothing else — so an ontology that is wrong is a confident wrong answer with logic's authority behind it, which is worse than no ontology at all. And it is a standing maintenance cost: the domain moves, a new status is added by the payments team, and the constraint that was protecting you starts rejecting legitimate work. This is the failure that ended the expert-systems era, and adding a language model next to it does not repeal it.

It also cannot tell you why. It catches the second refund; it has nothing to say about the forty turns that made the second refund look like the right thing to do. The check fires at the ledger, and the bug was upstream.

Observability: the flight recorder

Verification tells you whether something passed. It cannot tell you why it failed. A test fails — was the context wrong? Did a tool return bad output? Did the agent edit the wrong file? Did a sub-agent miss a constraint?

Without a run record, debugging an agent is folklore. Observability is the recorder:

• Traces — the full chain from user intent to final output
• Tool-call timelines — what was called, with what arguments, what came back
• Constraint violations — which axiom refused what, and how the model answered
• Recall decisions — which memory the harness pulled forward, under which policy, and whether it was the slice that mattered. Recall is measurable, and a policy nobody measures fails silently: the agent answers confidently from whatever did arrive
• Prompt and tool versions, costs, latency, approval events

In the wild

Eval suites that score agent runs. Trace viewers that replay every step of a session. Cost and latency dashboards per tool. Approval-event logs. Typed tool arguments and a graph store the harness checks writes against. If your agent product can answer "what exactly did the model see on turn 14?", it has this primitive.

Knowing isn't improving

Now the harness can prove what passed, refuse what contradicts the domain, and inspect why things failed. One question remains — the one that separates a good agent session from a good agent system: does any of this make the next run better?