Module formal_ai 

The task loop of the experimental --use-formal-ai mode (issue #255). Mirrors js/src/lib/formal-ai.js.

The natural-language request goes to Formal AI verbatim. Formal AI decides what to observe and which tool calls to make; start checks every call against the effect policy, runs approved calls, reports each receipt back and keeps evidence of what actually happened. The run ends when Formal AI gives its final answer, says it did not understand, or a bound, refusal, protocol error or cancellation stops it, and the exit status says which.

A final answer that is a known capability gap (issue #258) is reported as incomplete with a nonzero exit, and structured read, edit and write calls run under the same workspace policy as bash commands.

A failed change stays unresolved until the same typed tool changes the same target and its readback is verified (issue #261): a later read, a copy over the file or Formal AI’s final answer does not resolve it, and the run then ends incomplete with the original failure and its exit status.

Structs

Outcome

The final state of a run.

TaskOptions

What one task run needs besides the Formal AI client.

Functions

describe_effects

Observed working-directory changes, in words.

describe_gap

Capability gap, in words. When tools changed the working directory, the message keeps what start observed: Formal AI’s gap still means the task is not confirmed, whatever start verified on its own (#261).

gap_obligations

What a capability gap leaves to do, and how to offer the change tools.

lino_gap_record

A final answer that is exactly one Links Notation record whose record_type names a gap, as Formal AI’s task obligations answer (obligation_gap, e.g. reason no_artifact_in_clause): an id line, then key "value" lines. Returned in the JSON gap shape (schema = record_type, never complete), so a gap Formal AI states in its own notation is never taken as success, even when start verified every change it made (#261).

run_formal_ai_task

Run one request to completion. Fills evidence (a JSON object) as it goes, sets evidence.outcome and returns the outcome.

signal_exit

Exit status of a cancellation by signal name (128 + signal number).

track_failures

Keep the failed calls of a run until a later call meets their obligation (issue #261). A failed edit or write is resolved only by a verified edit or write of the same target (a write also resolves a failed read of the file it created); a failed read by a read of the same target; a failed write command only by the same command succeeding. A copy or move over the target never counts as the edit.

unrecognized_gap_record

A final answer that is a JSON (or Links Notation) record of a gap start does not know: it is never taken as success, though its schema grants no recognized gap. A record echoed from a tool message is not Formal AI’s.