flowproof trace format (v1)
Status: shipped. The serde types in flowproof-trace are
implemented against this document and the JSON Schema at
crates/flowproof-trace/schema/trace-v1.schema.json.
A trace is what the recording agent writes while performing a flow once, and the only thing the deterministic replayer reads. Design constraints:
- Replayable with zero LLM calls. Every step carries the full selector ladder with recorded payloads; replay walks the ladder top-down.
- Diffable and reviewable. JSON-lines, one step per line, stable key order, content-addressed artifacts — so healing produces a small, readable diff instead of a silent mutation.
- Provenance-tagged. Every selector says which perception source produced
it (
uia,sap-com,web,vision), so a step records why replay may trust it.
File layout
UTF-8 JSON-lines (.trace.jsonl). Line 1 is the header; every following
non-empty line is a step. Consumers must reject a file whose first line
has format != "flowproof-trace" or an unsupported version.
app: agent traces are a different shape. An agent-boundary flow
(see agent-testing.md) records a self-contained JSON
document ({"app":"agent","mocks":{…},"cassette":{…}}), not JSON-lines and
without the header below, because a new app kind gets a new trace shape
rather than bending the step-log format. A step-log reader never opens one.
An agent flow that mocks MCP tool servers adds one more key, mcp, a map
from server name to that server's lane. Each lane is
{"mocks":{…},"calls":[…],"events":[…]}, where the fields are additive and
skipped when empty, so a trace with no MCP servers (or one recorded before
these fields existed) is byte-identical:
callsis the strict-positional JSON-RPC lane: an ordered list of{"method":…,"params":…,"result":…}, matched by position at replay (method first, then fortools/callthe tool name, then a field-level diff of the arguments). This is the only lane the verdict judges.eventsis the server-initiated NOTIFICATIONS captured on the lane (a JSON-RPC message with amethodand noid), re-emitted at replay. Each is{"after":<n>,"method":…,"params":…}, whereafteris the count of client calls answered when the notification crossed toward the agent.afteris an emission cue, RECORDED and REPLAYED but never MATCHED, so a notification racing at call n versus n+1 changes only the byte ordering, not the verdict. (Two further fields,idandanswer, are reserved for the v3.4 server-initiated REQUEST slice and stay absent until then.)
Header line
{"format":"flowproof-trace","version":1,
"trace_id":"5f0f2f6e-6f0a-4c25-9b1c-1a2b3c4d5e6f",
"recorded_at":"2026-07-18T10:12:33Z",
"spec":{"name":"Create sales order","path":"flows/create-order.yaml","hash":"sha256:…"},
"app":{"name":"SAP GUI for Windows","adapter":"sap-com","window_title":"SAP Easy Access","version":"7.70"},
"agent":{"backend":"anthropic","model":"<model-id>"},
"env":{"os":"windows-11","resolution":[1920,1080],"dpi_scale":1.25,"locale":"en-US"}}
speclinks the trace to the YAML flow spec it was recorded from;hashlets replay detect drift between spec and trace.adapteris the primary perception/adapter mode:uia,sap-com,web,vision(vision = Citrix/RDP mode where only pixels exist), orapi(no UI at all — the flow is out-of-band assertions only). The reserved valuemultiappears only on a multi-surface header (below), never as selector provenance.app.urlis how replay reaches the app again: the URL forweb, the SAP Logon connection description forsap(absent = attach to the running session). Either may be a${VAR}reference, stored raw and resolved at every launch.- Optional
app.login_user(sap) is the user the recording logged in as, stored raw likeurl. The identity is part of what a recording means — an order created by a clerk and one created by an approver are different evidence — so a trace that could not name it would not be reviewable. There is deliberately no password field: the password lives in the spec'slogin:block and is resolved fresh at every launch, so a committed trace has nothing to leak and nothing to redact. Absent = the flow took whatever session was open, fromSAP_USER/SAP_PASSWORDor from a human's own login. agentrecords provenance of authorship only; replay never uses it.- Optional
recordingreferences the authoring execution's recording bundle ({"format": "filmstrip/1", "dir": "...", "started_at"?}); each step'sartifacts.recording {start_ms, end_ms}maps it into that bundle. Optionalredactioncarries the masking rules copied from the spec at record time, so every replay masks identically without the spec (see docs/recording.md). - Optional
sessionseeds pre-launch state (cookies,local_storage) so an authenticated flow starts without a login walk; values may be${VAR}references, resolved at apply time and never stored. - Optional
mockis the network-mock ruleset (web flows), copied from the spec and applied identically at record and replay: each rule matches a request-URL substring (and optionallymethod) and answers it locally. - Optional
browseris the launch/emulation config (web flows):viewport(device emulation),user_agent, extra Chromeargs, andclock({at, timezone}: a pinnedDateoffset plus a CDP timezone override, so a date-dependent flow replays deterministically), andrandom({seed}: a seededMath.random, the clock's sibling, so a flow against a page that mints random values is deterministic), anddownloads_dir(where downloaded files land, applied via CDP at launch socapture_downloadhas a fixed place to look; absent means the driver creates its own per-launch temp directory). All travel in the header so record and every replay run the SAME browser shape. - Optional
appsis the surface map of a multi-surface trace (docs/multi-surface.md):name -> app object, each entry the same shape asapp—{"gui": {"name": "SAP GUI for Windows", "adapter": "sap-com", "url": "${SAP_CONNECTION}"}, "portal": {"name": "web", "adapter": "web", "url": "${PORTAL_URL}/orders"}}. Whenappsis present,appcarries the reserved namemultiwith adaptermulti— deliberately not a copy of any one surface, so an engine predating multi-surface fails LOUDLY at load (an unknown adapter) instead of replaying every step against whichever surface happened to be first. Surface names match[a-z][a-z0-9_-]*; each step names its surface (seesurfacebelow). A web surface's entry may carry its ownbrowserblock (the same shape as the header-level one, which stays the single-surface spelling), applied identically at record and every replay so that surface keeps the shape it was recorded on.
Step line
{"id":"s0004",
"intent":"Enter order type ZOR in the Order Type field",
"action":{"type":"type_text","params":{"text":"ZOR","submit":false}},
"selectors":[
{"tier":"native_id","provenance":"sap-com","confidence":1.0,
"payload":{"id":"wnd[0]/usr/ctxtVBAK-AUART"}},
{"tier":"structural","provenance":"uia",
"payload":{"path":[{"control_type":"Window","index":0},{"control_type":"Edit","index":3}]}},
{"tier":"text_anchor","provenance":"vision",
"payload":{"text":"Order Type","relation":"right_of","max_distance_px":220}},
{"tier":"visual_template","provenance":"vision",
"payload":{"template":"sha256:…","region":[412,318,180,24]}},
{"tier":"ai_relocation","provenance":"vision",
"payload":{"context":"The Order Type input in the Create Sales Order header section"}}
],
"sync":{
"pre":[{"kind":"element_exists","selector_ref":0,"timeout_ms":10000}],
"post":[{"kind":"ocr_text_present","text":"ZOR","region":[412,318,180,24],"timeout_ms":5000}]
},
"artifacts":{"pre_screenshot":"sha256:…","post_screenshot":"sha256:…"}}
Fields
-
id— unique within the trace, monotonically ordered (s0001,s0002, …). -
intent— the natural-language step description. Never executed; used for review, reporting, and as the prompt seed forai_relocation/healing. -
surface(optional) — the named surface (a key of the header'sapps) that executed this step: how a multi-surface replay knows which driver a step belongs to. Absent on single-surface traces, where the header's oneappis the surface — those serialize byte-identically to before the field existed. Optional PER STEP even in a multi-surface trace: an out-of-band assertion (assert_api/assert_sql/assert_spreadsheet) drives no UI and may carry none. -
action.type— one oflaunch,focus_window,click,double_click,right_click,hover,drag,scroll,type_text,press_key,upload,capture,capture_download,set_checked,wait,assert.paramsis action-specific (see schema$defs). Text params (type_texttext, assert expectations) may contain${VAR}secret references: the engine resolves them from the environment at execution time — recording and every replay — and the trace only ever stores the reference, never the value. An unset variable fails closed with an error naming it. Atype_texttext may also contain a${captured.<name>}capture reference, resolved the same way but from the flow's own captures (action.type == "capture") rather than the environment. This is what makes a value the app generates per run enterable at all: there is no literal to record, so the trace stores the reference and each replay reads the value fresh. A name that was never captured fails closed, naming what was in scope. Captures resolve before secrets, because a${VAR}name may not contain a dot.A
capturestep carries{"name": "<name>"}and, for the counted reading,"count": true— how many elements match, rather than one element's text. A new param key rather than a new action type, so a trace written before counting existed still loads and an old reader meeting one does not misread it as a text capture. Either way the trace holds only the name: the number is taken at execution time on record and on every replay, so a page that grew a row does not need the trace rewritten. A counted capture of zero fails rather than remembering0— a selector typo matches nothing and so does an empty table, and the step that means zero is anassertwithelement_count: 0.A
capture_downloadstep carries{"name": "<name>"}and an optional{"timeout_ms": …}, and has no selectors — a download belongs to the surface, not an element on screen, the same reasoningpress_keyuses for the focused element. Likecapture, only the name is stored: the download's resolved path is read at execution time on record and on every replay and lives only in that run's captures, never in the trace.A
kind: "cell"payload may carryrow_anchor_also: [...], and akind: "scoped"payloadanchor_also: [...]— the ADDITIONAL anchors that must all be present in the same row or container, beside the primaryrow_anchor/container_anchor. A new key rather than a changed one, so a reader that knows only one anchor still finds the field it expects; absent in every trace written before conjunction existed, which decodes to the single-anchor behaviour unchanged.A
scrollstep carriesto: "top"|"bottom",into_view: true, orto_px: <n>— an exact offset from the top of the scroll container. A new key rather than a new action, so a trace written before offsets still loads.A
type_text,scrollorcapturestep whose selector payload iskind: "framed"acts INSIDE that frame. The action is performed through the frame's own document rather than at composited coordinates, which is why value-driving actions are recordable there and pointer actions are not — see docs/authoring.md.A
type_textstep may carryparams.values: [...]— a multi-selection, the whole set committed at once. Wherevaluesis present it is authoritative;params.textrepeats only the first option, so a reader that shows text still names something concrete. A consumer that honourstextalone would under-select, which is whyvaluesis the field to read. A new param key rather than a new action type, so a trace written before multi-selection existed still loads.type_textvariants: an emptyselectorsarray means "type into the element that currently has keyboard focus";params.replace: truemarks fill semantics — the input's current value is cleared before typing (a bareClear the … fieldstep is a replace-typing of the empty string).press_keycarries{key, modifiers[]}and never has selectors — it goes to the focused element by definition.A trigger action (
click,double_click,right_click,hover) may carry an optionalparams.dialogobject folding in how a native JavaScript dialog (alert/confirm/prompt/beforeunload) that the trigger opens is answered. A JS dialog blocks JS synchronously, so it cannot be a step AFTER the trigger; the disposition is armed BEFORE the trigger dispatches and a one-shot listener answers it the instant it opens.{"disposition":"accept","message":"Are you sure?","match":"contains","reply":"New name"}dispositionisaccept(OK, supplying anyreply) ordismiss(Cancel/close);messageis the recorded text matched permatch(alwayscontainsin v1), omitted to match any message;replyis a prompt answer, authored input liketype_texttext (a${VAR}reference resolves at execution, so only the reference travels, never the value the page received). The object is strictly additive: a trace without it is byte-identical to before the field existed, and only a trigger action ever carries it. A trace that USESdialogneeds an engine at least the version that introduced it: an older replayer ignores the field and never arms the handler, so the declared dialog would hang rather than be answered. That is a forward-compat note, not a format break. Web-only: non-web adapters reject a step carryingdialog, since a native desktop message box is a real window driven by ordinary steps. -
selectors— the ladder, ordered deterministic-first. Tiers:native_id— UIA AutomationId, SAP GUI Scripting ID, DOM id/CSS.structural— path through the accessibility/DOM tree.text_anchor— OCR text anchor + spatial relation (left_of|right_of|above|below|inside).visual_template— content-addressed image patch + expected region.ai_relocation— NL context for model-assisted relocation. Replay treats reaching this tier as a failure that proposes a heal diff, never a silent fix. A step records only the tiers its perception sources could produce (a Citrix recording may have tiers 3–5 only).confidenceis optional,[0.0, 1.0]. Any rung's payload may carrynth(1-based) to address the nth matching element when a selector legitimately matches several (Type email into the 2nd "Field Name" field).nthindexes the adapter's natural match enumeration — document order on the web, tree-walk order on UIA, reading order for OCR — so the same trace means the same element on every provenance.
A
structuralrung may instead carry a cell payload ({"kind":"cell","column_text":"Status","row_anchor":"Grace Hopper"}), addressing a table cell by its column-header text and a row anchor rather than a tree path, so a row insert or a column reorder does not move the target (see authoring.md). Record may attachcolumn_field/row_idhints read from the live grid, used as fallbacks if the header text or the anchor later fails to resolve.Its sibling is the scoped payload, which addresses an element inside a container identified by an anchor:
{"kind":"scoped","container":"item","container_anchor":"Invoice 4711", "inner_text":"Amount","container_id":"transaction-183VHWyuQMS"}containeris the literalitem(the closed list of list-ish roles) or thecss:…/id:…string exactly as the spec wrote it;container_idis the record-time hint (therow_idanalog), harvested from the container's first present ofid/data-id/data-test/data-testid. The inner target's keys are prefixed -inner_text,inner_css,inner_id,inner_name- and that is load-bearing, not cosmetic: an engine that predates this rung reads barecss/textoff any structural payload, so bare keys here would make it resolve the inner target PAGE-WIDE and pass on the wrong element. Prefixed, the old decode yields an empty selector, skips the rung, and fails loudly. For the same reason a scoped target records no fallback rung: an unscoped text anchor would match any "Amount" on the page and pass green-degraded on a lie.The framed payload is the third of the family, for an element inside a same-origin iframe:
{"kind":"framed","frame":"checkout","inner_css":"#total"}frameis the quoted anchor matched against the iframe's owntitle/name/id/aria-label, or thecss:…string exactly as the spec wrote it. The inner keys are prefixed for exactly the reason above, and here the stakes are the same: an old engine resolving a barecsswould read the MAIN document, which is precisely the element the frame scope exists to exclude. Framed rungs are recorded for assertions only (see authoring.md).Replay semantics: the engine walks rungs in order and acts on the first one that resolves to a live element. Tiers 1–3 execute today (
text_anchorcurrently via accessible-name matching; OCR arrives with the vision mode, as doesvisual_template). Matching on any rung other than the recorded primary keeps the run green but marks the step — and the run —degradedinresult.json, with the matched tier inselector_tier: the flow still works, the app has drifted, heal the trace. -
sync.pre/sync.post— conditions gating the action / confirming its effect. Kinds:element_exists,element_state,window_title,ocr_text_present,visual_stable. Each carriestimeout_ms.selector_refpoints into this step'sselectorsarray by index. -
artifacts— content hashes (sha256:<hex>) of screenshots taken immediately before/after the action. Blobs live outside the trace in the artifact store (.flowproof/artifacts/<hash>), keeping traces small and diffable.
Assertions
action.type == "assert" covers checks as first-class steps. params.kind:
-
element_state— selector resolves and matches{property: value}.expectkeys in use:value_contains,value_equals(+normalize: numeric),value_not_contains(text must be absent),count(withvalue_contains: exact occurrence count of the TEXT, not an element count — provenance-neutral, an OCR adapter counts occurrences in the scene the same way; the ELEMENT countthe "Row" appears N timesserializes instead aselement_countover the step's resolved selector ladder),element_present(true/false — presence itself is the assertion; note this means "the target resolves", not visual visibility — a tree-present-but-hidden element counts as present until the vision mode adds a true visual check), andtimeout_ms(the auto-wait bound; the resolver runs inside the poll, so the target may legitimately appear — or disappear — during the wait).expect.scope: "surface"marks a surface-scoped assertion: no selector ladder (the step'sselectorsis empty,selector_refnull) — the expectation runs against everything readable on the app's surface. Each adapter answers its own way: the page text for a browser, the foreground window's subtree for UIA, the OCR'd frame for a vision adapter. This is howpage shows Xserializes without baking any provenance into the trace. -
ocr_text— OCR ofregion(or the resolved element bounds) matchestext(equals|contains|regex). -
visual_diff— region matchesbaseline(asha256:hash) withinthreshold(0.0–1.0 normalized difference). -
sql— out-of-band DB probe: namedconnection,query,expect(equals: first column of the first row as text;timeout_ms). Credentials are never stored in the trace;connectionis a name resolved fromFLOWPROOF_SQL_<NAME>in the environment at run time (recording and every replay), failing closed when unset. The query may carry${VAR}references, resolved at execution. -
api— out-of-band HTTP probe:request {method,url,body?,headers?}, expectedstatus(default: any 2xx) andexpect(body_contains,timeout_ms). The url, header values, and body string leaves may carry${VAR}references — base hosts, tokens, and connection strings resolve at execution and never persist.bodyis any JSON, sent for POST/PUT/PATCH with an autoapplication/jsoncontent-type unless a usercontent-typeheader is present. -
spreadsheet— out-of-band file probe:path(may carry${captured.x}/${VAR}references — the export this checks is often itself a captured download path — resolved at probe time), optionalsheet(the workbook's first sheet when absent), and a cell addressed EITHER byat(an absoluteA1reference, e.g."B2") OR bycolumn+row_contains(a header/anchor pair resolved against the sheet like a table cell on a live page:columnmatched exact-after-trim then unique-contains against the first row,row_containsthe unique row where any cell contains it) — exactly one form, a parse-time error otherwise.expect(equals,contains,timeout_ms): with neither set, resolving the cell is the whole assertion, mirroringsql's bare row-exists check. Read viacalaminedirectly against the file on disk, not through UI Automation over Excel's grid — untested and known-flaky there.
Versioning
version bumps only on breaking changes; additive optional fields may land
within v1 (the schema allows unknown extra fields on payload and params
but nowhere else). Replayers must refuse newer major versions.