When authoring gets stuck

Choose the intended authoring backend

In auto mode, plain freeform UI text (for example, Smash the shiny button) is model intent. The model receives the live scene and must ground its answer to one of the listed target tokens; it cannot invent a selector. An explicit rules: step instead succeeds or fails against the grammar on this page and names the accepted forms for that app. Use --author rules or --author llm when the entire recording should force one backend.

When auto mode has no configured model (flowproof config ai, or FLOWPROOF_AI_PROVIDER / FLOWPROOF_AI_API_KEY), the CLI emits a visible warning before trying the deterministic grammar. This fallback is identified as its own fallback route in the per-step human and structured diagnostics, so ordinary prose is never silently mistaken for deliberate rule syntax.

Resolve an ambiguous step

When a step is too ambiguous to author at all ("make required field changes", which fields?, or Enter it with several remembered values), recording fails with a structured clarification payload: the stuck step plus the relevant live-scene fields or remembered-value candidates. It is available via record --json, the MCP record tool, or Python's ClarificationNeeded. The driving agent rewrites the step more precisely and re-records; see The outside-in loop for the loop.

Whichever route authors a step, recording persists grounded selectors and actions in the trace. flowproof run executes those deterministic artifacts directly and makes zero authoring-model calls. See getting-started.

Drafting a spec from a requirement document (author-from-doc)

QA teams already write test cases in a test-management tool and export them as a document (today: an HP ALM/Quality Center PDF, with Step Name / Description / Expected / Actual fields per step). flowproof author-from-doc reads that PDF and drafts a .flow.yaml spec from it, instead of hand-translating the same steps twice:

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

• --app: the target app id the draft's app: field is written with (sap, web, …).
• --name: the flow name written into the draft's name: field.
• --out: where the draft .flow.yaml is written.

A draft is one test case. An ALM test-set report holds a run of each test case in the set, so name the one to draft with --test-case: its number as --check lists them, its name, or its ID (the part of the name before -). A test case run more than once is read from its latest run.

flowproof author-from-doc test-set.pdf --check
flowproof author-from-doc test-set.pdf --test-case M-040-090-020-1 --app sap --name "TECO production order" --out teco.flow.yaml

To draft several test cases, repeat --test-case, or give --test-case all. --out is then a folder, and each test case is drafted into its own flow there. The flow is named after its test case without the ID, unless two names would then be the same. Its file is named after the test case too, e.g. m-040-090-020-1-teco-production-order.flow.yaml. Nothing is drafted if any of those files already exists. A test case the model fails on is reported and the others are still drafted. The exit code is 1 when some failed and 2 when none were drafted. With --json, the result is {"drafts": [...], "failed": [{"test_case", "error"}]}, where each draft has the same fields as a single draft's JSON.

flowproof author-from-doc test-set.pdf --test-case all --app sap --out drafts/

When the document contains concrete non-secret business data, such as a material, supplier, plant, customer, or order id, the draft can use ${NAME} placeholders and author-from-doc writes a sibling values file next to the flow:

draft.flow.yaml
draft.values.yaml

flowproof record draft.flow.yaml and flowproof run draft.flow.yaml load that values file automatically. Keep passwords, tokens, and login credentials in flowproof config or the caller's secret environment, not in the generated values file.

The PDF's text is extracted and segmented into per-step records, then each Description/Expected pair is translated into this page's grammar by a model call, the same "flag, don't guess" discipline as live authoring above, extended to three distinct outcomes instead of a binary action-or-not:

• A Description that maps cleanly becomes a real step in the grammar above, and its Expected becomes a real assert:, something a video recording never has, since a document already states a belief about correctness.
• A Description that implies an action within the app under test, but too ambiguously to map with confidence, is flagged as a # TODO plus a freeform step for the next live flowproof record pass to resolve against the real screen, never a forced guess.
• A Description whose action clearly targets a different app or tool entirely (e.g. reviewing a downloaded export in a spreadsheet program) is flagged as its own distinct # TODO rather than silently dropped or confused with in-app ambiguity: it isn't automatable here at all, and needs a human decision, not a screen to search.

The output is a draft: review every step, then run flowproof record to resolve any flagged ones against the live app before trusting it.

For tools that call it (the desktop app does), two flags help:

• --check reads the PDF and prints how many steps it holds and how many have an expected result, and for a test-set report each test case with its step count. Nothing is sent to a model and nothing is written, so it is a fast way to confirm the export is readable. With --json it prints steps and with_expected for the whole document and test_cases, each with its name (or null), run_id, steps and with_expected.
• --json prints one JSON object when the draft is written: flow, values (or null), test_case (its name, or null), and steps, each with a kind (action, assert, flagged, out_of_scope), the exact text written to the file, and for the two flagged kinds the observed document wording.

While drafting, drafting step N of M goes to stderr before each model call. The model comes from flowproof config ai or the usual environment variables.

Drafting a spec from an outcome and the app's code (author-from-code)

When nobody has written the steps yet, only the outcome a flow should prove, flowproof author-from-code drafts them from the app's own source. The code already says how the app is navigated: its routes, its link and field labels, where a status is rendered. That beats exploring the live app by trial.

flowproof author-from-code ~/src/portal/apps/web \
  --goal "the supplier list shows Acme Metals with status Active" \
  --name "Find Acme Metals" --url https://portal.example.test --out draft.flow.yaml

• --goal: what the flow should prove, as the screen shows it when done.
• --url: the starting address, written into the draft's url: field.
• --app: the target app id (default web).
• --name and --out: as for author-from-doc.

Two model calls: the first picks up to 12 files from the repository's list of source files, the second drafts steps from those files with line numbers. Every step ends up citing the path:line it rests on, so you check it against the code rather than take it on trust. Dot-files (.env, .git), dependency and build folders, and anything the root .gitignore names are never listed, read or sent. Anything the code cannot settle, such as sign-in credentials or a record that must already exist, is flagged as a # TODO, as above.

With --json, the report is flow and steps, each step with kind, text, observed for a flagged one, and source (file, line) when the model cited a file it was given. reading <path> for each picked file, then drafting steps, go to stderr.