The authoring grammar — every accepted form

record resolves each spec step with deterministic rules first; anything the rules cannot parse falls back to the LLM author (when a model backend is configured). This page is the complete rules grammar. Nothing here requires a model call, and everything here is covered by a test that parses 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).

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, or an associated <label> (both <label>Name: <input/></label> wrapping and <label for>/id pairing). 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. 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.

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

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.

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!"

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.

Visual assertions (structured step)

- 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)

record captures the surface, blanks each mask's element rect, and mints <spec-stem>.baselines/<name>.png next to the trace — re-recording (or record --reuse) is how baselines refresh. Replay captures with the same masks and compares pixel-exact (up to threshold); on failure the run bundle gains visual/<name>.actual.png and visual/<name>.diff.png (differing pixels in red) and the message names the diff percentage. Masks take the same forms as quoted labels (text anchor, css:, id:) and every mask must resolve — a silently-unmasked volatile region would mint a flaky baseline. Pin the viewport with browser: so capture dimensions stay stable across machines.

Network mocks (web flows; spec-level, not steps)

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

Requests matching a rule are answered inside the browser — the real host is never contacted (it need not even exist). The rules travel in the trace header and apply identically at record and replay: what was mocked once is mocked always, which is what keeps the two executions equivalent. Mocked responses carry permissive CORS headers and answer preflights, so cross-origin fetch() calls just work. The tool for third-party calls (payments, analytics) and hard-to-provoke server states; for asserting on real APIs, use assert_api instead.

Browser config (web flows; spec-level, not steps)

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

The config travels in the trace header and applies identically at record and replay — a flow recorded on an emulated phone never replays on a desktop viewport. This is how *.mobile test variants and deterministic-seeding user agents (previously an env-var wrapper around Chrome) become first-class. args forces a private (non-shared) browser for the flow, since flags only apply at process start — expect its cold start. A suite's suite.yaml may carry the same browser: block as a default for every flow; a flow's own block wins outright.

App sugar

• calc: Type <digits> (one press per digit), Press plus|minus|times|divided by|equals, assert: display shows <number>.
• notepad: Type <text>, assert: document contains <text> (plus the shared grammar).

When a step doesn't parse

The error names the accepted forms for that app. Anything freeform (e.g. Smash the shiny button) is handled by the LLM author when a model backend is configured (FLOWPROOF_AI_PROVIDER / FLOWPROOF_AI_API_KEY) — the model grounds the step against the live scene and can never invent a selector; replay stays zero-model either way. See getting-started.

When a step is too ambiguous to author at all ("make required field changes" — which fields?), recording fails with a structured clarification payload: the stuck step plus the live screen's field inventory, via record --json, the MCP record tool, or Python's ClarificationNeeded. The driving agent rewrites the step into concrete grammar and re-records — see self-help.md for the loop.