Coding agents after the code: a poly workbench

Today's coding agent workflow

Working with a coding agent such as Claude Code means managing a long list of settings and steps. You write instructions in a CLAUDE.md, answer permission prompts, set hooks, watch the context window, split work across sessions and worktrees, and then read the diff. Each of these exists for a good reason: the agent writes code that only a person can vouch for, so the person must stay close to every step.

The bottleneck has moved from writing to reviewing. Spotify reports that its developers now have 76% more pull requests to review. A reviewer reads one change at a time and can follow a few paths through it. The defects that matter (a refund sent twice, a page never answered, private notes sent to the wrong model) live in the paths between the lines.

The shift: from reading code to approving behaviour

poly changes what people look at. The agent still writes the program, but the program is a set of state machines that a check explores completely, over declared domains. People no longer need to read every line. They state what must be true, sign the rules the program must follow, and approve the change in behaviour the check reports.

The person who gains most never opens the workbench: the guest who asks for a refund. A refund is never sent twice, a large one never goes out without a person, and an approval that is needed arrives in minutes because it lands in one queue with its reason attached.

This is already measured, not only imagined. On τ²-bench, the airline and retail benchmark for customer-service agents, a gate built this way (the written policy translated into poly, checked over every path, and applied to every action the agent proposes) removed nearly all policy breaches without lowering task success. In two preregistered studies, actions breaking the policy fell from 178 to 0 in retail and from 31 to 1 in airline (the paper).

This is not the compiler story. A compiler translates a complete source into an equivalent program. Here people write a contract that is deliberately incomplete: properties, rules and boundaries. The agent writes an implementation that satisfies it, and makes its own choices wherever the contract is silent. So the code is an implementation of a contract, and three things cover what the contract does not say: people review every new path the build adds, contracts on each action catch errors where they happen, and recorded tests cover the code at the edges.

It is no silver bullet either. Brooks split the difficulty of software into what is essential (deciding what the software must do) and what is accidental (the tools and plumbing around that decision). The workbench removes accidental difficulty: prompts, permissions, context windows, diffs to read. The essential part stays, and moves: it becomes the work of writing properties that say the right thing.

Roles and their responsibilities

A poly project gives each role a part of the program it writes, and a part it signs.

Seven roles do not mean seven people. On a small team one person holds several, and the team that owns a machine also owns what it sends to a person: its escalations, its unknown outcomes, its pager. Operations is a duty of the owning team, not a separate team the work is handed to. Signatures follow risk: a change that only adds a reversible path needs the owner; a change that touches an irreversible call or the policy needs security too.

Many signers must not mean many designers. Each project has one owner with the final word when a property and a boundary pull apart, so the design stays one coherent idea. Brooks's surgical team fits the workbench well: one person decides and answers for the result, and the agent is the support team that writes, checks and repairs around that person.

The flow of work

One column per role. Purple columns are people, blue columns are poly itself, grey is the coding agent. Dashed arrows return work to an earlier step.

Work starts from intent, not from a ticket that describes code. The product manager and the architect state what must hold and what the program may touch. The agent writes machines until the check is CLEAN, or returns findings, each with the shortest path that breaks a property. A developer and the agent repair them. People with the right keys sign the policy and admit the build. The runtime runs only that build, sends every call through the gate, and records every step. Operations handles what the program sends to a person. The journal feeds learning, and learning comes back as proposals to the people who own the properties.

The flow is a spiral: each turn runs from intent to the check, review, admission, production and learning, and then starts again. Three of Boehm's anchor points mark where a project stands on it. The objectives are agreed when the owners confirm the properties. The architecture is settled when the boundaries and the policy are signed. The first operational capability is reached when an admitted build serves its first share of real runs.

The command line of the workbench

The screens below are imagined. Each one is built on commands poly already has; the table after them names which. "A working prototype" shows the same steps on screen.

The project at a glance

$ poly
refunds-desk · build 1.7 admitted · signed by owner, security · running
  machines   Desk, Ledger, Conversation              CLEAN  5,762 states
  policy     refunds (12 rules, 2 never)              signed by owner
  live       318 runs today · 4 waiting for a person · 1 unknown outcome
  learning   3 candidate rules · triage model drifting (agreement 0.71 → 0.64)

  levels     gate 40 ms at p99 ok · escalation wait 6 min median ok · false refusals 2.1% (target 3%) ok
  cost       models $3.12 today · last check 41 s (cached) · agent jobs 7

next  poly ops · poly learn · poly intent "…"

Intent in, behaviour out

$ poly intent "A refund above 100 dollars waits for a person"
agent   reading the program and its policy …
proposal (3 changes)
  property  refund-large-needs-person    Desk, step property
  policy    large-refund-reviewed        escalate when amount > 100
  machine   Desk: new state Held, action Resolve by an approver
check   CLEAN
read back  "Whenever a refund over 100.00 is issued, a person approved it
            earlier in the same request."
allowed    request 240.00 → Held → approved by raj → Issued
forbidden  request 240.00 → Issued                     cannot happen
owners  property → product (ana) · policy → security (raj)

Is this what you meant?  [y]es  [n]o, refine  [e]dit

The product manager never sees a line of the machine. She sees her sentence read back in plain words, one path the program allows and one it can no longer take, and who else must sign. Her "yes" is part of the record. This is the validation step: the check verifies the program against the property, and her confirmation validates the property against what she meant. Without it, "proved" would only certify the agent's reading of her sentence.

A review of behaviour, not of lines

$ poly review 42
behaviour change  build 1.7 → 1.8
  paths added      Asking → Held → Issued           a person approves        example ▸
                   Asking → Held → Released         after 48h, refund cancelled  example ▸
  paths removed    Asking → Issued, amount > 100    no longer possible        example ▸
  effects changed  none · stripe.refund still irreversible, sent once
  + property  refund-large-needs-person      proved · confirmed by ana
  = property  no-reissue                     still proved
  + rule      large-refund-reviewed          needs a signature: security

[w]alk a path  [s]ign  [c]omment

A behaviour change has a precise meaning: the difference between the paths the old build can take and the paths the new build can take. The review lists the paths added, the paths removed and the paths whose effects changed, each with one example run a person can walk. State counts say nothing to a reviewer and are left out. A diff of lines is still there for anyone who asks for it.

A finding, step by step

$ poly why page-is-answered
PL3301 the page is never answered: a loop of 9 steps
   1  Report("db down")       Reported  → Triaging
   2  Triaged(High, 0.93)     Triaging  → Paging      sends pager.page
   …
 ↺ 7  Snooze                  Paged     → Snoozed
 ↺ 8  Wake                    Snoozed   → Paged
agent's fix  limit snoozes to 2 (2 lines)    check with it: CLEAN

[a]pply  [t]est  e[x]plain

The solution in production

$ poly ops
waiting for a person (4)
  #811  refund 240.00   guest-17   rule large-refund-reviewed     [a]pprove [d]eny
  #812  refund 130.00   guest-04   rule large-refund-reviewed     [a]pprove [d]eny
unknown outcomes (1)
  #799  stripe.refund   no answer after one attempt
        look it up in Stripe, then:  [i]ssued  [n]ot issued
journal  verified · replay of yesterday's runs: 0 divergences

Lessons from production

$ poly learn
from 2,140 runs (journal verified, private values replaced by digests)
  candidate r-7c1  refunds from 100 to 150 for a returning guest
                   were approved 97 times out of 97
     proposed rule   no escalation when amount <= 150 and the guest is returning
     check with it   CLEAN · narrows large-refund-reviewed
     needs           product and security          [r]eal [s]purious [l]ater
  drift   triage: the small model agrees with people less often (0.71 → 0.64)
     [f]it a new map from people's verdicts · admission required

The running solution teaches its designers. Patterns in what people approve become candidate rules. A model that drifts gets a new calibration map. Nothing learned reaches production until a person rules on it, the check runs again, and the build is admitted.

Learning has one trap. Once a rule stops sending these refunds to a person, nobody sees them any more, and the data that justified the rule stops coming in. So an automated rule keeps a small random sample of its cases going to a person, and the workbench compares their verdicts with the rule. When they disagree, the rule goes back to its owners.

Commands available today

The shared workbench

A command line suits one person. A release is decided by several. The workbench therefore also opens as a shared, live document, one per project: everyone with the link sees the same page, edits arrive as they are made, and comments sit beside the block they are about. Each tab is a live view of the project, not a copy: a property block shows whether it is proved, a finding block can be walked step by step, and a signature block holds the button that signs.

A mockup. People write and sign; @poly asks the agent from inside the document, and its answer arrives as a block already checked.

Checks take time. A change that touches one machine is checked in seconds from cached results; a change to a large configuration can take minutes. The workbench shows a block as "checking" while the check runs, never as proved before it is, and states its time budget for an answer in a conversation. A question that needs a long check is answered with "checking, results in about N minutes", and the block updates when the check finishes.

The tabs follow the flow of work. Intent holds sentences and the properties they became. Behaviour is the review of what a build can do. Policy holds the rules and their signatures. Operations lists what the running solution sends to a person. Learning holds candidate rules and drifting models, each with the people who must rule on it. A comment can be answered by a person or by the agent; a question that changes the program comes back as a proposal, never as an edit.

A working prototype

The screens above are designs. A first prototype of the shared workbench runs the same steps without a terminal. Each person gets a card when a decision is theirs, answers it on screen, and the agent and the check do the rest.

In the run shown here, a small team changed the refunds desk from build 1.7 to build 1.8: Ana (product), Raj (security), Ben (developer) and JJ (release lead). The agent ran on a real model, and poly v1.5.0 checked every proposal. Each image is the card one person received, cropped from the full screen. The Operations and Learning tabs read a short recorded run prepared for the demo.

The release waits for three people: Ana's confirmation of the read-back, Raj's signature and JJ's admission. Each has a date, and a missing one puts the release at risk before its date, not after.

This prototype is the one to throw away. Brooks warned that a team will build one anyway, and that the second system tends to carry every idea the first one left out. The smallest workbench worth building is three things: the read-back of a property, the behaviour review of a build, and one queue for what the program sends to a person. Everything else on these pages comes after those prove their value.

Under the hood

The workbench does not need its own model. The coding tasks (drafting a machine from a sentence, writing a handler, proposing a fix for a finding, explaining a path in plain words) go to Claude Code in headless mode, claude -p. On one developer's machine it runs under that developer's own login, as poly new does today. In a shared workbench it runs under a service identity that belongs to the project, and every job records who asked for it, so the journal says "proposed by the agent, at Ana's request". The team checks that its plan's terms allow this kind of automated use on its behalf.

• The agent gets tools, not the file system. Each job runs with poly's MCP server as its only tools (edit-check, witness, fix), so every change it proposes is parsed and checked before anyone sees it.
• Jobs are small and bounded. One job per ask, with a limit on turns and a structured result, so the workbench shows a proposal and its verdict, not a transcript.
• No model on the decision path. The check, the signatures, admission and the gate are poly's own code. The agent proposes; people and the check decide.

This is where the intricacies of today's agents go. The prompt, the context, the permissions and the session are the workbench's business. People see a sentence, a proposal, a verdict and a button.

Running it in production

Imagined, like the screens above. The runtime, the gate, the journal and its replay exist today; the rollout steps do not.

A build that is proved correct still has to reach production safely, keep running when parts of the system fail, and stay affordable. The check answers none of these. The workbench has to.

From admission to production

Admission makes a build eligible to run; it does not switch traffic. Every run records the certificate it started under, so a run never changes build halfway: runs in flight finish on 1.7 while new runs start on 1.8. Before any new run starts on 1.8, the journal's recent runs are replayed against it, and any divergence the behaviour review did not announce stops the rollout. Then a small share of new runs moves to 1.8, while the team watches its service levels. Rolling back means sending new runs to the previous certificate, which is still signed and still loadable.

From admission to production. At each step a divergence or a broken service level sends new runs back to the previous certificate.

When the workbench itself fails

The gate sits on every call, so it has a latency budget like any other service. Its decisions are local and need no model, which keeps them fast. Loading a large build is the slow part: a bridge loads it once when it starts, not on each call, and the overview screen reports both.

Service levels

The metrics of the previous section become targets the owning team runs to: the gate's latency, how long an escalation waits for a person, and the false-refusal rate. The last one matters most. A gate that refuses too much is safe and useless, and only a target makes that visible before customers feel it. Cost sits beside them on the same screen: model spend, check time and agent jobs, per day and per run.

Contracts and the edges of the proof

Properties speak about a whole run. People also need statements they can read one action at a time, and that say where an error happened. Each action carries a contract: what must be true before it runs, and what it guarantees after.

action Approve(by: Person, amount: Money)  require state == Held and by != requester  ensure  state == Issuing and approvedBy == by

An illustration: poly has require today; ensure and this action form are proposed.

The check proves the machine contracts on every path. The host handlers sit outside the check, so their contracts are checked at runtime, on every call: a handler that breaks its contract stops the step and records which side was at fault. This is where the proof meets the code people still write by hand.

The same edge exists for data. The check explores declared, finite domains; real amounts, names and dates are not finite. Each project therefore states its mapping from real values to checked values, for example an amount as "100 or less" or "over 100". The mapping is code, and it is tested at the boundary values (100.00 and 100.01) with recorded tests. A proof is only as good as this mapping, so the mapping has an owner too.

Lessons from software and manufacturing

None of this starts from zero. Software delivery and factories have learned, over decades, how to let many people and machines work fast without losing control. Each lesson below has a direct place in the workbench.

Toyota did not make its workers faster. It made a defect stop the line. Coding agents need that more than they need speed.

The cost of a defect

Boehm showed that a defect costs more to fix the later it is found. A wrong rule caught when the owner reads a property back costs a minute. The same rule caught by the check costs a short repair. Found in production, it costs a refund paid twice, an audit, and a customer's trust. This is the economic case for the workbench: it moves the discovery of whole classes of defects to the left of the chart, before anything runs.

Delivery metrics for agents

DORA's four metrics (deployment frequency, lead time for changes, change failure rate, time to restore service) measure a delivery pipeline. They still apply to software an agent writes. An agent that acts on its own also needs measures of its behaviour while it runs:

The last two pull in opposite directions. A gate that refuses everything has no breaches and a useless agent. The workbench reports both, side by side, for every build.

The hard parts

Boehm's advice is to let the largest risks decide where the effort goes. Ranked by our own estimate of how likely each is and how much it would cost:

• The check proves what you wrote. A property that misses the point is proved all the same. The read-back and the example paths reduce this risk; they do not remove it. Writing good properties becomes the core skill, for property owners as much as for engineers.
• The edges stay outside the proof. Host handlers, the mapping from real data, the accuracy of a model, and whether a service keeps its promises are assumptions, listed in the certificate. Runtime contracts, recorded tests and the gate cover them, not the check.
• State spaces grow. Checks run over declared, finite domains. A large crew of agents can make a search too large to finish, and the check then says INCONCLUSIVE rather than CLEAN. Even when it finishes, a cold check can take tens of minutes, which shapes how people work.
• Keys are the new root of trust. Admission and policy signatures are only as good as the keys behind them: who holds each key, how it rotates, and what happens when the agent's service identity is compromised (it can propose, never sign) must be decided before the first build is admitted.
• More agents are not always faster. Brooks's law says adding people to a late project makes it later, because every new person adds paths of communication. Agents add proposals to review in the same way. The workbench limits each agent to one bounded job and one machine where it can, and treats the number of open proposals as a cost.
• Adoption has a price. A team pays to learn poly, to write its first properties, and for the compute of every check. The return comes from defects found early and from reviews that read behaviour instead of lines. A first project should be small enough to measure both.
• Signatures need owners. A workflow of keys and approvals only helps if each property and rule has a person who answers for it.

Conclusion

Coding agents will not stay tools that people supervise line by line. When the program an agent writes can be checked as a whole, people stop reading code and start approving behaviour. They write outcomes as properties, draw the boundaries, sign the rules and admit the builds; the agent writes the machines, and the check covers every path. The intricacies we manage today (prompts, permissions, context windows, diffs) move into the tool. The first evidence is encouraging: on τ²-bench, a checked gate removed nearly all policy breaches with no measurable cost in task success. None of this is a silver bullet, and none of it is new in spirit: it is Toyota's stopped line and Amazon's "you build it, you run it", applied to software that acts. What remains for people is the part that was always theirs: deciding what the software must do, and answering for it.

poly is open source: github.com/cognitive-fab/poly.

Glossary

Property

A statement that must hold on every path: in every state (invariant), at every step, over a whole run, or eventually (liveness).

Check

The exploration of every state a program can reach, over declared domains, against its properties.

Finding

A broken property, reported with a code and the shortest path that breaks it.

Policy

Signed rules the gate applies to every call: allow, deny, or send to a person.

Admission

Signing a certificate that binds a checked build, so the runtime runs only that build.

Behaviour change

The difference between the paths an old build and a new build can take: paths added, paths removed, and paths whose effects changed.

Contract

What an action requires before it runs and ensures after; checked by the check in machines, and at runtime in host handlers.

Read-back

A property stated again in plain words, with one allowed and one forbidden example path, for its owner to confirm.

Property owner

The person who answers for a property: writes it with the product manager and signs it.

Data mapping

The code that turns real values into the finite values the check explores, tested at its boundaries.

Human sample

The share of cases an automated rule still sends to a person, so the rule can be compared with people's verdicts.

Service identity

The project's own account for running agent jobs, recording who asked for each job.

Escalation

A call the policy sends to a person for approval before it is made.

Unknown outcome

A call that cannot be undone and got no answer. A person looks it up and settles it.

Candidate rule

A rule mined from past runs, proposed for a person to rule real or spurious.

Calibration map

A table that turns a model's raw confidence into a calibrated one, refitted when the model drifts.

claude -p

Claude Code run without its interactive interface: it takes a prompt, works with the tools it is given, and returns a result.

Essential difficulty

In Brooks's terms, the part of software work that comes from deciding what to build, as opposed to the accidental difficulty of tools and notation.

Conceptual integrity

A design that reads as one coherent idea, usually because one person or a very small group holds it.

Anchor point

One of Boehm's milestones: objectives agreed, architecture settled, first operational capability reached.

Risk exposure

How likely a risk is, combined with what it would cost; used to rank risks and spend effort where it matters most.

Canary

A small share of new runs sent to a new build first, to watch it before all runs move.

Rollback

Sending new runs back to the previous certificate, which stays signed and loadable.

Service level

A target the owning team runs to, such as the gate's latency or the false-refusal rate.

Jidoka

Toyota's practice of stopping the line as soon as a defect appears, so it is fixed at its source.

Andon

The cord or button any Toyota worker can pull to call for help and stop the line.

Poka-yoke

A design that makes a mistake impossible, or visible at once.

Kaizen

Continuous improvement in small steps, proposed by the people who do the work.

DORA metrics

Four delivery measures from the DevOps Research and Assessment group: deployment frequency, lead time for changes, change failure rate, time to restore service.

pass^k

The share of tasks an agent completes in every one of k attempts: a measure of consistency.

Journal

The runtime's record of every step, model answer and gate decision, verified and replayed.

Sources: F. Brooks, The Mythical Man-Month (1975) and "No Silver Bullet" (1986); B. Boehm, Software Engineering Economics (1981); W. Royce, "Managing the Development of Large Software Systems" (1970); B. Boehm, "A Spiral Model of Software Development and Enhancement" (1986); W. Vogels, interview in ACM Queue (2006); the DORA research program; Spotify Engineering, Coding is no longer the constraint (June 2026); J.-J. Dubray, Enforcing written policies on AI agents with a checked gate: evidence from τ²-bench (2026).