Trust Before Ship

Codex builds the feature. Trust Before Ship proves whether it kept its promises.

Comment

AI coding tools can now build working software remarkably quickly. But a working application is not necessarily a trustworthy one. A feature may compile, pass a basic test, and appear correct while still failing in important ways—creating duplicate records, accepting unauthorised actions, mishandling money, or leaving incomplete audit evidence.

Trust Before Ship was inspired by a simple question:

Codex built the feature. How do we prove it kept its promises?

Instead of treating generated code as correct because it runs, we define the operation’s obligations first and test the implementation against them.

What it does

Trust Before Ship demonstrates this approach using a small invoice-creation operation.

The operation must satisfy eight declared obligations, including:

invoice totals are calculated by the server; line items and monetary values are bounded; tax follows an explicit policy; mixed currencies are rejected; client-supplied totals are never trusted; retries do not create duplicate invoices; the invoice and audit record are committed atomically; only an authorised actor can create the invoice.

Alongside the correct implementation, the project contains four deliberately defective variants:

the same idempotency key is accepted with different invoice data; unlimited line items are accepted; an unauthorised actor can create an invoice; the invoice is saved without its audit record.

A separate, contract-derived behavioural checker tests each defective variant and the clean implementation, producing a simple evidence view:

what the software promised; what was implemented; which behaviour was tested; whether the obligation passed or failed; what remains outside the demonstrated scope.

The point the type system misses. All four defective variants compile and pass strict TypeScript type-checking with zero diagnostics—and still violate their obligations at runtime. A green build and a clean strict type-check are not evidence that the software kept its promises. Only the behavioural checker catches the difference.

How we built it

We used Codex to implement the invoice operation from a written contract rather than from an open-ended feature prompt.

The implementation and verification were deliberately separated. One workstream built the operation. A separate workstream created the behavioural checks from the same declared obligations without relying on the implementation’s internal enforcement logic.

To be precise about what “independent” means here: the separation is by author and role. The checker’s author derived the checks from the contract and did not read the implementation’s enforcement logic. It is not a different-vendor audit. Independence in this project means role-and-evidence separation, not one vendor auditing another.

The defective variants sit behind a test-only fixture boundary and are never exposed through the public application interface. This allowed us to demonstrate both sides of the experiment: the checker detects each known contract violation, while the clean implementation passes the same checks.

We also exercised the operation as a running service under stress, including concurrent duplicate requests and a storage failure injected midway through the operation. This confirmed that “no duplicate on retry” and “invoice and audit commit together, or not at all” held under the tested conditions.

We were careful to state the mechanism honestly: the operation is synchronous, so these observed guarantees depend on that design. We do not claim protection against every possible race, deployment model, or distributed failure mode.

Challenges

The biggest challenge was defining what “independent verification” honestly means. A separate checker can demonstrate that declared, planted violations are detectable. It does not prove that every unknown defect has been discovered.

We therefore narrowed the claim:

Trust Before Ship demonstrates separate-author, contract-derived verification of selected obligations, seeded defects, and a clean twin.

Other challenges included:

defining bounded idempotency rather than claiming impossible universal “exactly once” behaviour; separating design review from behavioural verification; ensuring defective variants could never leak into the clean public interface; defining the invoice-and-audit atomicity rule precisely; keeping simulated assumptions separate from genuinely confirmed requirements; reporting coverage limits rather than presenting a false assurance of completeness. What we learned

The most important lesson was that software promises need to be explicit before they can be tested. A vague instruction such as “build invoice creation” leaves critical questions unanswered:

Who is authorised to create the invoice? What happens when a request is retried? How many line items are allowed? What happens if storage fails halfway through? Can the invoice exist without its audit record? Which totals come from the server, and which can be trusted from the client?

Writing these obligations first exposed failure paths before implementation.

We also learned that generated code and generated tests should not be treated as independent evidence merely because both pass. Verification needs separation of roles, visible traceability, deliberately broken variants, clean twins, and honest coverage limits.

What is next

Trust Before Ship is intentionally a narrow proof using one invoice operation.

The next step is to test whether the same approach scales across other operation types, including:

read and search operations; external payment-service calls; multi-step workflows; operations involving retries and partial failure; larger AI-generated applications and codebases.

The long-term goal is to help teams move from:

“The AI built it and it seems to work.”

to:

“The software’s critical obligations were declared, tested, and supported by visible evidence.”

What this project proves—and does not prove

This project demonstrates that selected invoice obligations can be implemented and separately checked through the public interface.

Four of the eight obligations have deliberately planted counter-examples that the checker detects. The remaining four are exercised against the clean implementation but do not yet have planted violating variants. For those obligations, the project demonstrates expected-behaviour coverage, not proven defect sensitivity. We report this limitation rather than hide it.

It does not claim that:

every unknown defect is found; the application is production-ready; one operation proves an entire codebase is trustworthy; software safety can be guaranteed or certified.

It is a bounded experiment in making AI-generated software more testable, explainable, and trustworthy.

Built With

Share this project:

Updates