The authoring grammar — every accepted form

In the default --author auto mode, a plain scalar UI step is natural-language model intent:

- Enter 24 Market Street in the shipping address field

record grounds that intent against the live scene. To opt one step into the deterministic grammar instead, mark it explicitly:

- rules: Type Ada into the "Full name" field
- rules: Press the "Save" button

--author rules remains the global opt-in when a whole flow already uses the deterministic grammar; --author llm forces model authoring for plain UI steps. Structured forms such as assert:, assert_api:, repeat: and when: retain their own semantics in every mode.

If auto mode has no configured authoring model, recording says so visibly and falls back to deterministic rules for plain steps. It never silently reinterprets model intent. Human output identifies each step's route as rules, llm, reused, or fallback, and structured/JSON output carries the same per-step routing information for tooling; consumers should use the structured output rather than scraping the display text.

This page is the complete rules grammar. The forms below are the text accepted inside rules: <text> (or as plain steps under global --author rules). They require no model call and are covered by tests that parse the exact examples shown (documented_grammar_examples_all_resolve in crates/flowproof-agent/src/rules.rs — if the doc and the code drift, CI fails).

Model authoring does not make replay probabilistic. The driver gives the model a finite list of provenance-neutral scene tokens and accepts only actions grounded to those listed tokens; the resulting selectors and actions are persisted in the trace. Replay executes that trace directly, with zero model calls.

On the web, that inventory also represents readable values whose identity is relational rather than global. A value cell in a div-based row may have no unique id or class of its own, but still be stable as “the value beside order id”. Flowproof exposes it to the model as one opaque scoped: token containing a container, neighbouring text anchor, and inner selector. The model must copy that token exactly; the token itself is not persisted. Recording translates it to the same deterministic scoped target used by explicit rules, so replay finds the newly rendered row by its anchor and reads the current value.

The inventory covers the rendered page, not just the current viewport, because users naturally refer to a control that starts below the fold. It also gives the model grounded identities for table-row collections, final table cells, drag sources and destinations, small styled or identified visual targets, and readable/actionable elements inside visible same-origin frames. Frame and scoped tokens are authoring-only handles: Flowproof translates them to ordinary deterministic targets before writing the trace.

A plain step is a unit of intent, not a unit of work. Fill out all the vehicle data and click next is one step, and the model answers it with the whole sequence of grounded actions it takes — one per field, plus the button — in a single call. Every action in that sequence is grounded against the same listed inventory and rejected as a whole if any one of them is not, so a half-filled form never reaches the trace. A rejected sequence is put back to the model as a correction rather than as a fresh question: the reply names which action failed and how many before it were already grounded, and asks for the corrected sequence. Re-authoring a dozen actions from scratch to fix one of them is a throw the model has to win twice, and a step naming a whole form is exactly where losing it costs the most. The inventory also reports what each field currently holds, which the page marks required, which boxes are ticked, and a dropdown's exact options, so a <select> is given a name it really has rather than a plausible guess. Values of password fields are never reported.

Plain language is not limited to midpoint clicks and typing. The structured model response can directly express clicking a point within a control, dragging, remembering a count or value, choosing one or several select options, scrolling a container to an exact offset, typing inside a frame, and pressing a key. These are capabilities of the authoring protocol, not syntax authors must learn. Write the user intent—for example, Select Functional, End2End, GUI, and Exploratory testing together—and keep rules: for the comparatively rare case where exact deterministic grammar is deliberately wanted in the source spec.

Conventions: forms are case-insensitive in their keywords. <text> is literal text (may carry ${VAR} secret references). A quoted "<label>" is a text anchor — matched against visible text, accessible label (aria-label), placeholder, an associated <label> (both <label>Name: <input/></label> wrapping and <label for>/id pairing), or, for <input type="submit|button|reset">, the value attribute (the accessible name of a void button-type input, so Press the "Login" button finds <input type="submit" value="Login">). Matching is exact first, then prefix ("Name" finds the field labelled Name:), then ASCII case-insensitive as a last resort ("Close Account" still finds the button reading Close account) — a case-sensitive match always wins. page shows reads visible text plus the accessible names of visible elements, so icon-only buttons that exist purely as an aria-label count. Assertion TEXT matches the same way selectors do: exact first, then case-insensitive (page shows Close Account passes against a page reading Close account), and the negative forms mirror it — if shows X would pass, does not show X fails. Two escape hatches work inside any quoted label: "css:<selector>" (web) and "id:<native id>" (DOM id, UIA AutomationId, SAP scripting id). [2nd ] marks an optional 1-based ordinal (2nd, 3rd, 10th) for when several elements match.

Steps are only half the spec. Starting state that a flow should not rebuild through the UI (an authenticated session, a pre-filled cart or other app-state fixture) is declared in the spec-level session: block, and network shaping in mock: - see test-context seeding before migrating a suite's setup helpers step by step.

Actions (web, sap, vision — the generic grammar)

There is deliberately no Blur step. Blur is not something a user does; it is a DOM event that a user action causes. Press Tab is that action, it already works, and it additionally tests what the user really experiences - that focus lands somewhere sensible. Blur-triggered form validation is exercised with Press Tab.

Refused on purpose

Blur is one of a set. When deterministic rule authoring is selected, these shapes are recognised in order to be refused: each fails with the reason and what to write instead. A refused rules: step is never rerouted to the model. That difference is the point: explicit deterministic intent must either mean exactly what the grammar says or stop, never be quietly reinterpreted as something adjacent that records green.

Native dialogs

A native window.alert / confirm / prompt (and the navigation beforeunload) blocks JavaScript synchronously: nothing else runs until it is answered. So it cannot be its own step AFTER the click that opens it - by then the page is already frozen waiting. Instead the disposition folds into the triggering action as a comma suffix, and the engine arms a one-shot handler BEFORE dispatching the click:

- Click "Delete", accepting the "Are you sure?" dialog
- Click "Cancel", dismissing the dialog
- Press the "Rename" button, answering the prompt with "New name"

accepting presses OK, dismissing presses Cancel. The message is optional; when present it is matched contains, and it IS the assertion - a dialog whose text does not contain it fails the step. answering the prompt with "<text>" accepts a prompt and supplies the reply; the reply is authored input like Type, so a ${VAR} reference resolves at execution and only the reference is stored. The suffix works on every trigger - Click, Press the … button, Right-click, Double-click, Hover - and composes with the scoped in the item containing "<anchor>" form.

The post-condition is verified: a declared dialog that does not open fails the step (parallel to Check verifying its state took). And a flow-wide safety net catches the other direction - a step that triggers a dialog it did NOT declare is dismissed and failed with an unexpected dialog opened: <message>, never left to hang (the least diagnosable failure). Both directions are deterministic. Native dialogs are web only; a desktop message box is a real window, driven by ordinary steps.

Assertions (every app — the shared grammar)

All assertion forms auto-wait (default 10s, recorded into the trace); append within <N>s to any form to change the bound.

Two different questions share the word "times", and picking the wrong one is a quiet way to write a test that cannot fail:

- assert: page shows Pending 3 times      # the TEXT appears 3 times anywhere
- assert: the "css:.order-row" appears 3 times   # 3 ELEMENTS match

A list assertion almost always wants the second. Three rows whose labels happen to repeat a word are still three rows, and a row that renders its status twice would satisfy the first without any row existing at all.

Counting rides on the same ordinal as the 2nd "Row", so it means on each adapter exactly what an ordinal means there: DOM order on web, UIA tree order on the desktop, reading order under vision. A passing count costs N + 1 questions to the app; only a FAILING one counts further, so the error can say found 5 rather than just "not 3".

The URL forms map cy.location("pathname").should("equal", "/signin") and cy.url().should("include", "checkout"), and they auto-wait like every other assertion, because an SPA redirect lands asynchronously:

- assert: page url is /signin
- assert: page url contains checkout
- assert: page title is Orders - Acme Admin
- assert: page title contains Acme
- assert: page url is /orders?page=2 within 15s

Checkboxes map cy.check() / should("be.checked"):

- Check the "Remember me" checkbox
- assert: the "Remember me" checkbox is checked
- Uncheck the "Remember me" checkbox
- assert: the "Remember me" checkbox is not checked

Scoped targets: table cells and list items, by identity

Repeated UI - a grid's rows, a list's items, a board's cards - needs a way to say WHICH one without counting. Both forms name the region by its content and then address the element inside it:

# a table cell: the column's header text plus an anchor identifying the row
- assert: the "Status" column of the row containing "Grace Hopper" shows Suspended
- assert: the "Balance" column of the row containing "Grace Hopper" is empty
- Click the "Actions" column of the row containing "Grace Hopper"

# a list item: an anchor identifying the item, then the ordinary target
- assert: the "css:.amount" in the item containing "Invoice 4711" shows 50.00
- assert: the "Amount" field in the item containing "Invoice 4711" contains 50
- Click the "Pay" in the item containing "Invoice 4711"
- Check the "Select" checkbox in the item containing "Invoice 4711"

# a container the `item` rung cannot see: name it
- Click the "Ship" in the "css:.card" containing "Order 8801"

# one column does not always name a row: require both
- Click the "Edit" in the item containing "John" and "Doe"
- assert: the "Email" column of the row containing "John" and "Doe" shows john@example.com

The same cell target composes with every predicate (shows, is empty, is [not] visible, is enabled, checkbox is [not] checked, attribute <name> is [not] <value>, has|does not have attribute <name>, style <prop> is [not] <value>) and every action (Click, Type … into, Clear, Check, Scroll, Select). in the row containing also works - the of/in coin flip is one you should not have to remember.

A dropdown inside a row is the case this exists for. A page that puts one <select> per row gives them all the same label, so without a scope the only way to reach the third one is the 3rd "Value" - the positional addressing scopes were built to remove:

- Select Approved from the "Value" column of the row containing "Invoice 4711"
- Select "A", "B" from the "Tags" field in the item containing "Invoice 4711"

A column is matched by its header's text and then addressed by that header's position within its own row, counting header and data cells together. A schedule-style grid whose header row opens with a stub above the row-label column (<tr><td></td><th>Monday</th>…) therefore lines up: counting ths against tds would read one column to the left, and return a real cell, which passes as confidently as the right one.

Both targets compose with every predicate (shows, shows ${captured.x} ± n, is [not] empty, is [not] visible, is enabled|disabled, field contains, checkbox is [not] checked) and every action (Click, Type … into, Clear, Check/Uncheck, Press … button, Right-click, Remember … as): one shared suffix parse rebinds the target, so nothing composes specially. A role noun goes BEFORE the scope phrase: the "Amount" field in the item containing "X" contains 50, Check the "Select" checkbox in the item containing "X".

Why identity, not the 2nd ".column-status": an ordinal encodes position, so inserting a row or reordering a column silently makes the assertion hit the wrong record. Identity survives both - the trace records the header text, the anchor, and (when the live DOM offers one) the row's or container's own id as a fallback, and replay finds them wherever they moved. For that reason an ordinal cannot address a scoped target on either half: the 2nd "Status" column … and the "Amount" in the 2nd item containing … are both parse errors. Nor can the two nest: one container, or one cell, and the element inside it.

Resolution is generic over any <table> or ARIA grid (role=grid/table/ treegrid), so react-admin, MUI DataGrid and AG Grid all work with no framework-specific selector. Two things are hard errors rather than a silent wrong guess, and both point at the css: escape hatch: a row anchor that matches more than one row (use a more specific anchor), and a duplicate column header. Known boundary: a virtualized grid that keeps off-screen rows out of the DOM (AG Grid's row virtualization) can only be addressed for rows that are rendered; bring the anchor row in with Scroll "<anchor>" into view first (or use css: against the grid's own row API), then the cell predicates - shows, attribute <name> is <value>, style <prop> is <value>, and the rest - resolve it. Cell resolution is generic over any <table> or ARIA grid (role=grid/table/treegrid), so react-admin, MUI DataGrid and AG Grid all work with no framework-specific selector. Container resolution has two rungs and no heuristics: the explicit css:/id: selector, or the closed item list above. Among the containers holding the anchor the innermost wins, so an item nested in a group resolves to the item.

Three things are hard errors rather than a silent wrong guess, and all three point at the css: escape hatch: an anchor matching more than one row or item (use a more specific anchor or a css: container), a duplicate column header, and a container that is neither item nor a selector (in the "Transaction" containing …, where "Transaction" is a noun, not a container).

Steps are not instant, and some apps care. A click step costs roughly 0.2 seconds between the action landing and the next one reaching the page, and typing adds about 20ms per character — measured on a local fixture with no network. The cost is CDP round trips, and a keystroke is two of them. The probes that only need an answer — does the target exist, is it actionable — each ask the page in a single round trip for css and text-anchor targets; earlier engines walked an element-handle path that cost four to six calls per question, which put a step at 3.1-3.2s.

Those numbers assume the patched transport this workspace pins (see the [patch.crates-io] block in the root Cargo.toml). The published headless_chrome transport shares one mutex between the socket reader and every sender, and the reader holds it across a blocking read — so a send waits out a read rather than proceeding. Profiling found the reader holding that lock for 94% of a run's wall-clock while the writes themselves cost 0.07ms each. Unpatched, a click costs ~1.4s and a character ~213ms, which is where the "0.2s per character" figure in older notes comes from. The patch shortens the read timeout and stops polling for responses; it does not remove the shared lock, so a send still queues behind a read.

A deadline-bearing interaction — a value that stays valid for two seconds, a token that expires, a confirmation that auto-dismisses — may still be out of reach once a step involves typing more than a few characters, and the failure is at least loud rather than silent: the app's own complaint (an alert, a rejection) surfaces as a failed step rather than a green run that did the wrong thing.

If a flow needs to beat a deadline, the honest options are to remove the deadline from the environment under test (mock: the endpoint that issues it, or pin the clock) rather than to hope the step lands in time.

Known boundaries. A virtualized list or grid that keeps off-screen rows out of the DOM (AG Grid's row virtualization, windowed feeds) can only be addressed for what is rendered: scroll the anchor into view first, or use css: against the widget's own API. Content inside a closed shadow root or a cross-origin iframe is unreachable to any selector, scoped or not. And an anchor that appears in EVERY item ("Invoice", when every item says "Invoice") is ambiguous by design: it identifies nothing, and the error says so instead of picking the first one. appears <N> times cannot be scoped to a container yet.

Remembering and reusing live values

Model-authored steps may describe a remembered value naturally and use a clear name or an unambiguous pronoun later:

- Remember the order number
- Enter it in the "Confirmation" field

Recording grounds both steps to the live scene and persists deterministic capture/read and type actions. The remembered value itself is still read fresh during recording and replay; it is not baked into the trace. A named reference is useful when the flow remembers more than one value:

- Remember the order number as the order ID
- Remember the customer number as the customer ID
- Enter the order ID in the "Confirmation" field

A pronoun such as it is accepted only when one remembered value is an unambiguous candidate. If two values could be meant, recording stops with a structured clarification that lists the candidates. It does not choose the nearest name or the first value.

For exact deterministic grammar, ${captured.<name>} remains the explicit advanced syntax. Mark the steps with rules: (or record the whole flow with --author rules):

- rules: Remember the "id:oid" as oid
- rules: Type ${captured.oid} into the "Order id" field

Computed assertions answer "did this change by the right amount?", which a literal cannot express because the starting value is only known at run time:

- Remember the "Account Balance" as balance
- Press the "Pay" button
- assert: the "Account Balance" shows ${captured.balance} - 100

The expression grammar is deliberately tiny and does not compose: one capture reference, optionally one + or -, and one plain number. There is no second capture, no nesting, no * or /.

A capture may also be typed, which is how a value the app generates per run gets entered — there is no literal a trace could record, so the trace stores the reference and every replay reads the value fresh:

- Click "GENERATE ORDER ID"
- Remember the "id:oid" as oid
- Type ${captured.oid} into the "Order id" field

A typed value is interpolated, not evaluated. Every ${captured.<name>} in the text is replaced by what that element displayed, and the literal characters around them are typed as written:

- Type order-${captured.oid} into the "Ref" field      # order-1061367
- Type ${captured.first} ${captured.last} into the "Name" field

More than one reference in one step is fine, and so is a step that is all literal apart from them. What does not happen is arithmetic. This:

- Remember the "id:no1" as a
- Remember the "id:no2" as b
- Type ${captured.a} + ${captured.b} into the "Sum" field

types 12 + 30 — three tokens of displayed text with a plus sign between them — and not 42. That is interpolation behaving correctly, not a bug, and it is the reason the step is worth spelling out: 12 + 30 looks close enough to an answer that a flow could go green on it while asserting nothing anybody meant.

Arithmetic is refused deliberately, not merely absent. A capture is text the app displayed, and supplying it back is data entry — the thing a user does with a generated id. Deriving a new value from two of them is a computation, and a trace that carries a computation has stopped being a recording of what happened. The one exception is on the assertion side, where shows ${captured.x} + <number> answers "did this change by the right amount?" — a question a literal cannot express, because the starting value is only known at run time. It takes one capture and one plain number, and it does not compose.

A name that was never remembered fails closed, naming what was in scope, rather than typing the reference or an empty string.

A counted capture is the same value with a different reading, so it composes with everything a captured value already does — including the computed comparison, which needs no second definition of what a number is:

- Remember how many "css:.order-row" appear as rows
- Type ${captured.rows} into the "Rowcount" field
- Press the "Add row" button
- assert: the "Total" shows ${captured.rows} + 1

Typing is where it stops. A capture may not choose an element or a destination - Click "${captured.x}", Go to ${captured.x}, or a capture in a target label are all parse errors, because that would let the app under test decide what the flow does next. Supplying text it just displayed is data entry; picking the next element is control flow. A name that was never remembered fails closed, naming what was in scope.

Handing a value to the next flow (exports:)

A capture is flow-scoped. exports: is how one crosses to the flows that run AFTER this one in a suite — which is how a test case spans technologies: one flow drives SAP GUI and captures the order number off the status bar, the next drives the web portal that must show it. Each flow keeps its own app: and its own driver; the suite is the test case, and the export is the thread through it.

# a-create-order.flow.yaml — SAP GUI mints the order number
name: Create standard order
app: sap
steps:
  - Go to /nVA01
  # ... create and save the order ...
  # VA02 opens with the order just created already filled in, so the number
  # has an element of its OWN. That is the shape a capture needs — reading
  # it out of the status bar's sentence would be pattern matching, which
  # the grammar refuses.
  - Go to /nVA02
  - Remember the "id:wnd[0]/usr/ctxtVBAK-VBELN" as order
exports:
  ORDER_NO: ${captured.order}

# b-verify-portal.flow.yaml — the portal must show what SAP minted
name: Order appears in the portal
app: web
url: ${PORTAL_URL}/orders
steps:
  - Type ${ORDER_NO} into the "Search" field
  - assert: page shows ${ORDER_NO}

Each export is ENV_NAME: template. The template may carry ${captured.<name>} references (this flow's captures) and plain ${VAR} references (the environment, resolved like suite env). When the flow's last step has passed, the templates resolve and the pairs become environment variables for the remaining flows — which reference them as ordinary ${VAR}s, so the downstream trace stores only the reference and resolves it fresh on every replay. The handoff happens at REPLAY time, from replay-time captures: flow B replays against the value flow A's replay just read, not against a value frozen at record.

What holds, and why:

• Nothing is persisted. Like a capture, an exported value exists only in the memory of the run. The trace holds the capture name, the run report and the [EXPORT] line hold the export NAME — an order number or balance stays out of committed artifacts and CI logs alike.
• An export that cannot resolve fails the flow that owns it. A ${captured.<name>} never remembered fails THIS flow with the captures that were in scope — not the downstream flow, which would otherwise fail holding a variable nobody visibly set. And a failed flow exports nothing: no partial contract.
• A single flowproof run <spec> resolves exports too, though there is no downstream flow to receive them — the verdict must not depend on whether the flow ran alone or in a suite.
• app: agent flows cannot export (a parse error): they record at the model boundary and have no captures. Chain them as consumers — an agent flow's spec can reference ${ORDER_NO} like any other.

The suite's existing machinery composes: env_from mints the data the FIRST flow needs, order: in suite.yaml pins who runs before whom, and exports: carries what a flow LEARNED to whoever follows.

iframes (same-origin, assertions)

An element inside an iframe is addressed with the same target-tail shape as a container scope:

- assert: the "css:#total" in the iframe "checkout" shows Total 42.00
- assert: the "Status" inside the iframe "checkout" is visible
- assert: the "css:#total" in the iframe "css:iframe[title=checkout]" shows Total 42.00

The frame names itself the way any target does: a quoted anchor matched against the iframe's own title, name, id, or aria-label, or an explicit "css:<selector>". The phrase is cut out of the tail like the container phrase, so every predicate composes without special casing, and a role noun still goes before it.

The frame is a fence, not a hint. The inner target is looked up in the frame's own document and nowhere else: if it is not in the frame, the assertion fails even when an identically named element sits on the page outside it. That is the whole point - a scope that silently fell back to the main document would pass green on the wrong element.

Three failures are kept distinct so none of them can read as a pass:

Limits in v1, each for a reason rather than for later:

• Value-driving actions, not pointer actions. Type, Replace, Clear, Check/Uncheck, Remember and Scroll work inside a frame; Click, Press … button, Hover, Double-click, Right-click and Upload are a parse error naming the reason.

  The original refusal covered every action, on the grounds that actions act at composited coordinates resolved against the main document and so could "succeed" without touching the frame. That reasoning was right, and it is specifically about COORDINATES. A same-origin frame does not need them: the parent's own scripts can reach iframe.contentDocument, so a value action is driven through the frame's DOM - the same mechanism Select uses in the main document - and nothing is dispatched at a point.

  A pointer action has no such route. It could only reach the frame as an untrusted event (isTrusted is false), which an application is free to ignore while the step still passes - release-without-effect. So those stay refused until a trusted mechanism exists.

  A framed Type is not the main-document Type. In the main document it is real keystrokes typed over a select-all (fill semantics - the field ends up reading the text exactly); inside a frame it is a value assignment plus input/change. Both replace, but an application that filters on keydown sees the main-document keys and not the framed assignment. Two guards keep that honest rather than silent: the target must not be disabled or read-only (a value assignment succeeds on a disabled control where typing would be ignored - so it is refused by name), and the value is read BACK from the element afterwards, so a control that rejected or rewrote it fails the step.

• Same-origin only. A cross-origin frame's document is unreachable, and the CDP per-frame execution-context path is not deterministic enough to ship behind a grammar that looks identical.

• One frame, no combining. A frame scope cannot be nested inside a container or cell scope yet; one context per target.

• An ordinal cannot address a frame (the 2nd iframe): name it.

Cookie controls (web, security)

"The session cookie is httpOnly" is a control that regresses SILENTLY: an auth library config changes, the cookie becomes readable by page scripts, and nothing about the UI looks different. These assertions pin it.

control:
  id: sec.session.cookie-flags
  title: The session cookie is not readable by page scripts
steps:
  - assert: cookie "session_token" exists
  - assert: cookie "session_token" is httpOnly
  - assert: cookie "remember_me" is persistent

A cookie's VALUE cannot be asserted, and never will be. A session cookie's value is a credential. There is no cookie "x" is <value> form, no contains, and no redacted comparison: the moment a value can be compared, the expected value has to live in the trace and the failure message tempts someone to print the actual one. flowproof's traces are meant to be safe to commit and safe to attach to a bug report. A failure names the cookie, which fact failed, and - for a missing cookie - the NAMES of the cookies that were set, which is what fixes a typo.

The is secure honesty note. Browsers exempt localhost from the secure requirement, so is secure can pass over plain http and certify nothing about production. The step still passes, because teams do run TLS-terminated staging, but the run prints a warning saying it does not certify production behaviour. Read that warning as a finding: a control that has only ever passed over http is an unverified control.

Out of v1: sameSite (three-valued, so it does not fit the is <flag> shape), exact expiry timestamps (nondeterministic across record and replay), and domain/path matchers.

Repeating a block (foreach)

A block that repeats with one value changing collapses into a foreach values matrix. Scalars are referenced with ${each}, mappings with ${each.<key>}; a whole-string token keeps its YAML type, so status: ${each.status} stays a number. Expansion happens at parse time - each iteration becomes an ordinary recorded step, so a foreach adds no runtime construct to the trace.

steps:
  - foreach:
      values: [mysql, mssql, oracle]
      steps:
        - assert_api:
            request: POST ${API}/connections/test
            body: { type: "${each}" }
            status: 500

Repeating until the app settles (repeat: and when:)

foreach repeats a block as many times as you know when you write it. Sometimes you do not know — press a button until the label changes, recover if an error appeared. Those are repeat: and when:.

steps:
  - repeat:
      until: the "id:button" shows Enough
      max: 15
      steps:
        - Press the "id:button" button
  - when: the "id:b1" is not visible
    steps:
      - Press the "id:tech" button

Both expand while recording, not while replaying. The condition is read against the live app, and what lands in the trace is the passes that actually ran — ordinary concrete steps, no repeat and no when. The trace stays a recording of what happened and replay still decides nothing. Against a non-deterministic application that recording only replays against the same behaviour, which for a regression test is the right way round: a flow that silently re-adapted every run would always pass.

until: is checked before the first pass, so a repeat: whose condition already holds runs zero times. max: is required: if the condition never holds within it, recording fails and names the bound. Each repeat: gets its own budget.

Conditions read state; they never wait:

A missing element makes a positive shows false and a negative one true — the same reading replay takes. Anything else is refused by name.

The comparison is the one condition that weighs two readings against each other rather than a reading against a literal, and it is numeric: "9" is greater than "10" as text and smaller as a number, and a condition that quietly answered the text question would be worse than one that refuses. A side that does not read as a number fails the recording and is quoted back.

Scope conditions tightly: page shows ERROR also matches a heading reading "Errors occur", so name the element instead.

Driving an arbitrary Windows app (app: mapping, window: config)

app: is normally a registry id (web, calc, notepad, sap, vision, api). It also accepts a mapping, which drives any Windows program through UI Automation:

app:
  command: '"C:\Program Files\My App\app.exe" --profile=test'
  window_title: ${APP_WINDOW}
window:
  width: 1280
  height: 800

command is a command LINE, not a program name: the program may be quoted so a path with spaces survives, and everything after it reaches the app verbatim. Both fields take ${VAR} references, resolved at launch and stored RAW in the trace. command is executed code, the same trust surface as a suite's env_from: a spec is code.

window: pins the window's shape, which is a determinism precondition for visual assertions rather than something a user does - so it is config, applied once before the first step and identical at record and replay, not a step. width and height go together; x and y are optional but go together and need a size. Geometry values are literal integers, never ${VAR}: a precondition that varies by environment is not one. The trace records what was APPLIED, so a spec that gives only a size still pins the position the window landed on.

A vision flow names the window it attaches to in the same block, and may pin geometry too - which is where it matters most, because OCR baselines depend on it:

app: vision
window:
  title: Citrix Receiver
  width: 1280
  height: 720

Each app kind has exactly ONE spelling for naming a window: app.window_title for a Windows program flowproof launches, window.title for a window vision attaches to but never launched. Using the wrong one is a parse error that names the right one. A web flow sizes its page with browser: viewport, and an api flow has no window at all.

UWP and packaged apps

A UWP app (Calculator, Settings, anything from the Store) is not an exe you launch by path. Launch one through the shell, naming the package by its Application User Model ID:

app:
  command: explorer.exe shell:AppsFolder\Microsoft.WindowsCalculator_8wekyb3d8bbwe!App
  window_title: Calculator
window:
  width: 640
  height: 900

explorer.exe returns immediately, before the app has a window, which is exactly why window_title exists: flowproof waits for a window with that title rather than for the process it spawned. List the ids on the machine with Get-StartApps in PowerShell.

The window matters for geometry. A UWP app draws into a Windows.UI.Core.CoreWindow hosted inside an ApplicationFrameWindow that belongs to ApplicationFrameHost.exe, and the CoreWindow does not own its own size - resizing it does nothing visible. flowproof detects the CoreWindow class and applies window: to the hosting frame instead, so a UWP flow pins its shape like any other. Nothing to configure; worth knowing only when a resize appears to be ignored.

For running a UWP app on a CI runner that does not ship one, see Deploying a UWP app on a CI runner: a Windows Server image has no Store apps, but it can build and side-load the one a suite needs.

Multi-surface flows (apps: and in: blocks)

One test case, several technologies, one flow file, one trace. Declare the surfaces under apps: and put steps in in: blocks; exactly one surface is active at a time, and captures share one namespace across blocks:

name: Order across GUI and portal
apps:
  gui: {app: sap, connection: "${SAP_CONNECTION}"}
  portal: {app: web, url: "${PORTAL_URL}/orders"}
steps:
  - in: gui
    steps:
      - Go to /nVA01
      # ... create and save the order ...
      - Go to /nVA02
      - Remember the "id:wnd[0]/usr/ctxtVBAK-VBELN" as order
  - in: portal
    steps:
      - Type ${captured.order} into the "Search" field
      - assert: page shows ${captured.order}

What holds, and why:

• One surface active at a time. SAP GUI scripting, UIA and vision all inject real input into the foreground window; sequential blocks are correctness, not a limitation. A block boundary launches its surface on the first visit and re-foregrounds it on returns — a later in: gui resumes the same session, same login, same screen.

• Captures cross blocks. The order number read off SAP's status bar types into the portal as ${captured.order} — and the trace stores the NAME, never the value, exactly as in a single-surface flow. On replay the capture is re-read live from this run's SAP and typed into this run's portal.

• Replay needs the trace and nothing else. The header carries the surface map with config stored as written, so a ${VAR} connection or url resolves fresh at every replay — and replay makes zero LLM calls, as always.

• Steps author against their surface's own grammar (what SAP performs differs from what a browser does), and out-of-band asserts (assert_api, assert_sql, assert_spreadsheet) run fine inside any block.

• A web surface carries its own browser: — viewport/device emulation, user-agent, pinned clock, seeded random, exactly the single-surface block, one level deeper:

  apps:
    portal:
      app: web
      url: "${PORTAL_URL}/orders"
      browser:
        viewport: {width: 390, height: 844, mobile: true, touch: true}
  

  It travels on the surface's header entry, so record and every replay launch that surface the same shape. On a non-web surface it is a parse error naming whose config it is. browser: also takes downloads_dir (where downloaded files land — absent means the surface creates its own per-launch temp directory), the field Wait until the download completes as <name> reads back.

• A surface launched with a Windows command/window_title may reference ${captured.x} — a value an EARLIER block captured, resolved at THIS surface's actual activation rather than before any step has run (a value that does not exist yet cannot resolve). This is the seam that lets one block download a file and a later block, in a different application, open it:

  apps:
    fiori: {app: web, url: "${FIORI_BASE_URL}/ui#Shell-home"}
    excel: {app: {command: "EXCEL.EXE ${captured.pir_export}", window_title: "Excel"}}
  steps:
    - in: fiori
      steps:
        - Press the "Export" button
        - Wait until the download completes as pir_export
    - in: excel
      steps:
        - assert: page shows Net Price
  

  An unresolved capture at activation time (the minting block never ran, or ran on the wrong surface) fails the run closed, naming what was missing — never a launch against the literal ${captured.x} text.

• A desktop surface carries its own window: — for vision, the title: names the window pixels mode attaches to (required there, and what finally makes a Citrix/RDP-published app a surface); for sap and windows-mapping surfaces, width/height (optionally x/y) pin the shape at the surface's FIRST activation, recording what was applied so replay reproduces it exactly:

  apps:
    citrix:
      app: vision
      window: {title: "Citrix Receiver", width: 1280, height: 720}
  

  On a web surface window: is a parse error — a page is sized with browser: viewport.

• assert_screenshot works in any block, and its baseline names its surface: the stored identity is <name>@<surface>.png, so two blocks may reuse one spec name and a gui baseline can never be compared against a portal frame. (@ in a spec-chosen name is refused for exactly that reason.)

• Surface kinds are UI kinds: agent (chain an app: agent flow in the suite instead) and api (nothing to drive) are refused at parse, each with its reason — as are flow-level session/mock/redact (and flow-level browser:/window:, which moved into the surface entries).

• flowproof heal works on multi-surface flows — healing is re-record-plus-diff, so it runs on the same surface registry recording uses, and a step that moved between surfaces is flagged as a surface change: the same action against another app is not the same step.

When the case is "do in system A, prove in system B" with no ping-pong, a suite of single-surface flows chained with exports: is still the simpler spelling — one driver per flow, per-flow verdicts, and the same value handoff.

Out-of-band assertions (any app; structured steps, not prose)

- assert_sql:
    connection: reporting        # resolved from FLOWPROOF_SQL_REPORTING
    query: SELECT count(*) FROM orders WHERE ref = '4711'
    equals: "1"
- assert_api:
    request: GET ${API}/orders/4711
    status: 200
    body_contains: "confirmed"
- assert_api:                    # authenticated JSON POST
    request: POST ${API}/connections/test
    headers:
      Authorization: Bearer ${SESSION_TOKEN}
    body:
      provider: postgres
      connectionString: ${TEST_CONN_STRING}
    status: 200
    body_contains: "Database not yet supported!"
- assert_api:                    # response-side JSON-field assertion
    request: GET ${API}/testData/users
    status: 200
    body_json: results.0.balance # a dotted path into the JSON response
    equals: 150953               # the leaf at that path must equal this
- assert_api:                    # how many elements are in a collection
    request: GET ${API}/testData/users
    status: 200
    body_json: results           # the path must resolve to an ARRAY
    count: 5                     # exactly 5 elements (count_at_least: 2 = a minimum)
- assert_api:                    # response-header assertion
    request: GET ${API}/testData/users
    status: 200
    header: Content-Type         # response header name (case-insensitive)
    header_contains: json        # a substring of the header value

headers values and body string values may carry ${VAR} refs. The trace stores only the raw reference; tokens and connection strings resolve when the probe fires (record and every replay). body is any YAML (mapping, list, or string), sent as JSON with content-type: application/json unless you set your own content-type header (yours wins). A body on GET/HEAD/DELETE is rejected at parse time.

body_json reads a value out of the JSON response and asserts on it, alongside status and body_contains (all three may appear on one step; they are checked in the order status, then body_contains, then body_json). The path is a dotted sequence of segments, each a plain object key or a decimal array index: results.0.balance means "the balance field of the first element of the results array". That is the whole path language: there are no wildcards, filters, brackets, or quoting, so a key that literally contains a dot cannot be reached. One body_json per step; to assert several fields, use several steps.

body_json on its own is an existence check: the path must resolve to a scalar leaf (mirroring assert_sql, where omitting equals means a row merely has to exist). Add equals (a string, number, or boolean) to also check the value; equals without body_json is a parse-time error. A string equals may carry a ${VAR} ref, resolved at probe time exactly like body_contains (only the ref travels in the trace). Comparison has two tiers: when both the leaf and equals are numbers, they compare numerically (150953 equals 150953); otherwise they compare by exact canonical text, so a string leaf never numeric-matches a number (the leaf "0953" does not equal the number 953). Only leaves compare, so there is no deep object equality.

The extracted response value never enters the trace: only the request and the raw expectation are stored, and the plucked value exists solely inside the live comparison, re-fetched on both record and replay. The failure modes are soft (the auto-wait loop keeps polling until they clear or the timeout elapses): a non-JSON body reports "response body is not valid JSON"; a path that runs off the document names the segment where it died (path 'results.0.balance' stops at segment 'balance'); a path that lands on an object or array reports "path resolves to a non-scalar; assert a leaf value".

header asserts on a response header, alongside status, body_contains, and body_json (all may appear on one step; they are checked in the order status, then body_contains, then body_json, then header). The header NAME is case-insensitive, per HTTP: header: Content-Type matches a response that spells it content-type. If the response repeats the header, its values are joined with ", " (HTTP field-value semantics) before matching. One header per step; to assert several headers, use several steps.

header on its own is an existence check: the header must be present (mirroring body_json alone, where reaching a scalar leaf is the whole assertion). Add header_equals (exact value) or header_contains (a substring) to also check the value; at most one of the two per step, and either without header is a parse-time error. Value comparison is case-SENSITIVE (unlike the name). A header_equals/header_contains value may carry a ${VAR} ref, resolved at probe time exactly like body_contains (only the ref travels in the trace). The live header value never enters the trace: it exists solely inside the comparison, re-fetched on both record and replay. The failure modes are soft: an absent header reports "response has no '' header (status )", and a value mismatch reports "header '' is '', expected <equals|contains> '' (status )".

- assert_spreadsheet:
    path: ${captured.pir_export}   # may carry ${captured.x} / ${VAR} refs
    sheet: Sheet1                  # optional; the workbook's first sheet if absent
    at: B2                         # an absolute A1 reference ...
- assert_spreadsheet:
    path: ${captured.pir_export}
    column: Net Price              # ... OR a header + row anchor, not both
    row_contains: "100-100"
    equals: "12.50"

- assert_api:                    # poll a write until it converges
    request: POST ${API}/jobs
    status: 202
    retry: true
- assert_api:                    # ask a read exactly once
    request: GET ${API}/jobs/1
    status: 200
    retry: false

- assert_screenshot:
    name: dashboard              # baseline PNG name (no path, no extension)
    mask: ["css:.clock", "Sync"] # optional: selectors blanked before compare
    threshold: 0.001             # optional: fraction of pixels allowed to differ (default 0)

mock:
  - url_contains: /api/rates          # substring match on the request URL
    method: GET                       # optional; any method when absent
    status: 200                       # optional; default 200
    body:                             # any YAML: string served verbatim
      rate: 1.23                      #   (text/plain), anything else as
      source: mocked                  #   JSON; content_type: overrides

browser:
  viewport:                   # device emulation, applied before navigation
    width: 390
    height: 844
    device_scale_factor: 3    # optional; default 1
    mobile: true              # optional; mobile layout + meta-viewport
    touch: true               # optional; emulate a touch screen
  user_agent: my-agent        # optional; navigator.userAgent override
  args: ["--lang=en-US"]      # optional; extra Chrome flags
  clock:                      # optional; pin the clock (GAP-P)
    at: "2026-01-15T12:00:00Z"   # required; RFC 3339, a mid-day time
    timezone: "Europe/Berlin"    # optional but recommended; IANA id

browser:
  random:
    seed: 1234

- assert: the "id:no1" shows 91        # the draw itself
- assert: the "id:no2" shows 98
- Type 189 into the "id:result" field  # the constant derived from it

name: A viewer cannot delete a customer
app: web
url: ${APP_URL}/customers
control:
  id: ac.customers.delete.viewer-denied      # required
  title: Viewer role is denied customer deletion   # optional
  description: >-                              # optional
    The viewer session may read a customer but the API refuses its DELETE.
steps: [ ... ]

- assert_no_secret_leak: ${DB_PASSWORD}        # one named secret
- assert_no_secret_leak:                       # or several at once
    - ${DB_PASSWORD}
    - ${API_TOKEN}

$ flowproof run examples/access-control              # writes the run record
$ flowproof audit examples/access-control            # YAML on stdout
$ flowproof audit examples/access-control --json     # JSON instead
$ flowproof audit examples/access-control --run <id> # a specific past record

suite: access-control
run: 2026-07-24T09-14-03Z-a1b2
controls:
  - id: ac.customers.delete.viewer-denied
    title: Viewer role is denied customer deletion
    flow: viewer-cannot-delete.flow.yaml
    verdict: pass
    evidence:
      trace: viewer-cannot-delete.trace.jsonl
  - id: sec.assistant.no-db-password-leak
    title: The DB password never surfaces in agent output
    flow: assistant-no-leak.flow.yaml
    verdict: pass
    lanes: [secret_leak]
    evidence:
      trace: assistant-no-leak.trace.jsonl
    secrets_checked: ["${DB_PASSWORD}"]        # variable names, never values
    corpus:
      - model-boundary trajectory (cassette request and response bodies)
      - MCP lanes
    excluded:
      - channels the engine never observed (server logs, third-party sinks)

$ flowproof audit examples/access-control --since 2026-07-24T09-14-03Z-a1b2

base: 2026-07-24T09-14-03Z-a1b2
head: 2026-07-24T11-02-55Z-9f3c
added:
  - id: ac.orders.refund.viewer-denied
    verdict: pass
removed: []
changed:
  - id: sec.assistant.no-db-password-leak
    old: pass
    new: fail

flowproof author-from-doc uat-export.pdf --app sap --name "Manage purchasing info records" --out draft.flow.yaml