poly · v1.4

Poly: a programming language for AI-augmented applications

Poly is a language for the stateful core of agent-written software.

A human-readable programming language for frontier models. The model writes it, a checker explores every state it can reach, and the runtime executes the machines that were checked.

Understanding Poly →Poly on GitHub ↗

Understanding Poly, a nine-minute explainer. Download the video.

Seven capabilities: one path and one loop

poly gives a program seven capabilities. Six are on the path from the model's proposal to the record of what happened: planning, checking, admission, governance, safe action and audit. The seventh, learning, closes the loop: what the journal records comes back as a better program, checked and admitted again before it runs.

LearningPast runs feed back into the program. Rules are mined from the journal and a model's calibration is refitted. A person approves each change, and the check runs again before it is used.before it runs

One step of the program, from the model's proposal to the journal, and the loop from past runs back to the program.before it runs the check, over every path while it runs the gate and the runtime

The constructs behind them

Each capability comes from one construct of the language. The code comes from programs checked CLEAN (the v1.4 examples and the travel planner), with some lines left out. The journal commands show the shape of the CLI; the replay line is from the appointment-booker test, and the promotion line from the inbox test.

Planning

construct: decision

A typed question put to a model. The answer must be one value of the declared type, and it comes back as an action with a confidence the program compares with a fixed number.

decision next(request: Content) -> Step {  provider "small"  timeout 2s  ok(r) -> Chose(step: r.answer, conf: r.conf)  failed -> Unsure()}

Checking

construct: machine

State, actions, the conditions each action must meet, and the properties that must hold. Several machines checked together form a configuration.

on Chose(step, conf) {  require phase == Asking else reject "not-asking"  ...}invariant within-budget: spent <= 5liveness cancels-finish:  hotel == Cancelling leads to hotel == None || hotel == Unknown  under fair { HotelCancelled, CancelFailed }

Repair

Every finding comes with a witness, the shortest path that breaks the property. poly witness --test turns it into a failing test, and poly fix applies a suggested fix. poly mcp and poly lsp give all of this to a coding agent, so it can check and repair its own code.

$ poly witness w3 --test --out test/free-slot.test.mjs$ poly fix w3$ poly mcp            # the same commands as tools for a coding agent

Admission

construct: poly admit

Admission signs a certificate that binds the checked program, its policy and its model maps by digest. The runtime starts only an admitted build. Translation validation, part of every check, compares the generated JavaScript with the checked program over every state, so what runs is what was checked.

$ poly check .verdict: CLEAN (exit 0)$ poly admit .$ poly sign policy drafts --by owner --key owner.key

Governance

construct: policy

Obligations allow, deny or escalate each proposed call. A never statement is also proved by the check. A person signs the policy, and the gate applies it to every call.

obligation large-payment-reviewed "A payment above 200 is made only after a person approves it." rule {  when proposal.kind == "effect" && effect.kind == "payroll.pay" && machine("expenses.Expense").large  require false else escalate  on unknown escalate}never merge-is-never-allowed "No merge is ever allowed.": allow when effect.kind == "github.merge"

Data boundaries

An audience labels who may see a piece of data. The check follows data into calls and messages, and a policy rule can refuse a call whose data is above the audience it allows. poly forget erases a person's data: exports of the journal then leave those steps out and count them.

audience { public < customer < owner }source notes: records { adapter "postgres" audience owner owned freshness 720h } $ poly forget --subject customer-42 --by owner --key owner.key

Cost limits

A budget caps what model calls may cost, per run and per month. A call that would go over is refused, and poly cost reports what was spent.

budget review_spend {  cap usd 0.25 per run  cap usd 0.45 per month}

Safe action

construct: effect

A call to the outside world, with its class (none, reversible, compensable, irreversible) and its retry. An irreversible call that may be sent twice is refused by the check (PL4003).

effect bookFlight() {  kind "airline.book"  class irreversible  retry { attempts 1, base 200ms, timeout 10s }  ok -> FlightBooked()  failed -> FlightRefused()  exhausted -> FlightUnknown()}

Audit

construct: journal

The runtime records every step, every model answer and every gate decision. The journal can be verified against the signer's key and replayed against the admitted build.

$ poly journal verify --db trip.db --trust owner=owner.pub$ poly journal replay --db trip.db --build .poly/build \    --certificate admission.json --trust owner=owner.pubreplay: 3 runs, 16 rows; 1 gate sessions; divergences: 0

Learning

construct: poly mine, poly promote, poly journal fit

poly mine reads past runs and proposes rules. A person rules each one real or spurious. poly promote inserts a real rule into the policy or the machine and runs the check again; a rule that would conflict with an obligation is refused (PL6501). poly journal fit refits a model's calibration map from recorded outcomes, and a tier that calls a new model needs a map fitted for it (PL6842).

$ poly mine --traces runs.jsonl --project . --polyx ../polyx --out candidates.json$ poly promote . --candidates candidates.json --adjudication verdict.jsonpromoted rb9f1ea42062b7c8a into src/inbox.policy.poly (promotions/0001-rb9f1ea42062b7c8a.json)$ poly journal fit --db inbox.db --decision triage --model small --out maps/triage.json

One text, read three ways

A poly program is a set of declared state machines. The same source is the model that is checked, the policy that gates every call, and the code that runs.

The model

The checker explores every reachable state over declared finite domains and returns a witness for each violation.

The policy

Every call the program can make crosses a gate that allows, denies or escalates it, against the state that made it.

The code

The runtime executes the same text durably and writes a hash-chained journal that replays exactly.

machine Gate {  state { mode : Mode = Locked,  coins : 0..3 = 0 }  on Coin { require coins < 3 else reject "coin-box-full";  coins' = coins + 1;  mode' = Unlocked }  on Push { require mode is Unlocked else reject "locked";  mode' = Locked }}

$ poly check hello.poly
PL3201 DEADLOCK  Gate   no action is accepted in a reachable non-terminal state
  witness (4 steps): Coin, Coin, Coin, Push  → Locked/3, then Coin: coin-box-full, Push: locked
verdict: FINDINGS (exit 1)

A turnstile whose full coin box locks it forever. No one wrote a deadlock property; the checker found it. Condensed from Understanding Poly.

Promises and enforcement

Capability	Construct	The promise	Enforced by
Planning	`decision`	The model chooses the next step; the type fixes what it can choose.	The check covers every answer at every confidence. The runtime calls the model.
Checking	`machine`	Every state the program can reach is checked against its properties. Each finding comes with a path, a test and a fix.	The check, before the program runs. `poly witness` and `poly fix` for repair.
Admission	`poly admit`	Only the checked program runs, bound by a signed certificate.	The runtime refuses a build that was not admitted. Translation validation compares the generated code with the checked program.
Governance	`policy`, `audience`, `budget`	Rules a person signs: allow, deny, or ask a person. Data stays within the audience a rule allows. Model spend stays within its budget.	The gate, at every call while the program runs. A `never` statement is also proved by the check.
Safe action	`effect`	Every outside call declares whether it can be undone and how it may be retried. Nothing is paid twice.	The check refuses an unsafe retry (`PL4003`). The runtime sends each call as declared.
Audit	`journal`	Every run can be verified and replayed, with every gate decision.	The runtime records it; `poly journal verify` and `replay` read it.
Learning	`poly mine`, `promote`, `journal fit`	Past runs improve the program. Nothing learned is used until it is checked and admitted.	A person rules on each mined rule. The check runs again on each promotion. Admission binds a new model to its refitted map.

Conclusion

Six capabilities follow one step through a program. The model plans it. The program's rules accept it, and a finding comes with the path to fix it. Admission makes sure the program that runs is the one that was checked. The signed policy allows the step, keeps data within its audience and spending within its budget. The call is made the way it was declared, and the journal records it. The seventh closes the loop: past runs come back as mined rules and refitted models, approved by a person, checked and admitted again. A test can show that one path works. These seven together show that no path breaks the rules, keep the record of what happened, and let the program improve without losing either.

Glossary

Check: poly check: tries every state the program can reach and reports each broken property with a code and a path.
Gate: The part of the runtime that applies the policy to every call before it is made.
Decision: A typed question put to a model, answered with a value and a confidence.
Machine: A program's state, its actions and their conditions, and its properties.
Policy: Signed rules: obligations that allow, deny or escalate, and never statements.
Effect: A call to the outside world, declared with whether it can be undone and how it may be retried.
Journal: The runtime's record of every step, model answer and gate decision.
Witness: The shortest sequence of steps that breaks a property, reported with each finding.
Promotion: Inserting a mined rule, ruled real by a person, into the program or its policy, followed by a new check.
Calibration map: A table that turns a model's raw confidence into a calibrated one, fitted from recorded outcomes.
Admission: Signing a certificate that binds a checked program, its policy and its model maps, so the runtime runs only that build.
Translation validation: Comparing the generated JavaScript with the checked program over every state.
Audience: A label for who may see a piece of data, such as customer or owner.
Budget: A cap on what model calls may cost, per run or per month.
Replay: Running a journal again against the admitted build and comparing every result.