pub fn recent_orders(
db: sql.Db[ReadOnly, schema: "orders"],
who: auth.AuthedCustomer
) -> Result[List[Order], sql.Error] may sql.read, alloc
ensures forall o: Order in result: o.customer == who.idRead-only access to one schema, a caller who has already passed authentication (the type can only be produced by the auth module), no other effects, and every returned order belongs to that customer. The compiler proves the last line from the query itself. A reviewer reads this and moves on.
Most of the effort in AI-assisted development now goes into steering: prompt wording, conventions documents, linters bolted on after the fact, and review that means reading every line the model produced. The specification of what the code must not do lives in prose, and prose is not enforced. When the model gets it wrong, someone notices — or doesn't — after the fact.
The root of it is the language. Current languages were designed so a human could write them quickly. They trade checkability for convenience at every turn: inferred types, implicit conversions, reflection, exceptions, ambient state. None of that convenience helps a model, and all of it hides things a reviewer needs to see.
The tools inherit the problem. A linter runs after the code exists and can only pattern-match what the language failed to say. A review tool shows a diff because there is nothing better to show. A prompt carries the rules because nowhere else can hold them. All of them try to catch problems after they exist, and none of them can see what the model was actually told. Fixing this starts at the language, but it does not end there: once the compiler knows what the code is allowed to do, the loop that drives the model, the ledger, and the review tool can be built on what it knows instead of on what it cannot see.
Onus moves the constraints out of the prompt and into the compiler.
path declaration states what a section of the program may do, and the compiler checks every function reachable from it. If the path declaration is right and the program compiles, the bodies don't matter.draft, where interfaces change freely and nothing is authoritative, next to a core that is already hardened or critical. The compiler keeps the core from depending on anything the draft has not yet hardened, and a module moves up only by earning it: its bodies are regenerated from its interfaces alone, and anything that does not come back was never written down.The language is the root, and it is the smaller half. Around it sits the environment: the loop that drives the model, the ledger the compiler writes, and the workbench a person reviews in. Each exists because the compiler knows what the code is allowed to do, and none of them guesses.
Signatures, contracts, effects, capabilities, paths, and each module's zone. This is the whole specification, and it is the only thing a person writes. If a convention matters, it is a claim; if it is not a claim, nothing downstream knows about it.
Contracts →The loop drives the model against the compiler. It sees interfaces and diagnostics, never a conventions document. It edits bodies and never claims, and the module's zone decides what it may touch at all. When a contract cannot be met it stops and proposes, rather than weakening anything to get green.
The loop →Every obligation ends proved, checked at runtime, or assumed, and the ledger records which, with every assumption's justification and where every capability came from. There is no linter and no second analysis: nothing runs after the fact to catch what the language failed to say.
The ledger →The workbench renders the ledger, path reports and interface diffs, and computes nothing of its own. Approvals, contract edits and answers to counterexamples return to the loop as tasks. A module earns promotion to a stricter zone by regenerating cleanly from its interfaces alone.
The workbench →Those four stages run once per change. Zones run across the project's whole life, and each module moves through them on its own. A module starts as draft, where interfaces can change freely and nothing is authoritative; it is promoted to hardened when it goes into service, and to critical when it becomes load-bearing, each step earned by regenerating its bodies from its interfaces and finding nothing missing. Nothing forces the project to move together: a subsystem being sketched sits beside a core that is already critical, the compiler refuses to let the core depend on anything the sketch has not yet hardened, and a module that needs rework is demoted alone, with everything that rested on it marked conditional until it earns its way back. Zones in practice →
This is the review artefact for the checkout endpoint of the third worked example: every function reachable from handle_checkout, the effects the path is bounded to, the obligations on it and what discharged each, and every assumption with its justification. Bodies are not shown because the reviewer does not need them. Nothing here was drawn by hand: it is rendered from examples/checkout/review/review.json, which onus review wrote.
path checkout · entry checkout.handle_checkout · 14 functions reachable · effects within alloc, io.clock, io.net, sql.read, sql.write · requires app.contracts.Idempotent · passes
entryfunctionintrinsiccarries an assumeassumption outside the project, permitted by except
Obligations on the path: 8 proved · 0 checked · 0 assumed · 0 failed · capabilities constructed on the path: sql.Db[ReadOnly] at checkout.handle_checkout:89:44
| Obligation | In | Status | Discharged by |
|---|---|---|---|
requires parse_select(text: text) is Ok | load_basket | provedpinned | const evaluator |
requires columns_match(text: text, record: row) is Ok | load_basket | provedpinned | const evaluator |
refinement it >= 0 | load_basket | proved | z3 |
refinement it >= 0 | handle_checkout | proved | z3 |
ensures result is Ok implies caller == customer | require | proved | z3 |
ensures result is Ok implies caller == customer | require | proved | z3 |
refinement it >= 0 | charge | proved | z3 |
ensures result == (len(xs: xs) == 0) | is_empty | proved | z3 |
The amber leaf is the one thing on this path that nobody can check: the payment vendor's promise to deduplicate on the idempotency key. The path's policy forbids assumptions outside the project, and names this one as the exception, so it appears here rather than being forgotten. Written by onus review on 3 September 2026; the review page it produced is served unchanged.
A team's conventions document says: reporting code must never write to the database. Today that lives in a prompt, a checklist, and a reviewer's memory. In Onus it is the function's own signature.
may sql.read, alloc is the complete list of what this function may do, and everything it calls must fit inside it. The model, asked to add run logging, writes an insert into a helper the report calls. The build fails before anyone sees it.
The model reads the diagnostic, moves the logging to the caller that holds write access, and the build is green. No prompt was edited, no reviewer read a diff, and the rule cannot be forgotten by the next model or the next person, because it is not advice — it is the function's type. For rules a signature can't express — required guarantees, which assumptions are acceptable, what must hold across a whole critical section — a path declaration applies the same check over every function reachable from an entry point.
reporting.onuspub fn monthly_totals(db: sql.Db[ReadOnly], year: Int) -> Result[List[MonthlyTotal], sql.Error] may sql.read, alloc -- everything this function calls must fit inside sql.read, alloc
$ onus check reporting.onusreporting.onus:17:3: E0201 undeclared effect in monthly_totals calling `log_run` has effect `sql.write`, which `monthly_totals` does not declare $ onus check reporting.onus # after the model moves the logging ok
A codebase is never uniformly trusted, and it does not have to be. A subsystem being sketched lives beside a core that is in service, under different rules, and the compiler enforces the one rule that makes that safe: nothing at a higher zone ever rests on a claim from a lower one.
recover.To build against the core, a draft module hardens its boundary first, and the core is permitted to see only that boundary. To move up, a module earns it: its bodies are thrown away and regenerated from its interfaces, and whatever does not come back was never written down. There is no manual override. How zones work in practice.
onus.toml[zones] "app.core.*" = "critical" "app.reporting" = "hardened" "app.payments.*" = "draft" $ onus zone promote app.payments hardened audit: 2 findings → proposals opened. Not promoted.