An agent books a trip: a flight and a hotel, within a budget. A model chooses the steps. Halfway through, the airline cancels the flight and the agent plans again. This article shows what it means for poly to support planning, and the steps to write your own planner.
A plan written by a model is a path nobody wrote down in advance. Tests try the plans someone imagined: book the flight, then the hotel. They cannot try every order the model may choose, every answer a booking service may give, and every moment the airline may cancel. Yet the questions that matter are about all of them. Can the trip end with a hotel and no flight? Can the agent spend more than the budget? Can a cancellation be left unfinished?
In poly, the model plans one step at a time, and the program owns the rules.
The model never calls a service. It proposes, the program decides, and the gate applies the traveller's policy.
Because the model's answer is a value from a fixed list, the check can try every value at every step. It explores every state the trip can reach, whatever the model picks. That is what "supports planning" means: the model plans freely, and the proof covers every plan it could make.
The code below comes from a small program written for this article and checked with poly v1.4: CLEAN, 162 states. Only the parts that matter are shown.
Do not ask the model for a whole plan in free text. Ask it for the next step, as a value of an enum. The answer comes back as an action, with a confidence.
enum Step { BookFlight, BookHotel, Finish } decision next(request: Content) -> Step { provider "small" labels { egress:external, read:private } timeout 2s ok(r) -> Chose(step: r.answer, conf: r.conf) failed -> Unsure()}Each step has conditions: no hotel before a flight, one hotel at a time, enough budget left, a confident answer. A step that breaks a rule goes to the traveller, not to a service. The hotel branch is shown; the flight branch has the same shape.
on Chose(step, conf) { require phase == Asking else reject "not-asking" if conf >= 0.8 && step == BookHotel && flight == Held && hotel == None && spent <= 3 { hotel' = Booking spent' = spent + 2 phase' = Planning emit bookHotel() } else { phase' = AskTraveller // unsure, or a step the rules do not allow now }}Record what the world holds: each booking and what has been spent. Keep the ranges small. Money in units of 100 dollars, from 0 to 8, is enough to prove the budget rule, and the check stays fast.
enum Slot { None, Booking, Held, Unknown, Cancelling } state { phase : Phase = Planning flight : Slot = None hotel : Slot = None spent : 0..8 = 0 // units of 100 dollars}A non-refundable flight cannot be undone. If the call times out, the seat may be booked, so a retry could buy a second ticket: send it once. A hotel that honors an idempotency key can be retried safely, and it can be cancelled. The check refuses an irreversible call that may be sent twice (PL4003).
effect bookFlight() { kind "airline.book" labels { egress:external } targets { egress: "https://airline.example/v1/bookings" } class irreversible retry { attempts 1, base 200ms, timeout 10s } ok -> FlightBooked() failed -> FlightRefused() exhausted -> FlightUnknown()} effect bookHotel() { kind "hotel.book" labels { egress:external } targets { egress: "https://hotels.example/v1/reservations" } class compensable idempotent header "Idempotency-Key" window 24h ok -> HotelBooked() failed -> HotelRefused()}When the one attempt gets no answer, the program does not guess. The booking moves to Unknown, and a person looks it up.
on FlightUnknown { require flight == Booking else reject "not-booking" flight' = Unknown // the seat may be bought: nothing is sent again} on Resolve(booked) { require flight == Unknown else reject "not-unknown" if booked { flight' = Held } else { flight' = None spent' = spent - 3 // not bought: the budget comes back }}This step makes planning safe. When the airline cancels, the old plan leaves a hotel for the wrong dates. The program cancels it and gives the budget back, then the model plans again. A hotel booking still in progress when the flight is cancelled is cancelled when it arrives.
The life of one booking. The red arrow is the re-plan: the program, not the model, moves a held booking to Cancelling.
on FlightCancelled { require flight == Held else reject "no-flight" flight' = None spent' = spent - 3 // the airline refunds the ticket if hotel == Held { hotel' = Cancelling emit cancelHotel() } phase' = Planning} on HotelBooked { require hotel == Booking else reject "not-booking" if flight == Held { hotel' = Held } else { hotel' = Cancelling // the flight was cancelled while the hotel was booking emit cancelHotel() }}Write down what must always be true and what must eventually happen. The check proves both over every plan. A policy can add what needs the traveller's approval, such as a booking above a price; the gate applies it when the program runs.
invariant no-hotel-without-flight: hotel == Held implies flight == Heldinvariant within-budget: spent <= 5liveness cancels-finish: hotel == Cancelling leads to hotel == None || hotel == Unknown under fair { HotelCancelled, CancelFailed }The first version of this program looked right. The check found four defects in it, each with the shortest path that shows it.
| Property broken | Path | What happened | Fix |
|---|---|---|---|
no-hotel-without-flight | 7 steps | The airline cancels while the hotel booking is in progress. The hotel is confirmed after the flight is gone. | The hotel's answer checks the flight (step 6). |
within-budget | 6 steps | A flight with no answer turns out not to be bought, but its cost stays in the budget. The next flight goes over. | Resolve gives the budget back (step 5). |
within-budget | 6 steps | The airline cancels, its cost is not given back, and the budget rule allowed 3 + 3 against a limit of 5. | The cancellation gives the budget back; the rule allows a flight only with 2 or less spent. |
cancels-finish | loop of 10 | The model says Finish while a hotel cancellation is still pending. The trip ends and the cancellation is never confirmed. | Finish is allowed only when no booking or cancellation is in progress. |
The first path is a race between two services, the kind of path tests rarely reach:
Plan → Chose(BookFlight) → Plan → FlightBooked → Chose(BookHotel) → FlightCancelled → HotelBooked
After the fixes the check is CLEAN. A coding agent can follow the same loop: each finding is a code and a path it can repair against.
An agent that plans is a goal-oriented system: it chooses its own steps, along paths nobody wrote down. poly does not limit the model's choices. It limits what a choice can do. The model picks the next step from a fixed list. The program checks the rules, makes the calls, and undoes what an old plan left behind. Because every choice is a value the check can try, the proof covers every plan the model could make, including the re-plan after a cancelled flight. Our own sketch had four defects that looked right on reading; the check found all four. Write your planner in seven steps, and let the check find the paths you did not think of.