This article presents ten poly examples that show how your code is checked, what the check finds and what it proves. Each one is a working program checked CLEAN. Beside it is a copy with one defect put in on purpose. The check names that defect with a code and the shortest path that leads to it.
The ten programs, their policies, the defect copies and the tests are in examples/ in the repository, each with a README in docs/examples/.
Tests cover the paths someone thought of. Agents are goal-oriented systems: they choose their own steps toward a goal, along the paths nobody thought of. Today's large engineering teams answer with more sampling. Stripe's coding agents rely on over three million tests, Amplitude routes each agent pull request by its assessed risk, and Spotify's background agent verifies its changes with builds and lint checks. Each of these checks the paths that ran. A proof covers every path that can run, including the ones no test reached.
The same gap appears at four levels, and at each level the number of paths grows. Trust is often called scarce when agents do the work. What is scarce is trust you can prove.
The check runs before the code does. A defect comes back as a code and a path, which the agent can use to fix it.
Every example; the defect copies show the findings
An agent is a program with state. Its model calls, tools, budgets and outside calls are steps the check explores.
Agents send each other messages, in any order. The check covers every order, and the properties of the crew as a whole.
A model of the device or business the agents act on. Their actions are checked against what it allows.
flash-controller, a small model of a device
Sources: Stripe, Minions part 2 · Cursor, Amplitude · Spotify Engineering
Each example has the same parts. The program and its policy are checked together. A copy of the program has one defect, and the check must report exactly the finding named on its first line. A TypeScript host runs the program on recorded traffic: no API key is needed and nothing goes over the network. The run leaves a journal, and replaying the journal gives the same results.
Each .poly file starts with the verdict it expects, for example // expected: FINDING PL3002. The test suite and the release gate compare the check's verdict with that line.
The examples go from the simplest (no outside call, no model) to the richest (three agents checked together). The finding is what the check reports on the defect copy. The path is the sequence of steps that leads to the defect.
| Example | What it shows | Key property | Seeded defect | Finding | Path |
|---|---|---|---|---|---|
flash-controller | Erase, program, verify, a retry limit | Never programmed unless erased | Erase check removed | PL3002 | 2 steps |
appointment-booker | Model reads a date, calendar call once | No slot booked twice | Overlap check removed | PL3002 | 6 steps |
subscription-cancel | One offer, cancel once | A request always ends | Decline offers again | PL3301 · PL4001 | loop of 6 · 3 |
incident-oncall | Timers, page once, person when unsure | A page is answered | Unbounded snooze | PL3301 | loop of 9 |
expense-approval | Approver check, person above 200 euros | Approver is not submitter | Submitter can approve | PL3001 | 3 steps |
claim-intake | Two models, person below 0.8 | Queued alone only at 0.8+ | Confidence misused · never checked | REFUSED PL1205 · PL3002 PL6201 | none · 2 |
order-fulfilment | Undo steps, two orders | Cancelled holds nothing; never oversold | Undo steps skipped | PL3001 | 4 steps |
pr-reviewer | Agent tools, budget | Never merges | Merge made reachable | PL4001 | 5 steps |
support-drafts | Private notes, owner approves | Notes never reach external model | Notes sent to it | PL6503 · PL7001 | 1 step each |
research-agents | Planner and two workers, shared budget | Every report has cited | A worker that guesses | PL5401 | 6 steps |
Read down a column to find the examples that use a feature. A one-shot call is an outside call that cannot be undone (a payment, a booking, a page) and is sent only once. A policy rule denies a step or sends it to a person.
| Example | Model decision | One-shot call | Timers | Always ends | Policy rules | never rule | Budget | Two models | Several machines | Data audiences |
|---|---|---|---|---|---|---|---|---|---|---|
flash-controller | · | · | · | · | · | · | · | · | · | · |
appointment-booker | ● | ● | · | · | ● | · | · | · | · | ● |
subscription-cancel | · | ● | ● | ● | ● | · | · | · | · | · |
incident-oncall | ● | ● | ● | ● | ● | · | · | · | · | ● |
expense-approval | ● | ● | · | · | ● | · | · | · | · | ● |
claim-intake | ● | · | · | · | ● | · | ● | ● | · | ● |
order-fulfilment | · | ● | · | · | ● | · | · | · | ● | · |
pr-reviewer | · | ● | · | · | ● | ● | ● | · | · | · |
support-drafts | ● | ● | · | · | ● | ● | · | · | · | ● |
research-agents | ● | · | · | · | ● | · | ● | · | ● | ● |
A call that cannot be undone, such as a payment, may time out and still have happened. Sending it again could pay, book or page twice. The check refuses such a retry (PL4003) unless the call is sent once, carries an idempotency key, or a person signs off on the risk. Seven of the examples send the call once. When no answer comes back, the program moves to an unknown state. Only a person can move it on, with Resolve or Confirm. The program never sends the call again.
The state diagrams below use the same colors. Each arrow is a step the program allows, labeled with the actions that take it.
A plain state machine · examples/flash-controller/
One block of a flash memory chip. The block is erased, programmed, then verified, with a limit on retries. There is no outside call and no model: the host drives the chip and tells the program what happened.
Key propertyA block is never programmed unless it is erased.
step property erased-before-program: action == Program implies pre.state == Erasedinvariant bad-after-limit: state == Bad implies retries == 2on Program(value) { require state == Erased else reject "not-erased" state' = Programming data' = value}The smallest example. A block that still fails after two retries is marked Bad, and every action on it is refused.
A model answer and a calendar booking · examples/appointment-booker/
A model reads a patient's message and returns a day and an hour, each with a confidence. The program books that slot with one calendar call, which cannot be undone. It refuses a slot that is already taken.
Key propertyNo slot is booked twice.
on Parsed(day, hour, dconf, hconf) { require phase == Parsing else reject "not-parsing" if dconf >= 0.8 && hconf >= 0.8 { if taken[day * 2 + hour] { phase' = Conflict } else { phase' = Booking taken' = taken with [day * 2 + hour] = true emit write(slot: day * 2 + hour) } } else { phase' = Unclear }}step property free-slot-only: (action == Parsed && post.phase == Booking) implies !pre.taken[post.slot]if dconf >= 0.8 && hconf >= 0.8 { if taken[day * 2 + hour] { phase' = Conflict } else { phase' = Booking slot' = day * 2 + hour taken' = taken with [day * 2 + hour] = true emit write(slot: day * 2 + hour) }}Both confidences must reach 0.8: a known day with a guessed hour is not a booking. If the calendar does not answer, the slot stays taken, since the event may exist. Only a person can free it.
A request that always ends · examples/subscription-cancel/
A subscriber asks to cancel. The service may make one offer to keep them. The subscriber keeps the subscription, declines, or says nothing. After a week the offer lapses and the cancellation goes ahead. The cancellation is a billing call, sent once.
Key propertyA request to cancel always ends, and the offer is made at most once.
path property offer-at-most-once: count("retention.offer") <= 1liveness request-ends: status == Offering || status == Offered leads to status == Cancelled || status == Retained || status == Stuck under fair { OfferSent, OfferFailed, Lapse, Billed, BillFailed, Resolve }on Decline { require status == Offered else reject "not-offered" status' = Cancelling status' = Offering cancel lapse emit cancel() emit offer()}One change gives two findings. The decline goes back to an offer, so the request never ends, and the offer is sent a second time.
Timers, and a person when the model is unsure · examples/incident-oncall/
A model rates the severity of a report. If it is sure the severity is High, the program pages the on-call engineer once and starts a five-minute timer. With no acknowledgement, it escalates once. The engineer may snooze twice at most. If the model is unsure, a person rates the report.
Key propertyA page is acknowledged or escalated, assuming the timers fire.
on Snooze { require status == Paged && snoozes < 2 else reject "cannot-snooze" status' = Snoozed snoozes' = snoozes + 1 cancel ack after 15m -> Wake() as wake}liveness page-is-answered: status == Paging leads to status == Acked || status == Escalated || status == Unreached under fair { Timeout, Wake, PageSent, PageFailed, Escalated, EscalateFailed, Confirm }on Snooze { require status == Paged && snoozes < 2 else reject "cannot-snooze" require status == Paged else reject "cannot-snooze" status' = Snoozed snoozes' = snoozes + 1 cancel ack after 15m -> Wake() as wake}The path is a loop: Paged, Snooze, Snoozed, Wake, Paged, again and again. With no limit on snoozes, the escalation never happens, even though every timer fires.
Who may approve, and a person above a threshold · examples/expense-approval/
An employee submits a receipt. A model picks its category. An approver approves or declines it. The payment cannot be undone and is sent once. Above 200 euros, the policy holds it until a person signs off. The approver's identity comes from the host's login, never from the request data.
Key propertyThe approver of a claim is never its submitter.
on Approve by a: Approver { require status == Submitted else reject "not-submitted" require a.principal != submitter else reject "own-claim" approver' = a.principal status' = Paying emit pay(amount: cost)}invariant approver-not-submitter: approver != none implies approver != submitteron Approve by a: Approver { require status == Submitted else reject "not-submitted" require a.principal != submitter else reject "own-claim" approver' = a.principalAmounts are stored in steps of 50 euros (0 to 10). With a wider range, the check takes too long to finish. This limit is listed in the language findings.
Two models and a confidence threshold · examples/claim-intake/
A model sorts an insurance claim into a category. A small model answers first. A larger one takes over when the small one is unsure. A claim goes to its queue on its own only when the confidence is 0.8 or more. Below that, a person decides. A fraud flag makes the assignment wait for a person's approval.
Key propertyA claim is assigned by itself only on a calibrated confidence of at least 0.8.
route classify { tier small provider "small" calibration "maps/classify-small.json" max tokens 20 tier large provider "large" calibration "maps/classify-large.json" max tokens 20 escalate when conf < 0.8 or failed budget monthly}step property confident-or-person: (action == Classified && post.status == Assigning) implies conf >= 0.8// claim-intake-defect.poly: a confidence added to a marginif conf >= 0.8 {if conf + margin >= 1 { // claim-intake-ignored.poly: the branch tests the categoryif conf >= 0.8 {if category == Auto {This example has two defect copies. The first is refused before the check even runs: a confidence can only be compared with a fixed number. The second never looks at the confidence at all.
Undo steps when a later step fails · examples/order-fulfilment/
Reserve the stock, charge the card, ship. If a later step fails, the earlier ones are undone: the stock is released and the charge is refunded. Shipping and refunds are sent once, and an unanswered one goes to a person. The check also runs two orders against one item in stock.
Key propertyA cancelled order holds no stock and no charge, and the stock is never oversold.
invariant cancelled-holds-nothing: st == Cancelled implies held == 0 && !charged configuration two-orders { stock : Stock order[2] : Order { stock: stock } bounds { transit 4 } invariant never-oversold: sum(order[*].held) <= init(stock.onHand)}on ShipFailed { require st == Shipping else reject "not-shipping" st' = Refunding held' = 0 send stock <- Release() emit refund() st' = Cancelled}Without the undo steps, a cancelled order stays charged and keeps its stock. The two-order check still passes: it tests that the stock is never oversold, which is a different property.
An agent's tools under a policy · examples/pr-reviewer/
An agent reviews a pull request with its tools: read the diff, review it, comment, add a label. Each use of a tool is a step of the program. The agent also has a merge tool. The program never asks for it, and the policy denies it. A budget caps the cost of each review and of each month.
Key propertyThe program never merges, and the policy proves no merge is ever allowed.
workflow review runs Review { tool "github.diff" -> gh_diff why "read the pull request's diff" tool "agent.review" -> reviewer why "review the diff" tool "github.comment" -> gh_comment why "post the review as a comment" tool "github.merge" -> gh_merge why "merge the pull request" budget review_spend prices "prices/agent.json" order cap usd 0.05}path property never-merges: count("github.merge") <= 0// policy: never merge-is-never-allowed: allow when effect.kind == "github.merge"phase' = Doneif outcome == Good { phase' = Merging emit merge(pr: number)} else { phase' = Done}Merging is drawn dashed: no step reaches it in the correct program. In the defect copy it can be reached, and the gate still denies the merge when the program runs.
Private notes kept from an outside model · examples/support-drafts/
For one customer, the program reads the customer's messages and the owner's private notes. An outside model summarizes the messages. An in-house model writes a draft and briefs the owner from the notes. Every draft waits for the owner's approval.
Key propertyThe owner's notes never reach the external model.
audience { public < customer < owner }source notes: records { adapter "postgres" audience owner owned freshness 720h } // the policyobligation external-model-audience "The external model is given nothing above the customer audience." rule { when proposal.kind == "effect" && effect.kind == "decision.summary" && !(effect.taint.class in { "public", "customer" }) require false else deny}never notes-to-external-model "Notes never reach the external model.": allow when effect.kind == "decision.summary" && effect.taint.class == "owner"on Noted(items) { require status == Noting else reject "not-noting" status' = Briefing decide brief(notes: items) decide summary(thread: items) // the notes sent to the external model}The check tracks private data into outside calls and messages. What a model call receives is checked by the gate when the program runs (finding 17). In the test, the gate refuses the summary built from the notes.
Three agents checked together · examples/research-agents/
One planner and two workers. The planner picks a focus. Each worker reads documents and answers with citations. All model calls share one budget. The check runs the three agents together, in every order their messages can arrive.
Key propertyEvery worker that reports has cited its sources (699 combined states).
configuration inquiry { planner : Planner worker[2] : Worker { planner: planner } bounds { transit 4 } invariant answers-cite: forall i in worker: worker[i].status is Reported implies worker[i].cited}action Guess(text: Content)on Guess(text) { require status == Researching else reject "not-researching" status' = Reported answer' = text send planner <- Report()} inputs { worker[*].Guess, planner.Wire, … }No single agent has this property: it belongs to the crew. A worker that can guess reports without citing, and the path mixes the steps of all three agents.
The check finds defects in the program: a missing test, a wrong comparison, a loop. It cannot see what happens outside the program. The recorded tests cover that part, and each README says where the check stops.
The language problems found while writing the ten, with workarounds and proposed fixes, are in docs/examples/language-findings.md. The proposals are in docs/proposals/v2.0.md. One problem was a defect of the toolchain and is fixed in v1.4: a policy scope that matches nothing is now reported (PL6504).
The ten examples make one point from ten angles. A property takes a few lines to write. The check tests it on every state the program can reach. A one-line defect is found with the shortest path that shows it: two steps for a missing erase check, a loop of nine steps for a snooze that blocks the escalation, six steps across three agents for a worker that guesses. Calls that cannot be undone are sent once, and an unknown outcome goes to a person, so no example can pay, book or page twice. What lies outside the program (a model's accuracy, a service's promise, a person's identity) is covered by the recorded tests and by the gate. Tests cover the paths that ran. The check covers the paths nobody thought of.
PL3002) and a path.pre.) and after (post.).never rule is also proved by the check.