GenServer that plays the dual of ContradictionAgent: probes live branches for satisfiability via an external model finder. A :sat verdict on any branch terminates the session with a confirmed countermodel.

Ticks on params.model_agent_min_delta_ms. On each tick it enumerates branches present in the session's work_queue and idle_queue ETS tables, filters out those whose ancestor is tombstoned, and dispatches a backend probe for each branch whose frontier_version has advanced since we last looked. Verdicts are collected asynchronously and reported to the Manager through the same send_proof_result/2 idiom ContradictionAgent uses.

When params.model_agent_backend is :none the GenServer starts, logs once, and stays passive — no ticks, no probes. This is the historical default and keeps every existing test path untouched.

Failure isolation

Probe Tasks are spawned via Task.Supervisor.async_nolink/2 and monitored. If a Task crashes (or the backend blows up), the monitor :DOWN message cleans the branch out of in_flight so it's eligible for a later re-probe. Without this the branch would stay stuck as "in flight forever."

Telemetry

Emits three event families under [:shot_tx, :model_agent, ...]:

• :tick — every scan pass. Meta includes counts of live / eligible / in-flight / skipped-too-small / skipped-too-big.

• :probe, :start | :stop — per-probe span with branch_id, frontier_size, and terminal verdict_tag.

• :verdict_conflict — when MA and CA fire simultaneously with disagreeing verdicts (indicates a soundness bug — frontier or decomposition).