Trust Models for AI-Generated Code

Three sources of trust

Where does trust in the code come from?

AI can write code, and it writes a lot of it, very fast. So the question is simple. Where does trust in this code come from?

For me there are three sources. The first one is reputation — we trust the producer: a known team, a developer who did good work before. The second one is process — we trust the result because we can see how it was built and checked: the tests, the CI, the audits, the reproducible build. The third one is specification — we say in advance what the product should do and which properties must hold, and then we connect specification, code and formal verification.

None of these three is better than the others in general. Each one gives us a different kind of feedback about the system. And with agentic development the real question is whether these feedbacks, taken together, keep the system converging to the product we actually wanted. Because the tools generate and extend and rewrite so fast that approving one output is not enough. We have to keep the direction of the whole evolving system under control.

Agentic scale

Speed changes the failure rate

Agentic development produces and modifies software much faster than before. That part is good. The bad thing is what happens to the errors.

Imagine the quality of every single change stays the same. If we produce ten times more changes, we get ten times more chances for a missed error. The number of bugs per change can stay flat, and the number of bugs per second still grows — maybe even faster, because nobody really knows whether the code is good or not, and it carries a lot of small misinterpretations of the intent.

So the technical debt that used to grow over months can now grow in days: duplicated logic, assumptions that do not match, fragile interfaces, changes that look fine locally and weaken the whole system. And so the question is no longer only whether one change is correct. The question is whether the system, evolving this fast, still stays inside its constraints.

System dynamics

Evolution needs two feedback loops

I like to look at this from the perspective of evolution. Every evolution process must have two forces. One force is positive: it creates new things, it explores. The agentic loops do exactly this — they generate, they extend, they combine, they try. We need this force. Without it the system does not develop at all.

The other force is negative. It measures what we actually have now, comparing it with what we wanted to have, and then it makes us fix what we have. Biological evolution works like this, naturally. In software we have to build this second force on purpose.

So a healthy development system needs both. And the design question is not how to stop the agents from generating. The question is how to give the system a correction signal that still means something when the system gets big.

Reputation is a positive loop

Reputation amplifies success

Reputation is a positive-force mechanism. A brand does good work. The good work brings attention and resources. The resources let the brand do more work, and the brand gets stronger. This is a strong loop for incentives and for accountability — it tells us who stands behind the system and who has a reason to keep the quality up.

But reputation talks about the past. It tells us who succeeded before. It does not say anything precise about this exact result, the one being produced right now. And in agentic development this gets weaker still, because one artifact can depend on a human request, several models, tools, retrieved context, many generated steps in between. The line from one producer to one result becomes thin. A strong brand can still ship a bad version. So the history of success is useful, and it is not evidence about the current artifact.

Local negative feedback

Process creates local control

The process gives us real negative feedback, but locally. A function has unit tests. An interaction has integration tests. An environment has an end-to-end scenario. CI runs all of this again after every change. Each of these closes a small loop: produce something, compare it with an expectation, fix it if the check fails.

The problem is composition. A complex agentic workflow can have dozens of these small loops, and every one of them can be green. Every module passes. Every local interaction looks correct. And the system as a whole can still drift — because the components share a wrong assumption, or some important interaction has no test, or no local test represents the common product target.

Here I like the picture of a car. We have many processes that can locally drive it — stay in the lane, keep the distance, hold the speed. But the question is: where is the navigator? Where are we now, on the whole route? Local control does not answer that. So we need the local loops, and we also need something that checks the behaviour of the whole system.

Audit

Audit now works in both directions

LLMs made audit cheaper. We can read much more code, apply the same checklist every time, find suspicious patterns at scale, and get a lot of ideas back. That part is easy now. The harder part is what the audit is for, because an audit can work in two directions.

In one direction it stays inside the current design and looks for bugs — does the implementation follow the architecture and the requirements it was given. This is good for finding defects and for keeping the implementation in line. In the other direction it questions the design itself — maybe the architecture is wrong, maybe a threat model is missing, maybe the property we want is impossible with this design. This can improve the design a lot. And if every assumption is always open, the audit produces noise and the system never converges.

So the person who starts the audit has to say which things stay fixed and which things are allowed to change. Cheap review helps, and only when its objective is explicit.

Global negative feedback

The system needs a global constraint

I am not saying we should replace the process with formal verification. The working model keeps both. Inside the system the local checks keep doing their job — unit, integration, end-to-end, audit. Around them we add one stricter loop that compares the implementation with properties written formally, outside the code.

The specification is the external reference. Formal verification takes the selected properties and checks them against a formal model of the system. If a property fails, that failure goes back into the development loop as a correction signal — the negative force again, now on the level of the whole system.

Formal verification is not magic. It does not prove the whole product is correct. It does not tell us we picked all the important properties. It does not prove by itself that the specification matches what the human meant. What it gives is one thing the local checks cannot give: a precise statement that has to stay true across the modelled system, even while the implementation keeps changing.

Evidence map

What do we check — and how?

Verification is not one method. First we have to ask what kind of property we are checking, and only then choose the evidence.

For local behaviour, unit tests and fuzzing work very well. For interactions, integration and end-to-end tests walk selected paths, and model checking can go through a state model more systematically. For invariants and formal properties, deductive verification can prove a theorem under stated definitions and assumptions, and SAT and SMT solvers help with particular classes of constraints. Audit moves across all of these levels and asks the wider questions.

These methods overlap, and each one has limits. So the order matters: first fix the object and the property, then pick the evidence that fits the decision.

Unresolved engineering gap

Words are understandable. Formulas are precise.

A specification for people and a specification for machines are two different things. The first one is a sentence. We can say: a transfer must conserve value — what one account loses, the other account gains. A person reads this and understands the idea. But the sentence still leaves questions open. Are there fees? Can value be minted or burned? Which accounts, which states are included?

Going from human meaning to a formal property is still an open engineering problem. It is a technical gap, not something impossible in principle — but I do not want to present it as solved. A human still has to read the formula and confirm that this is what people meant.

Development loop

Formal methods belong inside the development loop

Everyday development is already a loop. We plan, we write code, we test, we audit or review, and then we go back and revise. This loop is the engine — it lets the product grow through many small cycles of building and feedback. Tests, audit and human judgement stay necessary here. They work on concrete behaviour, on integration, on usability, on architecture, on risks that a formal model may not even see.

The problem is that this loop can stay green locally and still drift away from the system-level properties we wanted. The plan changes little by little. The assumptions spread across components. The tests check what the code does today, and not what the product was supposed to guarantee.

So we keep this loop, and we put it inside a bigger one. The bigger loop adds two things: a formal specification that turns selected requirements into explicit properties, and formal verification that compares the evolving implementation with those properties. When the check fails, the result comes back into development. And this should be part of the everyday work, and not a ceremony we do once at the end — because if formal methods arrive only at the end, every later change makes the evidence expensive to rebuild and easy to ignore.

OrdoCode

How OrdoCode closes the loop

This is how OrdoCode puts that bigger loop into practice. First a person describes the product they want. That intent becomes a specification, and the human reviews and approves it before any generation starts — this approval is a real checkpoint. Then the system builds and verifies: it generates the code, runs the tests, supports the audit, and produces proof artifacts for the properties we agreed on. And finally the customer gets a package — the code together with tests, proofs and documentation — so we can show another party that this software really has the properties we claim.

Specification and verification become part of everyday development — not an external ceremony.

Cambrian is the source layer that makes this possible: a declarative language built for stateful semantics and for formal translation, so the same description connects the specification, the generated code and the proofs. I am not claiming the gap between human language and formal specification is gone. The specification can still be incomplete or wrong, and the formal evidence only covers the properties and artifacts it actually touches. What changed is the shape of the work: specification, approval, implementation and verification are one path you can review from end to end.

One step closer — not a final answer

From trusted to trustless operations

My last point is about trust itself. The goal is not to say that trust disappeared. People still write the requirements. People still choose which properties matter. People still read the specification, decide if the evidence is enough, and take responsibility for the decisions that sit outside the formal model.

But we can make fewer decisions depend only on how much we believe the producer. More of the assurance can be explicit: a specification you can inspect, checks you can repeat, evidence tied to a named property, and clear places where human judgement still has to step in.

The best system you can trust is the one that needs no trust in any single step. We are not there. We move from trust based mostly on identity and confidence toward operation backed by explicit, checkable evidence. The honest result is not zero trust. It is clearer trust boundaries and stronger correction signals. This is OrdoCode, and this is OrdoHub.

• ReputationAmplifies success and assigns accountability. It does not check the current artifact.
• ProcessCloses the local loops. Necessary, and not enough for global convergence.
• AuditCheap with LLMs. Works in two directions, so its objective has to be explicit.
• Formal methodsAdd a global constraint written outside the code. Bounded by the properties we chose.
• The gapHuman intent to formal property is still an engineering problem, handled by human approval.