diff --git a/sdk/tests/test-agent-images.mjs b/sdk/tests/test-agent-images.mjs
index 5ce28c53a..be900078f 100644
--- a/sdk/tests/test-agent-images.mjs
+++ b/sdk/tests/test-agent-images.mjs
@@ -1234,6 +1234,29 @@ for (const [index, mimeType] of mediaTypes.entries()) {
   await restored.close();
 }
 
+// A host tool's image reaches a model the catalog lists with vision but not
+// file-input, as it lists the default spacexai/grok-4.7: file-input covers
+// documents such as PDFs, and image input needs only vision.
+{
+  const model = "sdk/vision-only-model";
+  const modelCatalog = [{ id: model, type: "language", tags: ["reasoning", "tool-use", "implicit-caching", "vision", "structured-output"] }];
+  const gateway = mockGateway((body, step) => {
+    if (step === 1) return toolResponse("load_image", {});
+  });
+  const agent = await createAgent(gateway, {
+    model,
+    modelCatalog,
+    tools: [{ name: "load_image", description: "Load the host image", inputSchema: { type: "object" }, execute: () => ({ type: "libfx.tool-result", text: "host image", images: [{ type: "image", data: pngData, mimeType: "image/png" }] }) }],
+  });
+  assert.equal((await runPrompt(agent, "load the image")).stopReason, "end_turn");
+  assert.equal(gateway.state.chatBodies.length, 2);
+  const followup = gateway.state.chatBodies[1];
+  assert.deepEqual(fileParts(followup), [{ type: "file", mediaType: "image/png", data: { type: "data", data: pngData } }]);
+  assert.doesNotMatch(JSON.stringify(followup.prompt), /Tool images were retained but not sent/);
+  assert.ok(!followup.tools.some((item) => item.name === "vision"), "a native image model is not offered the vision tool");
+  await agent.close();
+}
+
 // Rich host results share the existing data/count/frame limits. Referenced
 // overflow falls back to metadata; no-ref and malformed results remain errors.
 {
diff --git a/src/core/agent/runtime/gateway_step.zig b/src/core/agent/runtime/gateway_step.zig
index 19ae6234f..3be37ea01 100644
--- a/src/core/agent/runtime/gateway_step.zig
+++ b/src/core/agent/runtime/gateway_step.zig
@@ -1,6 +1,7 @@
 const std = @import("std");
 const agent_stream_provider = @import("../stream_provider.zig");
 const model_capabilities = @import("../../config/model_capabilities.zig");
+const image_route = @import("../../images/image_route.zig");
 const types = @import("../../shared/types.zig");
 const debug_trace = @import("../../shared/debug_trace.zig");
 const io_mod = @import("../../shared/io.zig");
@@ -261,68 +262,61 @@ pub const ToolImageProjection = struct {
     stripped: bool,
 };
 
-/// Projects stored tool images into the request only when the model accepts
-/// inline image input. Otherwise the images stay in the session image store
-/// and the tool message explains exactly why they were withheld and what the
-/// model can do instead, so the next step is never a dead end.
+/// Projects stored tool images into the request as `disposition` says, which
+/// the image route core decided (`src/core/images/image_route.zig`). Withheld
+/// images stay in the session image store, and each tool message that held
+/// one says why and what the model can do instead, so the next step is never
+/// a dead end.
 pub fn projectToolImageMessages(
     alloc: Allocator,
     messages: []const types.ChatMessage,
-    image_input_support: model_capabilities.ImageInputSupport,
-    vision_fallback_available: bool,
+    disposition: image_route.ToolImages,
     text_limit: usize,
 ) !ToolImageProjection {
-    if (image_input_support == .native) return .{ .messages = messages, .stripped = false };
-    const has_images = for (messages) |message| {
-        if (message.tool_result_memory) |memory| if (memory.tool_images.len > 0 or memory.tool_image_handle != null) break true;
-    } else false;
-    if (!has_images) return .{ .messages = messages, .stripped = false };
-    const notice: []const u8 = switch (image_input_support) {
-        .native => unreachable,
-        .non_native => if (vision_fallback_available)
-            "[Tool images were retained but not sent: this model receives image input through the vision tool, not inline. Call vision with the image file's local path to inspect it.]\n"
-        else
-            "[Tool images were retained but not sent: this model does not accept inline images and no vision fallback is available. Ask the user to attach the image directly or switch to a vision-capable model.]\n",
-        .unknown => "[Tool images were retained but not sent: fx could not confirm image input support for this model (the model is not listed in the model catalog, or the catalog is unavailable). This can recover later in the session, so a retry may succeed; otherwise ask the user to attach the image directly.]\n",
+    const notice: []const u8 = switch (disposition) {
+        .none, .attached => return .{ .messages = messages, .stripped = false },
+        .withheld_fallback => "[Tool images were retained but not sent: this model receives image input through the vision tool, not inline. Call vision with the image file's local path to inspect it.]\n",
+        .withheld_dead_end => "[Tool images were retained but not sent: this model does not accept inline images and no vision fallback is available. Ask the user to attach the image directly or switch to a vision-capable model.]\n",
+        .withheld_unknown => "[Tool images were retained but not sent: fx could not confirm image input support for this model (the model is not listed in the model catalog, or the catalog is unavailable). This can recover later in the session, so a retry may succeed; otherwise ask the user to attach the image directly.]\n",
     };
-    const projected = try alloc.dupe(types.ChatMessage, messages);
-    for (projected) |*message| {
-        if (message.tool_result_memory) |*memory| {
-            if (memory.tool_images.len == 0 and memory.tool_image_handle == null) continue;
-            memory.tool_images = &.{};
-            const content = message.content orelse "";
-            const keep = @import("../../config/context_limits.zig").utf8PrefixLength(content, text_limit -| notice.len);
-            memory.truncated = memory.truncated or keep < content.len;
-            message.content = try std.mem.concat(alloc, u8, &.{ notice[0..@min(notice.len, text_limit)], content[0..keep] });
-        }
+    var projected: ?[]types.ChatMessage = null;
+    for (messages, 0..) |message, index| {
+        var memory = message.tool_result_memory orelse continue;
+        if (memory.tool_images.len == 0 and memory.tool_image_handle == null) continue;
+        const out = projected orelse try alloc.dupe(types.ChatMessage, messages);
+        projected = out;
+        memory.tool_images = &.{};
+        const content = message.content orelse "";
+        const keep = @import("../../config/context_limits.zig").utf8PrefixLength(content, text_limit -| notice.len);
+        memory.truncated = memory.truncated or keep < content.len;
+        out[index].tool_result_memory = memory;
+        out[index].content = try std.mem.concat(alloc, u8, &.{ notice[0..@min(notice.len, text_limit)], content[0..keep] });
     }
-    return .{ .messages = projected, .stripped = true };
+    return .{ .messages = projected orelse messages, .stripped = projected != null };
 }
 
-test "projectToolImageMessages passes images through for native models" {
-    const alloc = std.testing.allocator;
-    const messages = [_]types.ChatMessage{.{
-        .role = .tool,
-        .content = "shot",
-        .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") },
-    }};
-    const projected = try projectToolImageMessages(alloc, &messages, .native, false, 1024);
+fn freeProjection(alloc: Allocator, projection: ToolImageProjection) void {
+    if (!projection.stripped) return;
+    for (projection.messages) |message| alloc.free(message.content.?);
+    alloc.free(projection.messages);
+}
+
+const shot_messages = [_]types.ChatMessage{.{
+    .role = .tool,
+    .content = "shot",
+    .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") },
+}};
+
+test "projectToolImageMessages passes images through when they are attached" {
+    const projected = try projectToolImageMessages(std.testing.allocator, &shot_messages, .attached, 1024);
     try std.testing.expect(!projected.stripped);
-    try std.testing.expect(projected.messages.ptr == (&messages).ptr);
+    try std.testing.expect(projected.messages.ptr == (&shot_messages).ptr);
 }
 
 test "projectToolImageMessages explains the vision fallback for non native models" {
     const alloc = std.testing.allocator;
-    const messages = [_]types.ChatMessage{.{
-        .role = .tool,
-        .content = "shot",
-        .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") },
-    }};
-    const projected = try projectToolImageMessages(alloc, &messages, .non_native, true, 1024);
-    defer {
-        for (projected.messages) |message| alloc.free(message.content.?);
-        alloc.free(projected.messages);
-    }
+    const projected = try projectToolImageMessages(alloc, &shot_messages, .withheld_fallback, 1024);
+    defer freeProjection(alloc, projected);
     try std.testing.expect(projected.stripped);
     const memory = projected.messages[0].tool_result_memory.?;
     try std.testing.expectEqual(@as(usize, 0), memory.tool_images.len);
@@ -332,16 +326,8 @@ test "projectToolImageMessages explains the vision fallback for non native model
 
 test "projectToolImageMessages tells the truth when the catalog is unavailable" {
     const alloc = std.testing.allocator;
-    const messages = [_]types.ChatMessage{.{
-        .role = .tool,
-        .content = "shot",
-        .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") },
-    }};
-    const projected = try projectToolImageMessages(alloc, &messages, .unknown, true, 1024);
-    defer {
-        for (projected.messages) |message| alloc.free(message.content.?);
-        alloc.free(projected.messages);
-    }
+    const projected = try projectToolImageMessages(alloc, &shot_messages, .withheld_unknown, 1024);
+    defer freeProjection(alloc, projected);
     try std.testing.expect(projected.stripped);
     const content = projected.messages[0].content.?;
     try std.testing.expect(std.mem.find(u8, content, "could not confirm image input support") != null);
@@ -350,30 +336,22 @@ test "projectToolImageMessages tells the truth when the catalog is unavailable"
 
 test "projectToolImageMessages names the dead end when no fallback exists" {
     const alloc = std.testing.allocator;
-    const messages = [_]types.ChatMessage{.{
-        .role = .tool,
-        .content = "shot",
-        .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") },
-    }};
-    const projected = try projectToolImageMessages(alloc, &messages, .non_native, false, 1024);
-    defer {
-        for (projected.messages) |message| alloc.free(message.content.?);
-        alloc.free(projected.messages);
-    }
+    const projected = try projectToolImageMessages(alloc, &shot_messages, .withheld_dead_end, 1024);
+    defer freeProjection(alloc, projected);
     try std.testing.expect(projected.stripped);
-    const content = projected.messages[0].content.?;
-    try std.testing.expect(std.mem.find(u8, content, "no vision fallback is available") != null);
+    try std.testing.expect(std.mem.find(u8, projected.messages[0].content.?, "no vision fallback is available") != null);
 }
 
 test "projectToolImageMessages leaves image free history untouched" {
-    const alloc = std.testing.allocator;
     const messages = [_]types.ChatMessage{.{
         .role = .tool,
         .content = "plain",
     }};
-    const projected = try projectToolImageMessages(alloc, &messages, .unknown, false, 1024);
-    try std.testing.expect(!projected.stripped);
-    try std.testing.expect(projected.messages.ptr == (&messages).ptr);
+    for ([_]image_route.ToolImages{ .none, .withheld_unknown }) |disposition| {
+        const projected = try projectToolImageMessages(std.testing.allocator, &messages, disposition, 1024);
+        try std.testing.expect(!projected.stripped);
+        try std.testing.expect(projected.messages.ptr == (&messages).ptr);
+    }
 }
 
 pub fn snapshotDynamicTools(alloc: Allocator, deps: *const @import("deps.zig").AgentRuntimeDeps, selected: *std.ArrayList(agent_stream_provider.DynamicFunctionTool)) ![]const agent_stream_provider.DynamicFunctionTool {
diff --git a/src/core/agent/runtime/orchestrator.zig b/src/core/agent/runtime/orchestrator.zig
index fa967e878..fb95a0456 100644
--- a/src/core/agent/runtime/orchestrator.zig
+++ b/src/core/agent/runtime/orchestrator.zig
@@ -54,6 +54,7 @@ const runtime_tool_contracts = @import("tool_contracts.zig");
 const runtime_gateway_step = @import("gateway_step.zig");
 const runtime_vision_contracts = @import("vision_contracts.zig");
 const image_attachments = @import("../../images/image_attachments.zig");
+const image_route = @import("../../images/image_route.zig");
 const image_data = @import("../../images/image_data.zig");
 const runtime_assistant_stream = @import("assistant_stream.zig");
 const runtime_tool_presentation = @import("tool_presentation.zig");
@@ -6183,98 +6184,42 @@ fn buildToolExecutionRootUserContext(
     );
 }
 
-const ImageRoute = enum {
-    native,
-    fallback,
-    unavailable,
-};
-
-const VisionPolicy = struct {
-    route: ImageRoute,
-    mode: runtime_gateway_step.VisionToolMode,
-};
-
-fn visionPolicy(
-    image_input_support: model_capabilities.ImageInputSupport,
-    fallback_available: bool,
-    tool_registered: bool,
-    pending_images: bool,
-) VisionPolicy {
-    return switch (image_input_support) {
-        .native => .{ .route = .native, .mode = .unavailable },
-        .unknown => .{ .route = .unavailable, .mode = .unavailable },
-        .non_native => if (!fallback_available or !tool_registered)
-            .{ .route = .unavailable, .mode = .unavailable }
-        else
-            .{
-                .route = .fallback,
-                .mode = if (pending_images) .required else .optional,
-            },
+/// The vision tool mode the request offers, for the mode the image route chose.
+fn visionToolMode(mode: image_route.VisionMode) runtime_gateway_step.VisionToolMode {
+    return switch (mode) {
+        .unavailable => .unavailable,
+        .optional => .optional,
+        .required => .required,
     };
 }
 
-test "vision policy keeps image route and tool visibility coherent" {
-    const cases = [_]struct {
-        image_input_support: model_capabilities.ImageInputSupport,
-        fallback_available: bool,
-        tool_registered: bool,
-        pending_images: bool,
-        expected_route: ImageRoute,
-        expected_mode: runtime_gateway_step.VisionToolMode,
-    }{
-        .{ .image_input_support = .native, .fallback_available = true, .tool_registered = true, .pending_images = true, .expected_route = .native, .expected_mode = .unavailable },
-        .{ .image_input_support = .native, .fallback_available = false, .tool_registered = false, .pending_images = false, .expected_route = .native, .expected_mode = .unavailable },
-        .{ .image_input_support = .non_native, .fallback_available = true, .tool_registered = true, .pending_images = true, .expected_route = .fallback, .expected_mode = .required },
-        .{ .image_input_support = .non_native, .fallback_available = true, .tool_registered = true, .pending_images = false, .expected_route = .fallback, .expected_mode = .optional },
-        .{ .image_input_support = .non_native, .fallback_available = false, .tool_registered = true, .pending_images = true, .expected_route = .unavailable, .expected_mode = .unavailable },
-        .{ .image_input_support = .non_native, .fallback_available = true, .tool_registered = false, .pending_images = false, .expected_route = .unavailable, .expected_mode = .unavailable },
-        .{ .image_input_support = .unknown, .fallback_available = true, .tool_registered = true, .pending_images = true, .expected_route = .unavailable, .expected_mode = .unavailable },
-    };
-
-    for (cases) |case| {
-        const policy = visionPolicy(
-            case.image_input_support,
-            case.fallback_available,
-            case.tool_registered,
-            case.pending_images,
-        );
-        try std.testing.expectEqual(case.expected_route, policy.route);
-        try std.testing.expectEqual(case.expected_mode, policy.mode);
-        try std.testing.expect((policy.route == .fallback) == (policy.mode != .unavailable));
-    }
-
-    const support_values = [_]model_capabilities.ImageInputSupport{
-        .unknown,
-        .non_native,
-        .native,
-    };
-    const boolean_values = [_]bool{ false, true };
-    for (support_values) |support| {
-        for (boolean_values) |fallback_available| {
-            for (boolean_values) |tool_registered| {
-                for (boolean_values) |pending_images| {
-                    const policy = visionPolicy(
-                        support,
-                        fallback_available,
-                        tool_registered,
-                        pending_images,
-                    );
-                    try std.testing.expect((policy.route == .fallback) == (policy.mode != .unavailable));
-                    if (support == .native) {
-                        try std.testing.expectEqual(ImageRoute.native, policy.route);
-                        try std.testing.expectEqual(runtime_gateway_step.VisionToolMode.unavailable, policy.mode);
-                    }
-                    if (support == .unknown) {
-                        try std.testing.expectEqual(ImageRoute.unavailable, policy.route);
-                        try std.testing.expectEqual(runtime_gateway_step.VisionToolMode.unavailable, policy.mode);
-                    }
-                    if (!fallback_available or !tool_registered) {
-                        try std.testing.expect(policy.mode == .unavailable or support == .native);
-                    }
-                }
-            }
+/// Whether a tool image in `messages` still reaches the request: one the
+/// session keeps, or a handle to materialize. `image_attachments.withholdDroppedImages`
+/// turns the others into notes.
+fn requestHasToolImages(messages: []const ChatMessage) bool {
+    for (messages) |message| {
+        const memory = message.tool_result_memory orelse continue;
+        if (memory.tool_image_handle != null) return true;
+        for (memory.tool_images) |image| {
+            if (!image.droppedFromSession()) return true;
         }
     }
+    return false;
+}
+
+test "requestHasToolImages ignores images the session dropped" {
+    var kept_bytes = "png".*;
+    var mime = "image/png".*;
+    const kept = [_]types.ToolImage{.{ .data = &kept_bytes, .mime_type = &mime }};
+    const dropped = [_]types.ToolImage{.{ .data = &.{}, .mime_type = &mime, .name = @as([64]u8, @splat('0')) }};
+    const with_kept = [_]ChatMessage{.{ .role = .tool, .content = "a", .tool_result_memory = .{ .tool_images = @constCast(&kept) } }};
+    const with_dropped = [_]ChatMessage{.{ .role = .tool, .content = "b", .tool_result_memory = .{ .tool_images = @constCast(&dropped) } }};
+    const with_handle = [_]ChatMessage{.{ .role = .tool, .content = "c", .tool_result_memory = .{ .tool_image_handle = @constCast("image-result-x") } }};
+    const plain = [_]ChatMessage{.{ .role = .tool, .content = "d" }};
+    try std.testing.expect(requestHasToolImages(&with_kept));
+    try std.testing.expect(!requestHasToolImages(&with_dropped));
+    try std.testing.expect(requestHasToolImages(&with_handle));
+    try std.testing.expect(!requestHasToolImages(&plain));
 }
 
 fn buildProviderPromptForCompactionWindow(
@@ -6941,7 +6886,9 @@ fn processQueuedPromptLoop(
     agent: *runtime_agent.Agent,
 ) !void {
     var request_capabilities = initial_request_capabilities;
-    var tool_image_capabilities_resolved = false;
+    // The image route core's turn state. This loop is its shell: it runs each
+    // effect `image_route.step` returns and feeds the result back.
+    var image_route_state = image_route.step(.{}, .{ .turn_started = request_capabilities.image_input_support }).state;
     var stable_prefix = stable_prefix_ptr.*;
     defer stable_prefix_ptr.* = stable_prefix;
     const history_messages = history_messages_ptr.*;
@@ -7077,7 +7024,6 @@ fn processQueuedPromptLoop(
         selected_fast_mode;
     var fast_unavailable_notified = false;
     var ultrafast_unconfirmed_notified = false;
-    var tool_image_strip_notified = false;
     // Attachment pixel sizes probed during this turn, so each step does not
     // reread every attachment snapshot. Entries live in the turn arena.
     var attachment_dimensions: image_attachments.AttachmentDimensionCache = .empty;
@@ -7370,41 +7316,81 @@ fn processQueuedPromptLoop(
             gateway_messages = provider_prompt.messages;
             current_user_message_index = provider_prompt.current_user_index;
             debug_trace.eventf("agent", "before_provider_preflight", step_ctx, "model={s} messages={d}", .{ gateway_model, gateway_instructions.items.len + gateway_messages.items.len });
-            const vision_policy = visionPolicy(
-                request_capabilities.image_input_support,
-                config.provider_capabilities.vision_fallback,
-                deps.tool_registry.lookup("vision") != null,
-                pending_image_ids.len > 0,
-            );
-            const vision_route: runtime_vision_contracts.VisionRoute = if (vision_policy.route == .fallback)
-                .text_only
-            else
-                .native_images;
-            const vision_mode = vision_policy.mode;
-            debug_trace.eventf(
-                "agent",
-                "vision_policy",
-                step_ctx,
-                "model={s} image_support={s} route={s} mode={s} pending_images={d}",
-                .{
-                    gateway_model,
-                    @tagName(request_capabilities.image_input_support),
-                    @tagName(vision_policy.route),
-                    @tagName(vision_mode),
-                    pending_image_ids.len,
-                },
-            );
             try appendRecoveryConversationContext(
                 overlay_arena,
                 &gateway_messages,
                 recovery_strategy,
             );
             const recovery_source_messages = gateway_messages.items;
+            // One image decision per request, read from one capability
+            // snapshot: the core asks for capabilities first when it must,
+            // and every route, mode, and tool image choice below follows the
+            // decision it returns (`tests/tla/image_route/spec/ImageRoute.tla`
+            // OneSnapshot).
+            var image_event: image_route.Event = .{ .request_ready = .{
+                .user_images = job.authorized_image_catalog.len > 0 or job.images.len > 0,
+                .pending_images = pending_image_ids.len > 0,
+                .tool_images = requestHasToolImages(recovery_source_messages),
+                .fallback = config.provider_capabilities.vision_fallback and deps.tool_registry.lookup("vision") != null,
+                .catalog_down = if (deps.model_catalog_unavailable) |unavailable| unavailable(deps.ctx) else false,
+            } };
+            var image_decision: ?image_route.Decision = null;
+            var image_failure: ?image_route.FailReason = null;
+            var notify_catalog_down = false;
+            // Ends: the core asks for capabilities at most once per turn, and
+            // its reply never asks again (ImageRoute.tla ResolveOncePerTurn).
+            while (true) {
+                const image_out = image_route.step(image_route_state, image_event);
+                image_route_state = image_out.state;
+                var reply: ?image_route.Event = null;
+                for (image_out.effects()) |effect| switch (effect) {
+                    .resolve_capabilities => {
+                        request_capabilities = try deps.resolve_model_capabilities(deps.ctx, overlay_arena, gateway_model);
+                        reply = .{ .capabilities_resolved = request_capabilities.image_input_support };
+                    },
+                    .notify_catalog_down => notify_catalog_down = true,
+                    .send => |chosen| image_decision = chosen,
+                    .fail => |reason| image_failure = reason,
+                };
+                image_event = reply orelse break;
+            }
+            if (image_failure) |reason| switch (reason) {
+                .capability_unknown => {
+                    diagnostics.recordModelCatalogEvent(true, .image_gate, "model={s} image_support=unknown err=ModelImageCapabilityUnavailable", .{gateway_model});
+                    return error.ModelImageCapabilityUnavailable;
+                },
+                .no_native_image => {
+                    diagnostics.recordModelCatalogEvent(true, .image_gate, "model={s} image_support=non_native err=SubscriptionNativeImageUnavailable", .{gateway_model});
+                    return error.SubscriptionNativeImageUnavailable;
+                },
+            };
+            // Each request ends in exactly one send or fail (ImageRoute.tla
+            // Answered), so a missing decision is a bug in the core.
+            const image_choice = image_decision.?;
+            const vision_route: runtime_vision_contracts.VisionRoute = if (image_choice.route == .fallback)
+                .text_only
+            else
+                .native_images;
+            const vision_mode = visionToolMode(image_choice.mode);
+            debug_trace.eventf(
+                "agent",
+                "vision_policy",
+                step_ctx,
+                "model={s} image_support={s} route={s} mode={s} pending_images={d} tool_images={s}",
+                .{
+                    gateway_model,
+                    @tagName(image_route_state.support),
+                    @tagName(image_choice.route),
+                    @tagName(image_choice.mode),
+                    pending_image_ids.len,
+                    @tagName(image_choice.tool_images),
+                },
+            );
             const projected_request_messages = blk: {
                 if (job.authorized_image_catalog.len == 0 and job.images.len == 0) {
                     break :blk recovery_source_messages;
                 }
-                break :blk switch (vision_policy.route) {
+                break :blk switch (image_choice.route) {
                     .native => try runtime_vision_contracts.project_native_messages(
                         overlay_arena,
                         recovery_source_messages,
@@ -7423,20 +7409,11 @@ fn processQueuedPromptLoop(
                             job.authorized_image_catalog,
                         );
                     },
-                    .unavailable => switch (request_capabilities.image_input_support) {
-                        .unknown => {
-                            diagnostics.recordModelCatalogEvent(true, .image_gate, "model={s} image_support=unknown err=ModelImageCapabilityUnavailable", .{gateway_model});
-                            return error.ModelImageCapabilityUnavailable;
-                        },
-                        .non_native => {
-                            diagnostics.recordModelCatalogEvent(true, .image_gate, "model={s} image_support=non_native err=SubscriptionNativeImageUnavailable", .{gateway_model});
-                            return error.SubscriptionNativeImageUnavailable;
-                        },
-                        .native => unreachable,
-                    },
+                    // The core fails a request whose user images have no route.
+                    .unavailable => unreachable,
                 };
             };
-            if (vision_policy.route == .native and projected_request_messages.len < recovery_source_messages.len) {
+            if (image_choice.route == .native and projected_request_messages.len < recovery_source_messages.len) {
                 debug_trace.logf("history", "native_vision_history_projected removed_messages={d} reason=native_image_input", .{
                     recovery_source_messages.len - projected_request_messages.len,
                 });
@@ -7483,16 +7460,7 @@ fn processQueuedPromptLoop(
                 read_tool_result_request_eligible,
                 subagent_request_messages,
             ));
-            if (!tool_image_capabilities_resolved and request_capabilities.image_input_support == .unknown) {
-                for (result_request_messages) |message| {
-                    const memory = message.tool_result_memory orelse continue;
-                    if (memory.tool_images.len == 0 and memory.tool_image_handle == null) continue;
-                    request_capabilities = try deps.resolve_model_capabilities(deps.ctx, overlay_arena, gateway_model);
-                    tool_image_capabilities_resolved = true;
-                    break;
-                }
-            }
-            const materialized_messages = if (request_capabilities.image_input_support == .native) native: {
+            const materialized_messages = if (image_choice.route == .native) native: {
                 const loaded_messages = try runtime_execution_memory.materializeToolImages(overlay_arena, config, result_request_messages);
                 const max_dimension = image_data.requestMaxDimension(image_data.countRequestImages(loaded_messages));
                 const safe_tool_messages = try runtime_execution_memory.withholdRequestToolImages(overlay_arena, loaded_messages, max_dimension, config.max_tool_result_bytes);
@@ -7506,7 +7474,7 @@ fn processQueuedPromptLoop(
                 );
                 break :native projection.messages;
             } else result_request_messages;
-            const image_projection = try runtime_gateway_step.projectToolImageMessages(overlay_arena, materialized_messages, request_capabilities.image_input_support, vision_policy.route == .fallback, config.max_tool_result_bytes);
+            const image_projection = try runtime_gateway_step.projectToolImageMessages(overlay_arena, materialized_messages, image_choice.tool_images, config.max_tool_result_bytes);
             // Saved turns keep steering without its envelope; the model gets it
             // back as the live update it saw when the turn took it.
             const steering_messages = try runtime_execution_memory.rewrapRestoredSteering(overlay_arena, image_projection.messages);
@@ -7518,15 +7486,11 @@ fn processQueuedPromptLoop(
                 debug_trace.eventf("history", "assistant_tail_continued", step_ctx, "messages={d}", .{located_messages.len});
             }
             // Tool images withheld because the catalog could not confirm image
-            // input are invisible in the transcript otherwise. Tell the user
-            // once per turn, and only when the catalog itself is known to be
-            // down; a confirmed model without image input relies on the
-            // model-facing notice instead.
-            if (image_projection.stripped and !tool_image_strip_notified and
-                request_capabilities.image_input_support == .unknown and
-                deps.model_catalog_unavailable != null and deps.model_catalog_unavailable.?(deps.ctx))
-            {
-                tool_image_strip_notified = true;
+            // input are invisible in the transcript otherwise. The core asks
+            // to tell the user once per turn, and only when the catalog itself
+            // is known to be down; a confirmed model without image input
+            // relies on the model-facing notice instead.
+            if (notify_catalog_down) {
                 try deps.push_text(deps.ctx, .{ .operational = "Images from tools aren't reaching the model right now because image support couldn't be confirmed (model catalog unavailable). fx will retry automatically as the catalog recovers." });
                 try deps.push_text(deps.ctx, .{ .operational = "\n" });
             }
diff --git a/src/core/agent/runtime/tests/gateway_flow.zig b/src/core/agent/runtime/tests/gateway_flow.zig
index 6f23a58e4..b776f5ef2 100644
--- a/src/core/agent/runtime/tests/gateway_flow.zig
+++ b/src/core/agent/runtime/tests/gateway_flow.zig
@@ -2505,7 +2505,7 @@ test "processQueuedPrompt never uses the vision fallback for Codex" {
     try std.testing.expectEqual(@as(usize, 0), gateway.request_bodies.items.len);
 }
 
-test "processQueuedPrompt routes images natively only when vision and file input are both supported" {
+test "processQueuedPrompt routes images natively whenever the catalog lists vision" {
     const alloc = std.testing.allocator;
     const cases = [_]struct {
         label: []const u8,
@@ -2514,7 +2514,7 @@ test "processQueuedPrompt routes images natively only when vision and file input
         expect_native: bool,
     }{
         .{ .label = "vision-file", .supports_vision = true, .supports_file_input = true, .expect_native = true },
-        .{ .label = "vision-no-file", .supports_vision = true, .supports_file_input = false, .expect_native = false },
+        .{ .label = "vision-no-file", .supports_vision = true, .supports_file_input = false, .expect_native = true },
         .{ .label = "file-no-vision", .supports_vision = false, .supports_file_input = true, .expect_native = false },
         .{ .label = "neither", .supports_vision = false, .supports_file_input = false, .expect_native = false },
     };
@@ -2532,7 +2532,10 @@ test "processQueuedPrompt routes images natively only when vision and file input
         const capability_overrides = [_]ModelCapabilityOverride{.{
             .model = model,
             .capabilities = .{
-                .image_input_support = if (entry.expect_native) .native else .non_native,
+                .image_input_support = model_capabilities.mergeCapabilities(.{}, .{
+                    .supports_vision = entry.supports_vision,
+                    .supports_file_input = entry.supports_file_input,
+                }).image_input_support,
                 .supports_vision = entry.supports_vision,
                 .supports_file_input = entry.supports_file_input,
             },
diff --git a/src/core/config/model_capabilities.zig b/src/core/config/model_capabilities.zig
index 329f438b6..ac9c47725 100644
--- a/src/core/config/model_capabilities.zig
+++ b/src/core/config/model_capabilities.zig
@@ -1,6 +1,7 @@
 const std = @import("std");
 const types = @import("../shared/types.zig");
 const model_provider = @import("model_provider.zig");
+const image_route = @import("../images/image_route.zig");
 
 pub const ResolvedProviderOptions = struct {
     reasoning: ?types.ReasoningEffort = null,
@@ -33,11 +34,7 @@ pub const ReasoningEffortOptions = struct {
     }
 };
 
-pub const ImageInputSupport = enum {
-    unknown,
-    non_native,
-    native,
-};
+pub const ImageInputSupport = image_route.Support;
 
 pub const GatewayMetadata = struct {
     supports_reasoning: bool = false,
@@ -97,10 +94,10 @@ pub fn mergeCapabilities(capabilities_value: Capabilities, gateway_metadata: ?Ga
         capabilities.supports_tool_use = metadata.supports_tool_use;
         capabilities.supports_vision = metadata.supports_vision;
         capabilities.supports_file_input = metadata.supports_file_input;
-        capabilities.image_input_support = if (metadata.supports_vision and metadata.supports_file_input)
-            .native
-        else
-            .non_native;
+        capabilities.image_input_support = image_route.supportFromCatalog(.{ .listed = .{
+            .vision = metadata.supports_vision,
+            .file_input = metadata.supports_file_input,
+        } });
         capabilities.supports_web_search = metadata.supports_web_search;
         capabilities.supports_explicit_caching = metadata.supports_explicit_caching;
         capabilities.supports_implicit_caching = metadata.supports_implicit_caching;
@@ -302,17 +299,19 @@ test "image input support distinguishes unknown native and non native capability
         capabilitiesForModel("provider/unknown").image_input_support,
     );
 
-    const native = mergeCapabilities(.{}, .{
-        .supports_vision = true,
-        .supports_file_input = true,
-    });
-    try std.testing.expectEqual(ImageInputSupport.native, native.image_input_support);
+    for ([_]bool{ false, true }) |file_input| {
+        const native = mergeCapabilities(.{}, .{
+            .supports_vision = true,
+            .supports_file_input = file_input,
+        });
+        try std.testing.expectEqual(ImageInputSupport.native, native.image_input_support);
 
-    const non_native = mergeCapabilities(.{}, .{
-        .supports_vision = true,
-        .supports_file_input = false,
-    });
-    try std.testing.expectEqual(ImageInputSupport.non_native, non_native.image_input_support);
+        const non_native = mergeCapabilities(.{}, .{
+            .supports_vision = false,
+            .supports_file_input = file_input,
+        });
+        try std.testing.expectEqual(ImageInputSupport.non_native, non_native.image_input_support);
+    }
 }
 
 test "reasoning effort picker helpers prepend default and preserve Gateway order" {
diff --git a/src/core/images/image_route.zig b/src/core/images/image_route.zig
new file mode 100644
index 000000000..5e9f56b3c
--- /dev/null
+++ b/src/core/images/image_route.zig
@@ -0,0 +1,369 @@
+//! How images reach the model on one request.
+//!
+//! `step` is the whole decision: given the turn's state and one event, it
+//! returns the next state and the effects to run. It performs no I/O and reads
+//! no clock, environment, or global. The orchestrator is its shell: it runs
+//! each effect and feeds the result back as an event.
+//!
+//! `tests/tla/image_route/spec/ImageRoute.tla` models `step` action for
+//! action, and `abstract` maps a state onto that model's variables. The laws
+//! below are the model's properties; `tests/tla/image_route/design/DESIGN.md`
+//! lists where each one is enforced.
+//!
+//! This file imports only `std`, so the JSON-lines harness in
+//! `tests/tla/drivers/image_route/` can build it on its own.
+const std = @import("std");
+
+/// Whether the selected model takes images inline.
+pub const Support = enum {
+    /// The catalog was unavailable or did not list the model.
+    unknown,
+    /// The catalog lists the model without vision.
+    non_native,
+    /// The catalog lists the model with vision.
+    native,
+};
+
+/// What the model catalog said about one model.
+pub const CatalogView = union(enum) {
+    /// The catalog could not be read: unreachable, refused, or malformed.
+    down,
+    /// The catalog was read and does not list the model.
+    missing,
+    listed: Tags,
+
+    pub const Tags = struct {
+        vision: bool,
+        file_input: bool,
+    };
+};
+
+/// Images reach the model inline exactly when the catalog lists `vision`.
+///
+/// fx sends every image, user or tool, in an AI SDK `file` part with an
+/// `image/*` media type, which is the AI Gateway's vision input. The
+/// catalog's `file-input` tag covers documents such as PDFs and says nothing
+/// about images, so it plays no part here.
+pub fn supportFromCatalog(view: CatalogView) Support {
+    return switch (view) {
+        .down, .missing => .unknown,
+        .listed => |tags| if (tags.vision) .native else .non_native,
+    };
+}
+
+/// Where the turn's user images go.
+pub const Route = enum {
+    /// Inline, as file parts.
+    native,
+    /// Through the vision tool, as text.
+    fallback,
+    /// Nowhere: a request with user images fails.
+    unavailable,
+};
+
+/// How the request offers the vision tool.
+pub const VisionMode = enum {
+    unavailable,
+    optional,
+    required,
+};
+
+/// What happens to the tool images in the request's history.
+pub const ToolImages = enum {
+    /// The history has none.
+    none,
+    /// They go inline.
+    attached,
+    /// Withheld; the model is told to call the vision tool.
+    withheld_fallback,
+    /// Withheld; the model is told no image path exists.
+    withheld_dead_end,
+    /// Withheld; the model is told support could not be confirmed.
+    withheld_unknown,
+};
+
+pub const FailReason = enum {
+    /// User images, and the catalog could not confirm image input.
+    capability_unknown,
+    /// User images, a model without vision, and no vision tool.
+    no_native_image,
+};
+
+/// What the shell knows about the request it is about to send. Only flags:
+/// image bytes never enter the core.
+pub const Request = struct {
+    /// The turn carries user images, attached now or authorized earlier.
+    user_images: bool,
+    /// Some of those images still wait for the model's first look.
+    pending_images: bool,
+    /// The request history holds tool images the session still has.
+    tool_images: bool,
+    /// The vision tool is configured and registered.
+    fallback: bool,
+    /// The catalog is known to be unreachable right now.
+    catalog_down: bool,
+};
+
+pub const State = struct {
+    /// The turn's one capability snapshot. Every decision reads it.
+    support: Support = .unknown,
+    /// This turn already asked for capabilities.
+    resolved: bool = false,
+    /// This turn already told the user the catalog is down.
+    notified: bool = false,
+    /// The request waiting for the capability reply.
+    pending: ?Request = null,
+};
+
+pub const Event = union(enum) {
+    /// A turn starts with the capabilities the shell holds. It also ends
+    /// whatever the previous turn left: a reply still owed is dropped.
+    turn_started: Support,
+    /// The shell has built a request's history and is about to send it.
+    request_ready: Request,
+    /// The reply to `resolve_capabilities`.
+    capabilities_resolved: Support,
+};
+
+/// One request's image handling, all read from one support value.
+pub const Decision = struct {
+    route: Route,
+    mode: VisionMode,
+    tool_images: ToolImages,
+};
+
+pub const Effect = union(enum) {
+    /// Ask the catalog again, then send `capabilities_resolved`.
+    resolve_capabilities,
+    /// Tell the user once that tool images wait on the catalog.
+    notify_catalog_down,
+    /// Send the request as decided.
+    send: Decision,
+    /// Fail the turn without sending.
+    fail: FailReason,
+};
+
+pub const max_effects = 2;
+
+pub const Output = struct {
+    state: State,
+    buffer: [max_effects]Effect = undefined,
+    len: usize = 0,
+
+    pub fn effects(self: *const Output) []const Effect {
+        return self.buffer[0..self.len];
+    }
+};
+
+pub fn step(state: State, event: Event) Output {
+    return switch (event) {
+        .turn_started => |support| .{ .state = .{ .support = support } },
+        .request_ready => |request| onRequest(state, request),
+        .capabilities_resolved => |support| onResolved(state, support),
+    };
+}
+
+fn onRequest(state: State, request: Request) Output {
+    if (state.pending != null) {
+        // Delivered while a reply is owed: the reply answers the newest
+        // request, and nothing runs twice.
+        var next = state;
+        next.pending = request;
+        return .{ .state = next };
+    }
+    if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) {
+        var next = state;
+        next.resolved = true;
+        next.pending = request;
+        return withEffects(next, &.{.resolve_capabilities});
+    }
+    return decide(state, request);
+}
+
+fn onResolved(state: State, support: Support) Output {
+    // A reply nothing waits for, stale or duplicated, changes nothing.
+    const request = state.pending orelse return .{ .state = state };
+    var next = state;
+    next.support = support;
+    next.pending = null;
+    return decide(next, request);
+}
+
+fn decide(state: State, request: Request) Output {
+    const chosen = decision(state.support, request);
+    if (request.user_images and chosen.route == .unavailable) {
+        const reason: FailReason = if (state.support == .unknown) .capability_unknown else .no_native_image;
+        return withEffects(state, &.{.{ .fail = reason }});
+    }
+    if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) {
+        var next = state;
+        next.notified = true;
+        return withEffects(next, &.{ .notify_catalog_down, .{ .send = chosen } });
+    }
+    return withEffects(state, &.{.{ .send = chosen }});
+}
+
+/// The image handling `support` implies for `request`.
+pub fn decision(support: Support, request: Request) Decision {
+    const route: Route = switch (support) {
+        .native => .native,
+        .unknown => .unavailable,
+        .non_native => if (request.fallback) .fallback else .unavailable,
+    };
+    const mode: VisionMode = if (route != .fallback)
+        .unavailable
+    else if (request.pending_images)
+        .required
+    else
+        .optional;
+    const tool_images: ToolImages = if (!request.tool_images) .none else switch (support) {
+        .native => .attached,
+        .unknown => .withheld_unknown,
+        .non_native => if (route == .fallback) .withheld_fallback else .withheld_dead_end,
+    };
+    return .{ .route = route, .mode = mode, .tool_images = tool_images };
+}
+
+fn withEffects(state: State, list: []const Effect) Output {
+    var out: Output = .{ .state = state, .len = list.len };
+    @memcpy(out.buffer[0..list.len], list);
+    return out;
+}
+
+/// The spec's view of a state: `support`, `resolved`, `notified`, and
+/// `pending` as a sequence of at most one request.
+pub const Abstract = struct {
+    support: Support,
+    resolved: bool,
+    notified: bool,
+    pending: []const Request,
+};
+
+/// Maps `state` onto the variables of `ImageRoute.tla`. The result borrows
+/// `state`.
+pub fn abstract(state: *const State) Abstract {
+    return .{
+        .support = state.support,
+        .resolved = state.resolved,
+        .notified = state.notified,
+        .pending = if (state.pending) |*request| request[0..1] else &.{},
+    };
+}
+
+fn eachRequest(comptime body: anytype) !void {
+    for (0..32) |bits| {
+        const request: Request = .{
+            .user_images = bits & 1 != 0,
+            .pending_images = bits & 2 != 0,
+            .tool_images = bits & 4 != 0,
+            .fallback = bits & 8 != 0,
+            .catalog_down = bits & 16 != 0,
+        };
+        if (request.pending_images and !request.user_images) continue;
+        try body(request);
+    }
+}
+
+const all_support = [_]Support{ .unknown, .non_native, .native };
+
+test "a catalog that lists vision makes image input native with or without file input" {
+    for ([_]bool{ false, true }) |file_input| {
+        try std.testing.expectEqual(Support.native, supportFromCatalog(.{ .listed = .{ .vision = true, .file_input = file_input } }));
+        try std.testing.expectEqual(Support.non_native, supportFromCatalog(.{ .listed = .{ .vision = false, .file_input = file_input } }));
+    }
+    try std.testing.expectEqual(Support.unknown, supportFromCatalog(.down));
+    try std.testing.expectEqual(Support.unknown, supportFromCatalog(.missing));
+}
+
+test "every decision reads one support value" {
+    try eachRequest(struct {
+        fn check(request: Request) !void {
+            for (all_support) |support| {
+                const chosen = decision(support, request);
+                try std.testing.expectEqual(chosen.route == .native, support == .native);
+                try std.testing.expectEqual(chosen.route == .fallback, chosen.mode != .unavailable);
+                try std.testing.expectEqual(chosen.tool_images == .none, !request.tool_images);
+                if (chosen.tool_images == .attached) try std.testing.expectEqual(Support.native, support);
+                if (chosen.tool_images == .withheld_unknown) try std.testing.expectEqual(Support.unknown, support);
+                if (chosen.tool_images == .withheld_fallback) try std.testing.expectEqual(Route.fallback, chosen.route);
+                if (chosen.tool_images == .withheld_dead_end) try std.testing.expect(support == .non_native and chosen.route == .unavailable);
+                if (chosen.route == .fallback) try std.testing.expectEqual(request.pending_images, chosen.mode == .required);
+            }
+        }
+    }.check);
+}
+
+test "a turn asks for capabilities at most once and answers the request it held" {
+    try eachRequest(struct {
+        fn check(request: Request) !void {
+            const started = step(.{}, .{ .turn_started = .unknown });
+            const first = step(started.state, .{ .request_ready = request });
+            if (!request.user_images and !request.tool_images) {
+                try std.testing.expectEqual(@as(usize, 1), first.len);
+                try std.testing.expect(first.effects()[0] == .send);
+                return;
+            }
+            try std.testing.expectEqual(@as(usize, 1), first.len);
+            try std.testing.expect(first.effects()[0] == .resolve_capabilities);
+            // A duplicate delivery while the reply is owed runs nothing.
+            const duplicate = step(first.state, .{ .request_ready = request });
+            try std.testing.expectEqual(@as(usize, 0), duplicate.len);
+            const answered = step(duplicate.state, .{ .capabilities_resolved = .unknown });
+            try std.testing.expect(answered.state.pending == null);
+            for (answered.effects()) |effect| try std.testing.expect(effect != .resolve_capabilities);
+            // A stale reply changes nothing.
+            const stale = step(answered.state, .{ .capabilities_resolved = .native });
+            try std.testing.expectEqual(@as(usize, 0), stale.len);
+            try std.testing.expectEqualDeep(answered.state, stale.state);
+            // The next request in the turn does not ask again.
+            const again = step(stale.state, .{ .request_ready = request });
+            for (again.effects()) |effect| try std.testing.expect(effect != .resolve_capabilities);
+        }
+    }.check);
+}
+
+test "the catalog-down notice reaches the user once per turn" {
+    const request: Request = .{ .user_images = false, .pending_images = false, .tool_images = true, .fallback = true, .catalog_down = true };
+    var state = step(.{}, .{ .turn_started = .unknown }).state;
+    var notices: usize = 0;
+    for (0..3) |_| {
+        var out = step(state, .{ .request_ready = request });
+        if (out.len == 1 and out.effects()[0] == .resolve_capabilities) out = step(out.state, .{ .capabilities_resolved = .unknown });
+        for (out.effects()) |effect| {
+            if (effect == .notify_catalog_down) notices += 1;
+        }
+        state = out.state;
+    }
+    try std.testing.expectEqual(@as(usize, 1), notices);
+    const next_turn = step(state, .{ .turn_started = .unknown });
+    try std.testing.expect(!next_turn.state.notified and !next_turn.state.resolved);
+}
+
+test "user images without a route fail the request and never send" {
+    for (all_support) |support| {
+        const request: Request = .{ .user_images = true, .pending_images = true, .tool_images = true, .fallback = false, .catalog_down = false };
+        const out = step(.{ .support = support, .resolved = true }, .{ .request_ready = request });
+        try std.testing.expectEqual(@as(usize, 1), out.len);
+        switch (support) {
+            .native => try std.testing.expect(out.effects()[0] == .send),
+            .unknown => try std.testing.expectEqual(Effect{ .fail = .capability_unknown }, out.effects()[0]),
+            .non_native => try std.testing.expectEqual(Effect{ .fail = .no_native_image }, out.effects()[0]),
+        }
+    }
+}
+
+test "abstract maps the pending request onto a sequence of at most one" {
+    const request: Request = .{ .user_images = true, .pending_images = false, .tool_images = false, .fallback = true, .catalog_down = false };
+    const idle: State = .{};
+    try std.testing.expectEqual(@as(usize, 0), abstract(&idle).pending.len);
+    const waiting: State = .{ .resolved = true, .pending = request };
+    const view = abstract(&waiting);
+    try std.testing.expectEqual(@as(usize, 1), view.pending.len);
+    try std.testing.expectEqualDeep(request, view.pending[0]);
+}
+
+test "requests carry flags, not image bytes" {
+    inline for (@typeInfo(Request).@"struct".field_types) |field_type| {
+        try std.testing.expect(field_type == bool);
+    }
+}
diff --git a/tests/e2e/file-tool-paths.test.ts b/tests/e2e/file-tool-paths.test.ts
index 52f6436b6..5121ac97f 100644
--- a/tests/e2e/file-tool-paths.test.ts
+++ b/tests/e2e/file-tool-paths.test.ts
@@ -349,11 +349,28 @@ async function runTerminalToolScenario(args: {
 }
 
 describe("filesystem path handling", () => {
-  for (const supportsImages of [true, false]) {
+  const readImageCases = [
+    {
+      name: "read_file attaches a workspace image inline for a vision model",
+      modelTags: ["tool-use", "vision", "file-input"],
+      inline: true,
+    },
+    {
+      // The catalog lists the default model, spacexai/grok-4.7, with vision
+      // and without file-input, which covers documents rather than images.
+      name: "read_file attaches a workspace image inline for a vision model without file input",
+      modelTags: ["reasoning", "tool-use", "implicit-caching", "vision", "structured-output"],
+      inline: true,
+    },
+    {
+      name: "read_file image is withheld with guidance for a text-only model",
+      modelTags: ["tool-use"],
+      inline: false,
+    },
+  ];
+  for (const imageCase of readImageCases) {
     test(
-      supportsImages
-        ? "read_file attaches a workspace image inline for a vision model"
-        : "read_file image is withheld with guidance for a text-only model",
+      imageCase.name,
       async () => {
         const root = createIsolatedRoot();
         const pngBase64 =
@@ -363,11 +380,7 @@ describe("filesystem path handling", () => {
             toolCall("read_image_1", "read_file", { path: "pixel.png" }),
             finalText("image inspected"),
           ],
-          {
-            modelTags: supportsImages
-              ? ["tool-use", "vision", "file-input"]
-              : ["tool-use"],
-          },
+          { modelTags: imageCase.modelTags },
         );
         try {
           writeFileSync(
@@ -398,7 +411,7 @@ describe("filesystem path handling", () => {
             ) as Record<string, unknown> | undefined;
           expect(part).toBeDefined();
           const output = part!.output as Record<string, unknown>;
-          if (supportsImages) {
+          if (imageCase.inline) {
             expect(output.type).toBe("content");
             expect(contentText(output)).toContain("image attached");
             expect(contentText(output)).not.toContain("binary or non-utf8");
diff --git a/tests/tla/README.md b/tests/tla/README.md
index 08ae0fac8..328b4f63d 100644
--- a/tests/tla/README.md
+++ b/tests/tla/README.md
@@ -7,6 +7,7 @@ TLA+ specifications for fx, checked with TLC, together with the scripts and Bun
 | `acp/` | The ACP permission modes, which match the CLI's `/permissions`, and the per-session Standard, Fast, and Ultrafast speed (`src/acp/`). | `acp/check.sh`, then the drivers in `drivers/acp/` |
 | `cli/` | How `fx` and `fx ask` handle `--model`, `--fast`, `--ultrafast`, and `--effort` at launch, for the current design and a proposed one that validates them. | `cli/check.sh`, `bun test drivers/cli/` |
 | `durable/` | Durable libfx sessions (`sdk/fx-sdk.js`): the journal, tool replay, parallel batches, fencing, the inbox, resumption, and snapshots. | `durable/check.sh`, `durable/mutants.py` |
+| `image_route/` | How images reach the model on each request (`src/core/images/image_route.zig`): whether the catalog's `vision` tag makes image input native, the user-image route and vision tool mode, tool images attached or withheld with a notice, one capability request and one catalog-down notice per turn, and crashes, duplicate requests, and lost or stale replies. `design/` holds the goal, vision, context, and design the checks trace to, and `mutations.json` the planted bugs. | `image_route/check.sh`, which runs `bun run verify`: TLC, every graph edge replayed against the real core, code traces checked by TLC, every planted bug, and `design/DESIGN.md` traceability |
 | `indexer/` | When a scanned root's listing may be reused, merging parallel grep results, the file picker's loading row, and listing snapshots (`src/core/indexer/`). | `indexer/check.sh` |
 | `mcp/` | The MCP-v2 engine (`src/mcp/`): wire format, requests, stdio, version detection, the tool catalog, both HTTP transports, input-required rounds, authorization, subscriptions, elicitation, and the engine. `rules.md` lists the MCP specification rules the models cite by ID. | `mcp/check.sh`, then the drivers in `drivers/mcp/` |
 | `mcp_host/` | fx's MCP host (`src/core/mcp_host/`): host lifecycle, saved credentials, logins shared between processes, sign-in, and elicitation routing. | `mcp_host/check.sh`, `bun test drivers/mcp_host/` |
diff --git a/tests/tla/drivers/image_route/code-to-spec.ts b/tests/tla/drivers/image_route/code-to-spec.ts
new file mode 100644
index 000000000..ed009349d
--- /dev/null
+++ b/tests/tla/drivers/image_route/code-to-spec.ts
@@ -0,0 +1,146 @@
+// Code to spec: runs event sequences through the real core, with faults,
+// records each run as a JSON trace, and has TLC check that every trace is a
+// behavior of ImageRoute and keeps its laws (TraceImageRoute.tla).
+//
+// Each trace starts in a new harness process. The scripted traces are the
+// adversarial cases the design names; the random ones mix every event with
+// the faults the model allows: a crash at any step (the process is killed),
+// a request delivered twice, a reply that is lost (the next turn starts
+// first), stale, or duplicated, and a catalog that is down, missing the
+// model, or flapping between answers.
+import { mkdirSync, writeFileSync } from "node:fs";
+import { join } from "node:path";
+import { Harness, actFor, checkTlc, seededRandom, specFiles, toTla, type CheckedTlc, type Event, type Request, type View } from "./lib.ts";
+
+const listed = (vision: boolean, file_input: boolean): View => ({ kind: "listed", vision, file_input });
+const down: View = { kind: "down", vision: false, file_input: false };
+const missing: View = { kind: "missing", vision: false, file_input: false };
+// The live catalog's entry for the default model, spacexai/grok-4.7.
+const visionOnly = listed(true, false);
+const views: View[] = [listed(true, true), visionOnly, listed(false, true), listed(false, false), missing, down];
+
+function req(flags: Partial<Request>): Request {
+  return { user_images: false, pending_images: false, tool_images: false, fallback: false, catalog_down: false, ...flags };
+}
+
+const requests: Request[] = [];
+for (let bits = 0; bits < 32; bits += 1) {
+  const r = req({
+    user_images: (bits & 1) !== 0,
+    pending_images: (bits & 2) !== 0,
+    tool_images: (bits & 4) !== 0,
+    fallback: (bits & 8) !== 0,
+    catalog_down: (bits & 16) !== 0,
+  });
+  if (r.pending_images && !r.user_images) continue;
+  requests.push(r);
+}
+
+const turn = (view: View): Event => ({ event: "turn_started", view });
+const ready = (flags: Partial<Request>): Event => ({ event: "request_ready", req: req(flags) });
+const reply = (view: View): Event => ({ event: "capabilities_resolved", view });
+const crash: Event = { event: "crash" };
+
+/// The adversarial cases, by name.
+export const scripted: Record<string, Event[]> = {
+  // The reported bug: a tool image under the default model's catalog entry.
+  "default model tool image": [turn(visionOnly), ready({ tool_images: true, fallback: true }), ready({ tool_images: true, user_images: true })],
+  // A down catalog: one notice per turn, however many requests.
+  "catalog down notice once per turn": [
+    turn(down), ready({ tool_images: true, catalog_down: true }), reply(down),
+    ready({ tool_images: true, catalog_down: true }), ready({ tool_images: true, catalog_down: true }),
+    turn(down), ready({ tool_images: true, catalog_down: true }), reply(down),
+  ],
+  // A request delivered again, then another, while the reply is owed.
+  "duplicate request while a reply is owed": [
+    turn(missing), ready({ user_images: true }), ready({ user_images: true }), ready({ tool_images: true }), reply(visionOnly),
+  ],
+  // The reply is lost when the turn ends first, then arrives stale.
+  "lost reply then stale reply": [turn(down), ready({ tool_images: true }), turn(visionOnly), reply(down), ready({ tool_images: true })],
+  // The process dies while a reply is owed.
+  "crash while a reply is owed": [turn(down), ready({ user_images: true, pending_images: true }), crash, reply(visionOnly), ready({ user_images: true }), reply(visionOnly)],
+  // A duplicated reply, the second with a different answer.
+  "duplicated reply": [turn(missing), ready({ tool_images: true, fallback: true }), reply(listed(false, false)), reply(visionOnly), ready({ tool_images: true, fallback: true })],
+  // User images on a model without vision and no vision tool fail.
+  "user images with no route": [turn(listed(false, true)), ready({ user_images: true, pending_images: true }), ready({ user_images: true, fallback: true, pending_images: true })],
+  // The catalog recovers within the turn: the one resolve picks it up.
+  "catalog recovers within the turn": [turn(down), ready({ tool_images: true, user_images: true, fallback: true }), reply(listed(true, false)), ready({ tool_images: true })],
+};
+
+function randomEvents(random: () => number, length: number): Event[] {
+  const pick = <T>(items: T[]): T => items[Math.floor(random() * items.length)]!;
+  const pickView = () => (random() < 0.3 ? visionOnly : pick(views));
+  const events: Event[] = [turn(pickView())];
+  for (let i = 1; i < length; i += 1) {
+    const roll = random();
+    const previous = events[events.length - 1]!;
+    if (roll < 0.1 && previous.event === "request_ready") events.push(previous);
+    else if (roll < 0.5) events.push({ event: "request_ready", req: pick(requests) });
+    else if (roll < 0.75) events.push(reply(pickView()));
+    else if (roll < 0.93) events.push(turn(pickView()));
+    else events.push(crash);
+  }
+  return events;
+}
+
+export type CodeToSpecResult = {
+  traces: number;
+  steps: number;
+  tracesPath: string;
+  tlc: CheckedTlc;
+};
+
+/// Runs the traces through `bin` and checks them with `cfgName` from
+/// `cfgText` (TraceImageRoute.cfg by default).
+export async function codeToSpec(options: {
+  bin: string;
+  dir: string;
+  seed: number;
+  randomTraces: number;
+  maxLength: number;
+  cfgName?: string;
+  cfgText?: string;
+}): Promise<CodeToSpecResult> {
+  const random = seededRandom(options.seed);
+  const runs: { name: string; events: Event[] }[] = Object.entries(scripted).map(([name, events]) => ({ name, events }));
+  for (let i = 0; i < options.randomTraces; i += 1) {
+    runs.push({ name: `random ${i + 1} (seed ${options.seed})`, events: randomEvents(random, 2 + Math.floor(random() * (options.maxLength - 1))) });
+  }
+
+  const harness = await Harness.start(options.bin);
+  const traces: { name: string; states: Record<string, unknown>[] }[] = [];
+  let steps = 0;
+  try {
+    for (const run of runs) {
+      await harness.crash();
+      const states: Record<string, unknown>[] = [{ ...harness.last, act: { name: "Init" } }];
+      for (const event of run.events) {
+        const before = harness.last;
+        const shown = await harness.send(event);
+        states.push({ ...shown, act: actFor(event, before) });
+        steps += 1;
+      }
+      traces.push({ name: run.name, states });
+    }
+  } finally {
+    await harness.close();
+  }
+
+  mkdirSync(options.dir, { recursive: true });
+  const tracesPath = join(options.dir, "traces.json");
+  writeFileSync(tracesPath, `${JSON.stringify(traces, null, 1)}\n`);
+  const data = [
+    "---- MODULE TraceData ----",
+    "EXTENDS Sequences",
+    "Traces == <<",
+    traces.map((trace) => `  \\* ${trace.name}\n  ${toTla(trace.states)}`).join(",\n"),
+    ">>",
+    "====",
+    "",
+  ].join("\n");
+  const files = { ...specFiles(), "TraceData.tla": data };
+  const cfgName = options.cfgName ?? "TraceImageRoute.cfg";
+  if (options.cfgText) files[cfgName as keyof typeof files] = options.cfgText;
+  const tlc = await checkTlc(join(options.dir, "tlc"), "TraceImageRoute", cfgName, files);
+  return { traces: traces.length, steps, tracesPath, tlc };
+}
diff --git a/tests/tla/drivers/image_route/harness.zig b/tests/tla/drivers/image_route/harness.zig
new file mode 100644
index 000000000..377362769
--- /dev/null
+++ b/tests/tla/drivers/image_route/harness.zig
@@ -0,0 +1,103 @@
+//! A JSON-lines shell around the real image route core, for the Bun drivers.
+//!
+//! Built from `src/core/images/image_route.zig` (or a planted-bug copy of it)
+//! as the `image_route` module. On start it prints the core's zero state. Then
+//! it reads one event per line and prints one line per event:
+//!
+//!   in:  {"event":"turn_started","view":{"kind":"listed","vision":true,"file_input":false}}
+//!        {"event":"request_ready","req":{"user_images":false,...}}
+//!        {"event":"capabilities_resolved","view":{"kind":"down","vision":false,"file_input":false}}
+//!   out: {"state":{"support":"unknown","resolved":false,"notified":false,"pending":[]},"out":[...]}
+//!
+//! `state` is `image_route.abstract`, and `out` is the effects `step`
+//! returned, in the spec's record shapes. The harness is a shell: it turns a
+//! catalog view into a support value with the core's own
+//! `supportFromCatalog`, exactly as `model_capabilities.mergeCapabilities`
+//! does, and holds the state between lines. A crash is the driver killing
+//! this process.
+const std = @import("std");
+const image_route = @import("image_route");
+
+const ViewJson = struct {
+    kind: []const u8,
+    vision: bool = false,
+    file_input: bool = false,
+};
+
+const Input = struct {
+    event: []const u8,
+    view: ?ViewJson = null,
+    req: ?image_route.Request = null,
+};
+
+const EffectJson = struct {
+    kind: []const u8,
+    route: ?image_route.Route = null,
+    mode: ?image_route.VisionMode = null,
+    tool_images: ?image_route.ToolImages = null,
+    reason: ?image_route.FailReason = null,
+};
+
+const Line = struct {
+    state: image_route.Abstract,
+    out: []const EffectJson,
+};
+
+fn catalogView(view: ViewJson) error{InvalidView}!image_route.CatalogView {
+    if (std.mem.eql(u8, view.kind, "down")) return .down;
+    if (std.mem.eql(u8, view.kind, "missing")) return .missing;
+    if (std.mem.eql(u8, view.kind, "listed")) return .{ .listed = .{ .vision = view.vision, .file_input = view.file_input } };
+    return error.InvalidView;
+}
+
+fn event(input: Input) error{ InvalidView, InvalidEvent }!image_route.Event {
+    if (std.mem.eql(u8, input.event, "turn_started")) {
+        return .{ .turn_started = image_route.supportFromCatalog(try catalogView(input.view orelse return error.InvalidEvent)) };
+    }
+    if (std.mem.eql(u8, input.event, "capabilities_resolved")) {
+        return .{ .capabilities_resolved = image_route.supportFromCatalog(try catalogView(input.view orelse return error.InvalidEvent)) };
+    }
+    if (std.mem.eql(u8, input.event, "request_ready")) {
+        return .{ .request_ready = input.req orelse return error.InvalidEvent };
+    }
+    return error.InvalidEvent;
+}
+
+fn effectJson(effect: image_route.Effect) EffectJson {
+    return switch (effect) {
+        .resolve_capabilities => .{ .kind = "resolve" },
+        .notify_catalog_down => .{ .kind = "notify" },
+        .send => |chosen| .{ .kind = "send", .route = chosen.route, .mode = chosen.mode, .tool_images = chosen.tool_images },
+        .fail => |reason| .{ .kind = "fail", .reason = reason },
+    };
+}
+
+fn writeLine(writer: *std.Io.Writer, state: *const image_route.State, effects: []const image_route.Effect) !void {
+    var buffer: [image_route.max_effects]EffectJson = undefined;
+    for (effects, 0..) |effect, index| buffer[index] = effectJson(effect);
+    try std.json.Stringify.value(Line{ .state = image_route.abstract(state), .out = buffer[0..effects.len] }, .{ .emit_null_optional_fields = false }, writer);
+    try writer.writeByte('\n');
+    try writer.flush();
+}
+
+pub fn main(init: std.process.Init) !void {
+    const io = init.io;
+    const alloc = init.gpa;
+
+    var in_buffer: [64 * 1024]u8 = undefined;
+    var stdin = std.Io.File.stdin().reader(io, &in_buffer);
+    var out_buffer: [64 * 1024]u8 = undefined;
+    var stdout = std.Io.File.stdout().writer(io, &out_buffer);
+
+    var state: image_route.State = .{};
+    try writeLine(&stdout.interface, &state, &.{});
+    while (try stdin.interface.takeDelimiter('\n')) |raw| {
+        const text = std.mem.trim(u8, raw, " \r\t");
+        if (text.len == 0) continue;
+        const parsed = try std.json.parseFromSlice(Input, alloc, text, .{});
+        defer parsed.deinit();
+        const out = image_route.step(state, try event(parsed.value));
+        state = out.state;
+        try writeLine(&stdout.interface, &state, out.effects());
+    }
+}
diff --git a/tests/tla/drivers/image_route/lib.ts b/tests/tla/drivers/image_route/lib.ts
new file mode 100644
index 000000000..0526bad44
--- /dev/null
+++ b/tests/tla/drivers/image_route/lib.ts
@@ -0,0 +1,286 @@
+// Shared pieces of the image route drivers: where the model and the core
+// live, building and running the JSON-lines harness around the real core, a
+// seeded random source, TLA+ value printing, and TLC runs on the pinned jar.
+import { existsSync, mkdirSync, readFileSync, writeFileSync } from "node:fs";
+import { join } from "node:path";
+import { REPO_ROOT, TLA_ROOT, runTlc, tlcToolchain, type TlcRun } from "../lib/tlc.ts";
+
+export const SPEC_DIR = join(TLA_ROOT, "image_route", "spec");
+export const MODEL_DIR = join(TLA_ROOT, "image_route");
+export const CORE_SOURCE = join(REPO_ROOT, "src", "core", "images", "image_route.zig");
+export const HARNESS_SOURCE = join(import.meta.dirname, "harness.zig");
+
+// TLC 1.7.4 (TLC2 2.19 of 08 August 2024, rev 5a47802), from
+// https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+export const PINNED_JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88";
+export const PINNED_TLC_VERSION = "TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)";
+
+export type View = { kind: "listed" | "missing" | "down"; vision: boolean; file_input: boolean };
+export type Request = {
+  user_images: boolean;
+  pending_images: boolean;
+  tool_images: boolean;
+  fallback: boolean;
+  catalog_down: boolean;
+};
+export type Effect = { kind: string; route?: string; mode?: string; tool_images?: string; reason?: string };
+export type CoreState = { support: string; resolved: boolean; notified: boolean; pending: Request[] };
+export type Shown = CoreState & { out: Effect[] };
+export type Act =
+  | { name: "Init" | "Crash" }
+  | { name: "TurnStarted"; view: View }
+  | { name: "RequestReady"; req: Request }
+  | { name: "CapabilitiesResolved"; view: View; answered: Request[] };
+export type Event =
+  | { event: "turn_started"; view: View }
+  | { event: "request_ready"; req: Request }
+  | { event: "capabilities_resolved"; view: View }
+  | { event: "crash" };
+
+/// The pinned toolchain, or a reason it is not the pinned one.
+export function pinnedToolchain() {
+  const toolchain = tlcToolchain();
+  if (toolchain.jarSha256 !== PINNED_JAR_SHA256) {
+    throw new Error(
+      `tla2tools.jar at ${toolchain.jar} has sha256 ${toolchain.jarSha256}, not the pinned ${PINNED_JAR_SHA256}. ` +
+        "Download v1.7.4 from https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar " +
+        "and point TLA2TOOLS_JAR at it.",
+    );
+  }
+  return toolchain;
+}
+
+/// A canonical JSON form with sorted keys, so equal values print equally.
+export function canonical(value: unknown): string {
+  if (Array.isArray(value)) return `[${value.map(canonical).join(",")}]`;
+  if (value && typeof value === "object") {
+    const entries = Object.entries(value as Record<string, unknown>).filter(([, v]) => v !== undefined);
+    entries.sort(([a], [b]) => (a < b ? -1 : a > b ? 1 : 0));
+    return `{${entries.map(([k, v]) => `${JSON.stringify(k)}:${canonical(v)}`).join(",")}}`;
+  }
+  return JSON.stringify(value);
+}
+
+/// A JSON value as TLA+: objects are records, arrays are sequences.
+export function toTla(value: unknown): string {
+  if (Array.isArray(value)) return `<<${value.map(toTla).join(", ")}>>`;
+  if (typeof value === "boolean") return value ? "TRUE" : "FALSE";
+  if (typeof value === "number") return String(value);
+  if (typeof value === "string") return JSON.stringify(value);
+  if (value && typeof value === "object") {
+    const entries = Object.entries(value as Record<string, unknown>).filter(([, v]) => v !== undefined);
+    return `[${entries.map(([k, v]) => `${k} |-> ${toTla(v)}`).join(", ")}]`;
+  }
+  throw new Error(`cannot print ${String(value)} as TLA+`);
+}
+
+/// Mulberry32: a small seeded generator, so a failing run can be replayed.
+export function seededRandom(seed: number): () => number {
+  let a = seed >>> 0;
+  return () => {
+    a = (a + 0x6d2b79f5) >>> 0;
+    let t = a;
+    t = Math.imul(t ^ (t >>> 15), t | 1);
+    t ^= t + Math.imul(t ^ (t >>> 7), t | 61);
+    return ((t ^ (t >>> 14)) >>> 0) / 4294967296;
+  };
+}
+
+/// Builds the harness around `core` (the real core, or a planted-bug copy)
+/// into `dir`. Throws with the compiler's output when the build fails.
+export function buildHarness(dir: string, core = CORE_SOURCE): string {
+  mkdirSync(dir, { recursive: true });
+  const bin = join(dir, "image-route-harness");
+  const build = Bun.spawnSync([
+    "zig", "build-exe", "-ODebug",
+    "--dep", "image_route", `-Mroot=${HARNESS_SOURCE}`, `-Mimage_route=${core}`,
+    `-femit-bin=${bin}`, "--cache-dir", join(REPO_ROOT, ".zig-cache"),
+  ], { cwd: REPO_ROOT, stdout: "pipe", stderr: "pipe" });
+  if (build.exitCode !== 0 || !existsSync(bin)) {
+    throw new Error(`harness build failed for ${core}:\n${build.stderr.toString()}${build.stdout.toString()}`);
+  }
+  return bin;
+}
+
+/// One running harness process. `crash()` kills it and starts a new one,
+/// which begins from the core's zero state: the only way the harness loses
+/// state is the way a real process does.
+export class Harness {
+  private proc!: ReturnType<typeof Bun.spawn>;
+  private lines: string[] = [];
+  private waiters: ((line: string) => void)[] = [];
+  private buffered = "";
+  last!: Shown;
+
+  private constructor(private readonly bin: string) {}
+
+  static async start(bin: string): Promise<Harness> {
+    const harness = new Harness(bin);
+    await harness.spawn();
+    return harness;
+  }
+
+  private async spawn() {
+    this.lines = [];
+    this.waiters = [];
+    this.buffered = "";
+    this.proc = Bun.spawn([this.bin], { stdin: "pipe", stdout: "pipe", stderr: "inherit" });
+    const reader = (this.proc.stdout as ReadableStream<Uint8Array>).getReader();
+    const decoder = new TextDecoder();
+    (async () => {
+      for (;;) {
+        const { value, done } = await reader.read();
+        if (done) break;
+        this.buffered += decoder.decode(value, { stream: true });
+        let newline = this.buffered.indexOf("\n");
+        while (newline >= 0) {
+          const line = this.buffered.slice(0, newline);
+          this.buffered = this.buffered.slice(newline + 1);
+          const waiter = this.waiters.shift();
+          if (waiter) waiter(line);
+          else this.lines.push(line);
+          newline = this.buffered.indexOf("\n");
+        }
+      }
+    })();
+    this.last = this.parse(await this.nextLine());
+  }
+
+  private nextLine(): Promise<string> {
+    const line = this.lines.shift();
+    if (line !== undefined) return Promise.resolve(line);
+    return new Promise((resolve, reject) => {
+      const timer = setTimeout(() => reject(new Error("the harness did not answer within 5 s")), 5000);
+      this.waiters.push((value) => { clearTimeout(timer); resolve(value); });
+    });
+  }
+
+  private parse(line: string): Shown {
+    const parsed = JSON.parse(line) as { state: CoreState; out: Effect[] };
+    return { ...parsed.state, out: parsed.out };
+  }
+
+  async send(event: Event): Promise<Shown> {
+    if (event.event === "crash") {
+      await this.crash();
+      return this.last;
+    }
+    const stdin = this.proc.stdin as import("bun").FileSink;
+    stdin.write(`${JSON.stringify(event)}\n`);
+    stdin.flush();
+    this.last = this.parse(await this.nextLine());
+    return this.last;
+  }
+
+  async crash() {
+    this.proc.kill("SIGKILL");
+    await this.proc.exited;
+    await this.spawn();
+  }
+
+  async close() {
+    (this.proc.stdin as import("bun").FileSink).end();
+    await this.proc.exited;
+  }
+}
+
+/// The event that performs `act` on the core.
+export function eventFor(act: Act): Event {
+  switch (act.name) {
+    case "TurnStarted": return { event: "turn_started", view: act.view };
+    case "RequestReady": return { event: "request_ready", req: act.req };
+    case "CapabilitiesResolved": return { event: "capabilities_resolved", view: act.view };
+    case "Crash": return { event: "crash" };
+    case "Init": throw new Error("Init is not an event");
+  }
+}
+
+/// The spec's act for `event`, applied from a core that showed `before`.
+export function actFor(event: Event, before: Shown): Act {
+  switch (event.event) {
+    case "turn_started": return { name: "TurnStarted", view: event.view };
+    case "request_ready": return { name: "RequestReady", req: event.req };
+    case "capabilities_resolved": return { name: "CapabilitiesResolved", view: event.view, answered: before.pending };
+    case "crash": return { name: "Crash" };
+  }
+}
+
+/// The part of a spec state the code shows.
+export function shownOf(state: Record<string, unknown>): Shown {
+  const { support, resolved, notified, pending, out } = state as Shown;
+  return { support, resolved, notified, pending, out };
+}
+
+export type CheckedTlc = TlcRun & { verdict: "pass" | "violated" | "error"; property: string | null; tlcVersion: string | null };
+
+/// Runs TLC and names the property it reports violated, including a
+/// temporal property, which TLC reports without a name.
+export async function checkTlc(
+  dir: string,
+  module: string,
+  cfg: string,
+  files: Record<string, string>,
+  extraArgs: string[] = [],
+): Promise<CheckedTlc> {
+  pinnedToolchain();
+  mkdirSync(dir, { recursive: true });
+  for (const [name, text] of Object.entries(files)) writeFileSync(join(dir, name), text);
+  const run = await runTlc(dir, module, cfg, [], dir, ["-deadlock", ...extraArgs]);
+  const tlcVersion = /^(TLC2 Version [^\n]*?)\s*$/m.exec(run.output)?.[1] ?? null;
+  // A property TraceImageRoute re-exports from ImageRoute is reported under
+  // its instance name, such as IR!ResolveOncePerTurn.
+  let property = /Error: (?:Invariant|Action property) ([\w!]+) is violated/.exec(run.output)?.[1]?.replace(/^\w+!/, "") ?? null;
+  if (!property && /Temporal properties were violated/.test(run.output)) {
+    const cfgText = files[cfg] ?? readFileSync(join(dir, cfg), "utf8");
+    const listed = /PROPERTY\s+([\s\S]*)$/.exec(cfgText)?.[1]?.split(/\s+/).filter(Boolean) ?? [];
+    property = listed.length === 1 ? listed[0]! : "temporal";
+  }
+  const passed = run.exitCode === 0 && /Model checking completed\. No error has been found\./.test(run.output);
+  const verdict = passed ? "pass" : property ? "violated" : "error";
+  return { ...run, verdict, property, tlcVersion };
+}
+
+/// The spec files with `ImageRoute.tla` replaced by `spec`.
+export function specFiles(spec = readFileSync(join(SPEC_DIR, "ImageRoute.tla"), "utf8")): Record<string, string> {
+  return {
+    "ImageRoute.tla": spec,
+    "MCImageRoute.cfg": readFileSync(join(SPEC_DIR, "MCImageRoute.cfg"), "utf8"),
+    "TraceImageRoute.tla": readFileSync(join(SPEC_DIR, "TraceImageRoute.tla"), "utf8"),
+    "TraceImageRoute.cfg": readFileSync(join(SPEC_DIR, "TraceImageRoute.cfg"), "utf8"),
+  };
+}
+
+/// A config that checks only `property`, which is an invariant or property
+/// of MCImageRoute.cfg, against `specification`.
+export function singleConfig(property: string, specification: string, invariants: string[]): string {
+  const kind = invariants.includes(property) ? "INVARIANT" : "PROPERTY";
+  return `SPECIFICATION ${specification}\n${specification === "TraceSpec" ? "CHECK_DEADLOCK FALSE\n" : ""}${kind}\n    ${property}\n`;
+}
+
+/// The names MCImageRoute.cfg lists, by section.
+export function configNames(cfgText = readFileSync(join(SPEC_DIR, "MCImageRoute.cfg"), "utf8")) {
+  const sections: Record<string, string[]> = {};
+  let current = "";
+  for (const raw of cfgText.split("\n")) {
+    const line = raw.replace(/\\\*.*$/, "").trim();
+    if (!line) continue;
+    const [first, ...rest] = line.split(/\s+/);
+    if (/^[A-Z_]+$/.test(first!)) {
+      current = first!;
+      sections[current] ??= [];
+      sections[current]!.push(...rest);
+    } else {
+      sections[current]?.push(first!, ...rest);
+    }
+  }
+  return { invariants: sections.INVARIANT ?? [], properties: sections.PROPERTY ?? [] };
+}
+
+/// Applies a planted bug: `find` must occur exactly once in `text`.
+export function plant(text: string, find: string, replace: string, id: string): string {
+  const first = text.indexOf(find);
+  if (first < 0 || text.indexOf(find, first + 1) >= 0) {
+    throw new Error(`${id}: the text to replace must occur exactly once`);
+  }
+  return text.slice(0, first) + replace + text.slice(first + find.length);
+}
diff --git a/tests/tla/drivers/image_route/mutations.ts b/tests/tla/drivers/image_route/mutations.ts
new file mode 100644
index 000000000..d0ec06c96
--- /dev/null
+++ b/tests/tla/drivers/image_route/mutations.ts
@@ -0,0 +1,81 @@
+// Proves no check is vacuous. Each planted bug in mutations.json breaks one
+// guard, in the spec or in the code, and must make its named property fail.
+//
+// A spec bug is checked twice: TLC on the mutated model with only the named
+// property, which must report exactly that property violated, and with all of
+// MCImageRoute.cfg, which must fail. A code bug is planted in a copy of
+// src/core/images/image_route.zig, the harness is rebuilt from the copy, and
+// both directions run: the spec-to-code sweep must find the core leaving the
+// model, and the code-to-spec traces must violate the named property alone and
+// fail the full trace check.
+import { mkdirSync, readFileSync, writeFileSync } from "node:fs";
+import { join } from "node:path";
+import { codeToSpec } from "./code-to-spec.ts";
+import { CORE_SOURCE, MODEL_DIR, SPEC_DIR, buildHarness, checkTlc, configNames, plant, singleConfig, specFiles } from "./lib.ts";
+import { specToCode } from "./spec-to-code.ts";
+
+type Mutation = { id: string; breaks: string; find: string; replace: string; expect: string };
+export const mutations = JSON.parse(readFileSync(join(MODEL_DIR, "mutations.json"), "utf8")) as { spec: Mutation[]; code: Mutation[] };
+
+export type MutationResult = {
+  id: string;
+  breaks: string;
+  expect: string;
+  caught: boolean;
+  detail: Record<string, string | number | null>;
+};
+
+export async function specMutations(dir: string): Promise<MutationResult[]> {
+  const spec = readFileSync(join(SPEC_DIR, "ImageRoute.tla"), "utf8");
+  const { invariants } = configNames();
+  const results: MutationResult[] = [];
+  for (const mutation of mutations.spec) {
+    const mutated = plant(spec, mutation.find, mutation.replace, mutation.id);
+    const files = specFiles(mutated);
+    const single = await checkTlc(join(dir, mutation.id, "single"), "ImageRoute", "Single.cfg", {
+      ...files,
+      "Single.cfg": singleConfig(mutation.expect, "Spec", invariants),
+    });
+    const full = await checkTlc(join(dir, mutation.id, "full"), "ImageRoute", "MCImageRoute.cfg", files);
+    results.push({
+      id: mutation.id,
+      breaks: mutation.breaks,
+      expect: mutation.expect,
+      caught: single.verdict === "violated" && single.property === mutation.expect && full.verdict === "violated",
+      detail: { alone: single.property ?? single.verdict, full: full.property ?? full.verdict, states: single.distinctStates },
+    });
+  }
+  return results;
+}
+
+export async function codeMutations(dir: string, graphPath: string, seed: number, randomTraces: number): Promise<MutationResult[]> {
+  const core = readFileSync(CORE_SOURCE, "utf8");
+  const traceCfg = readFileSync(join(SPEC_DIR, "TraceImageRoute.cfg"), "utf8");
+  const { invariants } = configNames(traceCfg);
+  const results: MutationResult[] = [];
+  for (const mutation of mutations.code) {
+    const work = join(dir, mutation.id);
+    mkdirSync(work, { recursive: true });
+    const source = join(work, "image_route.zig");
+    writeFileSync(source, plant(core, mutation.find, mutation.replace, mutation.id));
+    const bin = buildHarness(work, source);
+    const sweep = await specToCode(bin, graphPath);
+    const alone = await codeToSpec({
+      bin, dir: join(work, "alone"), seed, randomTraces, maxLength: 30,
+      cfgName: "Single.cfg", cfgText: singleConfig(mutation.expect, "TraceSpec", invariants),
+    });
+    const full = await codeToSpec({ bin, dir: join(work, "full"), seed, randomTraces, maxLength: 30 });
+    results.push({
+      id: mutation.id,
+      breaks: mutation.breaks,
+      expect: mutation.expect,
+      caught: sweep.failure !== null && alone.tlc.verdict === "violated" && alone.tlc.property === mutation.expect && full.tlc.verdict === "violated",
+      detail: {
+        specToCode: sweep.failure ? `left the model after ${sweep.failure.path.join(" > ")}` : "not detected",
+        alone: alone.tlc.property ?? alone.tlc.verdict,
+        full: full.tlc.property ?? full.tlc.verdict,
+      },
+    });
+  }
+  return results;
+}
diff --git a/tests/tla/drivers/image_route/spec-to-code.ts b/tests/tla/drivers/image_route/spec-to-code.ts
new file mode 100644
index 000000000..d5c6d96e8
--- /dev/null
+++ b/tests/tla/drivers/image_route/spec-to-code.ts
@@ -0,0 +1,86 @@
+// Spec to code: replays every transition of ImageRoute's TLC state graph
+// against the real core through the harness, and after every step checks
+// that what the core shows (abstract(state) and the step's effects) equals
+// the model's state.
+//
+// The model keeps no history beyond one turn, so its graph is small enough
+// to sweep whole: for each edge, the core is reset to its zero state, driven
+// along a shortest path from the initial state to the edge's source, and then
+// across the edge. A Crash edge kills the harness process and starts a new
+// one. Every edge is taken, so coverage is complete or the run fails.
+import { loadGraph } from "../graph.mjs";
+import { Harness, canonical, eventFor, shownOf, type Act } from "./lib.ts";
+
+type Graph = { states: Map<string, Record<string, unknown>>; next: Map<string, Set<string>>; init: string };
+
+export type SpecToCodeResult = {
+  states: number;
+  edges: number;
+  steps: number;
+  failure: null | { path: string[]; expected: string; shown: string };
+};
+
+function label(act: Act): string {
+  if (act.name === "TurnStarted" || act.name === "CapabilitiesResolved") {
+    const view = act.view.kind === "listed" ? `listed(vision=${act.view.vision},file_input=${act.view.file_input})` : act.view.kind;
+    return `${act.name}(${view})`;
+  }
+  if (act.name === "RequestReady") {
+    const flags = Object.entries(act.req).filter(([, on]) => on).map(([name]) => name);
+    return `RequestReady(${flags.join(",") || "no images"})`;
+  }
+  return act.name;
+}
+
+/// Shortest paths from the initial state, as state ids from init to each state.
+function shortestPaths(graph: Graph): Map<string, string[]> {
+  const paths = new Map<string, string[]>([[graph.init, [graph.init]]]);
+  const queue = [graph.init];
+  while (queue.length > 0) {
+    const from = queue.shift()!;
+    for (const to of graph.next.get(from) ?? []) {
+      if (paths.has(to)) continue;
+      paths.set(to, [...paths.get(from)!, to]);
+      queue.push(to);
+    }
+  }
+  return paths;
+}
+
+export async function specToCode(bin: string, graphPath: string): Promise<SpecToCodeResult> {
+  const graph = (await loadGraph(graphPath)) as Graph;
+  const paths = shortestPaths(graph);
+  const zero = canonical(shownOf(graph.states.get(graph.init)!));
+  const edges: [string, string][] = [];
+  for (const [from, targets] of graph.next) for (const to of targets) edges.push([from, to]);
+  edges.sort(([a1, b1], [a2, b2]) => (a1 + b1 < a2 + b2 ? -1 : 1));
+
+  const harness = await Harness.start(bin);
+  let steps = 0;
+  try {
+    for (const [from, to] of edges) {
+      // Back to the zero state: a turn that starts with an unreachable
+      // catalog holds exactly the core's initial state.
+      const reset = await harness.send({ event: "turn_started", view: { kind: "down", vision: false, file_input: false } });
+      if (canonical(reset) !== zero) {
+        return { states: graph.states.size, edges: edges.length, steps, failure: { path: ["reset"], expected: zero, shown: canonical(reset) } };
+      }
+      const route = [...paths.get(from)!.slice(1), to];
+      const taken: string[] = [];
+      for (const id of route) {
+        const state = graph.states.get(id)!;
+        const act = state.act as Act;
+        taken.push(label(act));
+        const shown = canonical(await harness.send(eventFor(act)));
+        steps += 1;
+        const expected = canonical(shownOf(state));
+        if (shown !== expected) {
+          return { states: graph.states.size, edges: edges.length, steps, failure: { path: taken, expected, shown } };
+        }
+      }
+    }
+  } finally {
+    await harness.close();
+  }
+  return { states: graph.states.size, edges: edges.length, steps, failure: null };
+}
diff --git a/tests/tla/drivers/image_route/traceability.ts b/tests/tla/drivers/image_route/traceability.ts
new file mode 100644
index 000000000..686cd3566
--- /dev/null
+++ b/tests/tla/drivers/image_route/traceability.ts
@@ -0,0 +1,139 @@
+// The traceability check: design/DESIGN.md must account for every review
+// question, every rule, and every law, and each enforcement entry must name
+// something that exists.
+//
+// Enforcement entries are backticked tokens in the last column of the rule
+// and law tables under "## Enforcement":
+//   inv:Name        an invariant defined in ImageRoute.tla and listed in MCImageRoute.cfg
+//   prop:Name       a property defined in ImageRoute.tla and listed in MCImageRoute.cfg
+//   trace:Name      a check TraceImageRoute.cfg lists, run on traces of the real core
+//   mutation:ID     a planted bug in mutations.json
+//   zig:path#name   a `test "name"` block in that Zig file
+//   e2e:path#name, sdk:path#name   a test whose source contains that name
+//   driver:name     a driver stage: spec-to-code or code-to-spec
+//   review:text     how a check that cannot be automated is enforced instead
+import { existsSync, readFileSync } from "node:fs";
+import { join } from "node:path";
+import { REPO_ROOT } from "../lib/tlc.ts";
+import { MODEL_DIR, SPEC_DIR, configNames } from "./lib.ts";
+import { mutations } from "./mutations.ts";
+
+export type Traceability = { problems: string[]; rules: number; laws: number; questions: number; entries: number };
+
+function section(text: string, heading: string): string {
+  const start = text.indexOf(`\n## ${heading}\n`);
+  if (start < 0) return "";
+  const rest = text.slice(start + heading.length + 5);
+  const end = rest.search(/\n## /);
+  return end < 0 ? rest : rest.slice(0, end);
+}
+
+function rows(text: string, prefix: string): string[][] {
+  return text.split("\n")
+    .filter((line) => new RegExp(`^\\|\\s*${prefix}\\d+\\s*\\|`).test(line))
+    .map((line) => line.split("|").slice(1, -1).map((cell) => cell.trim()));
+}
+
+export function checkTraceability(designPath = join(MODEL_DIR, "design", "DESIGN.md")): Traceability {
+  const problems: string[] = [];
+  const design = readFileSync(designPath, "utf8");
+  const spec = readFileSync(join(SPEC_DIR, "ImageRoute.tla"), "utf8");
+  const traceSpec = readFileSync(join(SPEC_DIR, "TraceImageRoute.tla"), "utf8");
+  const model = configNames();
+  const trace = configNames(readFileSync(join(SPEC_DIR, "TraceImageRoute.cfg"), "utf8"));
+  const mutationIds = new Set([...mutations.spec, ...mutations.code].map((m) => m.id));
+  const defined = (text: string, name: string) => new RegExp(`^${name} ==`, "m").test(text);
+  const referenced = new Set<string>();
+  let entries = 0;
+
+  const checkToken = (owner: string, token: string) => {
+    entries += 1;
+    const colon = token.indexOf(":");
+    const kind = token.slice(0, colon);
+    const value = token.slice(colon + 1).trim();
+    const fileTest = () => {
+      const [path, name] = value.split("#");
+      const file = join(REPO_ROOT, path ?? "");
+      if (!path || !name || !existsSync(file)) return problems.push(`${owner}: ${token} names a file that does not exist`);
+      const source = readFileSync(file, "utf8");
+      const found = kind === "zig" ? source.includes(`test "${name}"`) : source.includes(name);
+      if (!found) problems.push(`${owner}: ${token} names a test that does not exist`);
+    };
+    switch (kind) {
+      case "inv":
+        referenced.add(value);
+        if (!defined(spec, value)) problems.push(`${owner}: ${token} is not defined in ImageRoute.tla`);
+        if (!model.invariants.includes(value)) problems.push(`${owner}: ${token} is not an INVARIANT in MCImageRoute.cfg`);
+        break;
+      case "prop":
+        referenced.add(value);
+        if (!defined(spec, value)) problems.push(`${owner}: ${token} is not defined in ImageRoute.tla`);
+        if (!model.properties.includes(value)) problems.push(`${owner}: ${token} is not a PROPERTY in MCImageRoute.cfg`);
+        break;
+      case "trace":
+        if (!defined(traceSpec, value)) problems.push(`${owner}: ${token} is not defined in TraceImageRoute.tla`);
+        if (![...trace.invariants, ...trace.properties].includes(value)) problems.push(`${owner}: ${token} is not checked by TraceImageRoute.cfg`);
+        break;
+      case "mutation":
+        if (!mutationIds.has(value)) problems.push(`${owner}: ${token} is not in mutations.json`);
+        break;
+      case "zig":
+      case "e2e":
+      case "sdk":
+        fileTest();
+        break;
+      case "driver":
+        if (!["spec-to-code", "code-to-spec"].includes(value)) problems.push(`${owner}: ${token} is not a driver stage`);
+        break;
+      case "review":
+        if (value.length < 20) problems.push(`${owner}: ${token} must say how it is enforced`);
+        break;
+      default:
+        problems.push(`${owner}: ${token} has an unknown kind`);
+    }
+  };
+  const tokens = (cell: string | undefined) => [...(cell ?? "").matchAll(/`([a-z]+:[^`]+)`/g)].map((m) => m[1]!);
+
+  // Every review question is answered or listed as not applicable.
+  const answers = section(design, "Questions");
+  const answered = new Set([...answers.matchAll(/^- Q(\d+)\b/gm)].map((m) => Number(m[1])));
+  const notApplicable = /^Not applicable:(.*)$/m.exec(answers)?.[1] ?? "";
+  const skipped = new Set([...notApplicable.matchAll(/Q(\d+)/g)].map((m) => Number(m[1])));
+  for (let q = 1; q <= 39; q += 1) {
+    if (answered.has(q) && skipped.has(q)) problems.push(`Q${q} is both answered and listed as not applicable`);
+    if (!answered.has(q) && !skipped.has(q)) problems.push(`Q${q} is neither answered nor listed as not applicable`);
+  }
+
+  const enforcement = section(design, "Enforcement");
+  // Every rule has one row with a status; an applicable one names its checks.
+  const ruleRows = rows(enforcement, "R");
+  for (let r = 1; r <= 11; r += 1) {
+    const matches = ruleRows.filter((row) => row[0] === `R${r}`);
+    if (matches.length !== 1) { problems.push(`R${r} needs exactly one row under Enforcement, found ${matches.length}`); continue; }
+    const [, status, reason, enforced] = matches[0]!;
+    if (!["pass", "fail", "n/a"].includes(status ?? "")) problems.push(`R${r} has status "${status}", not pass, fail, or n/a`);
+    if (!reason) problems.push(`R${r} gives no reason`);
+    const found = tokens(enforced);
+    if (status !== "n/a" && found.length === 0) problems.push(`R${r} applies but names no enforcement`);
+    for (const token of found) checkToken(`R${r}`, token);
+  }
+
+  // Every law the design states has a row, enforced by the model or a test.
+  const lawIds = [...section(design, "Laws").matchAll(/^- \*\*(L\d+)\b/gm)].map((m) => m[1]!);
+  if (lawIds.length === 0) problems.push("the Laws section states no laws");
+  const lawRows = rows(enforcement, "L");
+  for (const id of lawIds) {
+    const matches = lawRows.filter((row) => row[0] === id);
+    if (matches.length !== 1) { problems.push(`${id} needs exactly one row under Enforcement, found ${matches.length}`); continue; }
+    const found = tokens(matches[0]!.at(-1));
+    if (found.length === 0) problems.push(`${id} names no enforcement`);
+    for (const token of found) checkToken(id, token);
+  }
+  for (const row of lawRows) if (!lawIds.includes(row[0]!)) problems.push(`${row[0]} has an enforcement row but is not stated under Laws`);
+
+  // Every check the model runs belongs to a rule or a law.
+  for (const name of [...model.invariants, ...model.properties]) {
+    if (name !== "TypeOK" && !referenced.has(name)) problems.push(`MCImageRoute.cfg checks ${name}, which no rule or law names`);
+  }
+  return { problems, rules: ruleRows.length, laws: lawIds.length, questions: answered.size + skipped.size, entries };
+}
diff --git a/tests/tla/drivers/image_route/verify.ts b/tests/tla/drivers/image_route/verify.ts
new file mode 100644
index 000000000..fbc1082b4
--- /dev/null
+++ b/tests/tla/drivers/image_route/verify.ts
@@ -0,0 +1,111 @@
+// `bun run verify` from tests/tla/image_route/: the one gate for the image
+// route design. In order, and every step must pass:
+//
+//   1. the pinned TLC and the Java that runs it;
+//   2. TLC on ImageRoute.tla with MCImageRoute.cfg, which also writes the
+//      state graph;
+//   3. the harness, built from the real src/core/images/image_route.zig;
+//   4. spec to code: every graph edge replayed against the real core;
+//   5. code to spec: scripted and random traces with faults, checked by TLC;
+//   6. every planted bug in the spec caught by its property;
+//   7. every planted bug in the code caught in both directions;
+//   8. traceability: DESIGN.md accounts for every question, rule, and law.
+//
+// Settings: FX_IMAGE_ROUTE_SEED (default 20261019), FX_IMAGE_ROUTE_TRACES
+// (random traces, default 300), FX_TLA_OUT (where the report goes).
+import { mkdirSync, readFileSync, writeFileSync } from "node:fs";
+import { dirname, join } from "node:path";
+import { outDir, writeJson } from "../lib/tlc.ts";
+import { codeToSpec } from "./code-to-spec.ts";
+import { MODEL_DIR, PINNED_TLC_VERSION, buildHarness, checkTlc, pinnedToolchain, specFiles } from "./lib.ts";
+import { codeMutations, specMutations } from "./mutations.ts";
+import { specToCode } from "./spec-to-code.ts";
+import { checkTraceability } from "./traceability.ts";
+
+const seed = Number(process.env.FX_IMAGE_ROUTE_SEED ?? "20261019");
+const randomTraces = Number(process.env.FX_IMAGE_ROUTE_TRACES ?? "300");
+const out = outDir("image-route");
+const report: Record<string, unknown> = { started: new Date().toISOString(), seed, randomTraces, out };
+const failures: string[] = [];
+const started = performance.now();
+const elapsed = (from: number) => `${((performance.now() - from) / 1000).toFixed(1)} s`;
+
+function stage(name: string, ok: boolean, summary: string) {
+  console.log(`${ok ? "PASS" : "FAIL"} ${name}: ${summary}`);
+  if (!ok) failures.push(name);
+}
+
+try {
+  const toolchain = pinnedToolchain();
+  report.toolchain = toolchain;
+  stage("toolchain", true, `tla2tools.jar sha256 ${toolchain.jarSha256.slice(0, 12)}, ${toolchain.javaVersion}`);
+
+  let at = performance.now();
+  const model = await checkTlc(join(out, "model"), "ImageRoute", "MCImageRoute.cfg", specFiles(), ["-dump", "dot,actionlabels", join(out, "model", "graph")]);
+  report.model = { verdict: model.verdict, property: model.property, distinctStates: model.distinctStates, depth: model.depth, durationMs: model.durationMs, tlcVersion: model.tlcVersion, generated: Number(/^(\d+) states generated, \d+ distinct states found/m.exec(model.output)?.[1] ?? NaN) };
+  const versionOk = model.tlcVersion === PINNED_TLC_VERSION;
+  stage("model check", model.verdict === "pass" && versionOk,
+    `${model.verdict}${model.property ? ` (${model.property})` : ""}, ${model.distinctStates} distinct of ${(report.model as { generated: number }).generated} generated states, depth ${model.depth}, ${model.durationMs} ms, ${model.tlcVersion}`);
+  const graphPath = join(out, "model", "graph.dot");
+
+  at = performance.now();
+  const bin = buildHarness(join(out, "harness"));
+  stage("harness", true, `built from src/core/images/image_route.zig in ${elapsed(at)}`);
+
+  at = performance.now();
+  const sweep = await specToCode(bin, graphPath);
+  report.specToCode = sweep;
+  stage("spec to code", sweep.failure === null,
+    sweep.failure
+      ? `the core left the model after ${sweep.failure.path.join(" > ")}: expected ${sweep.failure.expected}, shown ${sweep.failure.shown}`
+      : `${sweep.edges} of ${sweep.edges} edges over ${sweep.states} states, ${sweep.steps} steps, ${elapsed(at)}`);
+
+  at = performance.now();
+  const traces = await codeToSpec({ bin, dir: join(out, "code-to-spec"), seed, randomTraces, maxLength: 30 });
+  report.codeToSpec = { traces: traces.traces, steps: traces.steps, tracesPath: traces.tracesPath, verdict: traces.tlc.verdict, property: traces.tlc.property, distinctStates: traces.tlc.distinctStates, durationMs: traces.tlc.durationMs };
+  stage("code to spec", traces.tlc.verdict === "pass",
+    `${traces.traces} traces, ${traces.steps} steps, TLC ${traces.tlc.verdict}${traces.tlc.property ? ` (${traces.tlc.property})` : ""}, ${traces.tlc.distinctStates} distinct states, ${elapsed(at)}`);
+
+  at = performance.now();
+  const specBugs = await specMutations(join(out, "spec-mutations"));
+  report.specMutations = specBugs;
+  for (const bug of specBugs) console.log(`  ${bug.caught ? "caught" : "MISSED"} ${bug.id} by ${bug.expect}: alone ${bug.detail.alone}, full ${bug.detail.full}`);
+  stage("spec mutations", specBugs.every((bug) => bug.caught), `${specBugs.filter((bug) => bug.caught).length} of ${specBugs.length} caught, ${elapsed(at)}`);
+
+  at = performance.now();
+  const codeBugs = await codeMutations(join(out, "code-mutations"), graphPath, seed, Math.min(randomTraces, 150));
+  report.codeMutations = codeBugs;
+  for (const bug of codeBugs) console.log(`  ${bug.caught ? "caught" : "MISSED"} ${bug.id} by ${bug.expect}: alone ${bug.detail.alone}, full ${bug.detail.full}; spec to code ${bug.detail.specToCode}`);
+  stage("code mutations", codeBugs.every((bug) => bug.caught), `${codeBugs.filter((bug) => bug.caught).length} of ${codeBugs.length} caught, ${elapsed(at)}`);
+
+  const trace = checkTraceability();
+  report.traceability = trace;
+  for (const problem of trace.problems) console.log(`  ${problem}`);
+  // The check itself must reject a design that drops a rule, names a check
+  // that does not exist, or leaves a question unanswered.
+  const design = readFileSync(join(MODEL_DIR, "design", "DESIGN.md"), "utf8");
+  const broken = [
+    ["a missing rule row", design.replace(/^\| R5 \|.*\n/m, "")],
+    ["an invariant that does not exist", design.replace("`inv:OneSnapshot`, `trace:OneSnapshot`", "`inv:OneSnapshots`, `trace:OneSnapshot`")],
+    ["an unanswered question", design.replace(/^- Q24:.*\n/m, "")],
+  ] as const;
+  const rejected = broken.filter(([, text]) => {
+    const path = join(out, "traceability", "DESIGN.md");
+    mkdirSync(dirname(path), { recursive: true });
+    writeFileSync(path, text);
+    return text !== design && checkTraceability(path).problems.length > 0;
+  });
+  report.traceabilitySelfCheck = rejected.map(([name]) => name);
+  stage("traceability", trace.problems.length === 0 && rejected.length === broken.length,
+    `${trace.questions} questions, ${trace.rules} rules, ${trace.laws} laws, ${trace.entries} enforcement entries, ${trace.problems.length} problems; rejects ${rejected.length} of ${broken.length} broken designs`);
+} catch (error) {
+  failures.push("verify");
+  console.error(`FAIL verify: ${(error as Error).message}`);
+  report.error = (error as Error).stack;
+}
+
+report.failures = failures;
+report.durationMs = Math.round(performance.now() - started);
+writeJson(join(out, "report.json"), report);
+console.log(`${failures.length === 0 ? "verify passed" : `verify failed: ${failures.join(", ")}`} in ${elapsed(started)}; report ${join(out, "report.json")}`);
+process.exitCode = failures.length === 0 ? 0 : 1;
diff --git a/tests/tla/image_route/check.sh b/tests/tla/image_route/check.sh
new file mode 100755
index 000000000..1845654bb
--- /dev/null
+++ b/tests/tla/image_route/check.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Checks the image route design: TLC on ImageRoute.tla, both driver
+# directions against the real core, every planted bug, and DESIGN.md
+# traceability. `bun run verify` in this folder is the gate; this script is
+# the tests/tla/<area>/check.sh entry point that runs it.
+set -euo pipefail
+cd "$(dirname "$0")"
+exec bun run verify
diff --git a/tests/tla/image_route/design/CONTEXT.md b/tests/tla/image_route/design/CONTEXT.md
new file mode 100644
index 000000000..14a5167c0
--- /dev/null
+++ b/tests/tla/image_route/design/CONTEXT.md
@@ -0,0 +1,98 @@
+# Context: how images reach the model
+
+Line numbers refer to `origin/main` at `b0a90fd3a` unless a line says "this change". The design in `DESIGN.md` moves some of this code. `git show b0a90fd3a:<path>` shows it as cited.
+
+## The report
+
+A libfx user building an AI SDK harness adapter reported that an image in a tool result never reaches the agent unless they pass a custom `model`. The default model, `spacexai/grok-4.7`, is listed in fx's model catalog with `vision` but without `file-input`, and fx requires both. The report held on libfx 0.0.13 and again on 0.0.14. The reproduction is the AI SDK example `examples/ai-functions/src/harness-agent/fx/with-to-model-output.ts`, lines 53–54, which set the model. Removing them makes the image disappear.
+
+Both catalogs fx reads were fetched on 2026-10-19:
+
+| Catalog | Used by | Models | `spacexai/grok-4.7` tags |
+| --- | --- | --- | --- |
+| `https://ai-gateway.vercel.sh/coding-agent/v1/models` | capability lookups (`src/builtins/gateway.zig:46`, the E2E fake at `tests/e2e/gateway-stream-lifecycle.test.ts:1305`), libfx `listModels` (`sdk/fx-sdk.js:611`) | 263 | `reasoning`, `tool-use`, `implicit-caching`, `vision`, `structured-output` |
+| `https://ai-gateway.vercel.sh/v1/models` | the public catalog, and the fallback models path when no web-search path is set (`src/core/app/app_agent_runtime.zig:250`) | 478 | the same |
+
+In `/v1/models`, 73 models list `vision` without `file-input`, including the default and `spacexai/grok-4.6`. None lists `file-input` without `vision`.
+
+The AI Gateway documents the two tags as separate capabilities. Vision covers images such as a PNG screenshot. File input covers documents such as a PDF ([Inputs and Tools](https://vercel.com/docs/ai-gateway/inputs-and-tools)). For the AI SDK format that fx speaks, image input is "a `file` part with an `image/*` `mediaType`" ([Vision and Image Input](https://vercel.com/docs/ai-gateway/inputs-and-tools/vision)).
+
+## Entry points
+
+| Entry point | Path to the decision |
+| --- | --- |
+| `fx`, `fx ask` | `processQueuedPromptLoop` (`src/core/agent/runtime/orchestrator.zig:6915`) builds every model request of a turn |
+| libfx `createFxEngine` (native and WebAssembly) | The ACP server in the Zig core, then the same loop. A host tool returns `{ type: "libfx.tool-result", text, images }` (`sdk/tests/test-agent-images.mjs:1266`), which becomes `tool_result_memory.tool_images` |
+| `read_file` on an image | The same loop, with the image in `tool_result_memory` (`tests/e2e/file-tool-paths.test.ts:349-440`) |
+
+The default model is `spacexai/grok-4.7` (`src/builtins/gateway.zig:43`).
+
+## Data flow today
+
+1. The gateway catalog's `tags` array is parsed into `has_vision` and `has_file_input` (`src/builtins/gateway.zig:2755-2762`, fields at `src/core/gateway/model_catalog.zig:326`).
+2. `fromCatalogEntry` copies them to `supports_vision` and `supports_file_input` (`src/core/gateway/model_catalog_metadata.zig:17-18`).
+3. `mergeCapabilities` sets `image_input_support` to `.native` only when both are true, and to `.non_native` otherwise (`src/core/config/model_capabilities.zig:100-103`). Without catalog metadata it stays `.unknown` (`src/core/config/model_capabilities.zig:36-40`, `:66`). **This is the bug.**
+4. `CapabilityResolver` caches the catalog per process. Its states are `idle`, `ready`, and `failed` (`src/core/gateway/gateway_provider.zig:148-160`). `resolve` fetches only when idle (`:217-219`). When the catalog failed, or the model is missing from it, `resolve` returns the local fallback, whose support is unknown (`:221-228`, `:242-247`). The catalog is refreshed at most every 60 seconds (`src/core/gateway/provider_versions.zig:12`, `gateway_provider.zig:177-181`), and a failed refresh keeps the last good catalog (`gateway_provider.zig:196-197`).
+5. At turn start, the orchestrator resolves capabilities when the turn has images or when vision routing needs them (`orchestrator.zig:5772-5783`, `requiresResolvedRequestCapabilities` at `:5606-5618`).
+6. For each request in the turn loop:
+   - `request_capabilities` is a turn-local copy (`orchestrator.zig:6942`).
+   - `visionPolicy` picks the user-image route and the vision tool mode from `image_input_support` (`orchestrator.zig:6196-6213`, called at `:7372-7377`).
+   - User images are projected for that route. A request with user images and no route fails with `ModelImageCapabilityUnavailable` or `SubscriptionNativeImageUnavailable` (`:7402-7437`).
+   - Only then, if tool images are present and support is unknown, capabilities are resolved again, at most once per turn (`:7485-7493`).
+   - Native support materializes the tool images inline (`:7494-7506`). Otherwise `projectToolImageMessages` strips them and adds a notice to the tool message (`src/core/agent/runtime/gateway_step.zig:268-300`).
+   - When support is unknown and the catalog is known to be down, the user is told once per turn (`orchestrator.zig:7523-7530`).
+7. On the wire, every retained tool image goes out as a `{"type":"file","mediaType":"image/…","data":…}` part in a user message after the tool run (`src/gateway/vercel_protocol.zig:679-716`). The tool-result part keeps only its text (`:718-742`). User images are file parts too (`:780-823`).
+
+## Who owns each piece of state
+
+| State | Owner | Lifetime | Refresh |
+| --- | --- | --- | --- |
+| Which models take images | The AI Gateway catalog | External | Read by HTTP |
+| Cached catalog | `CapabilityResolver` (`gateway_provider.zig:154-160`) | One process | Every 60 s, or when access changes |
+| Request capabilities | The turn loop (`orchestrator.zig:5774`, `:6942`) | One turn | Once at turn start, and once more for tool images (`:7489`) |
+| Whether the turn re-resolved | `tool_image_capabilities_resolved` (`orchestrator.zig:6943`) | One turn | Set once |
+| Whether the user was told | `tool_image_strip_notified` (`orchestrator.zig:7079`) | One turn | Set once |
+| Pending user images | `pending_image_ids` (`orchestrator.zig:7028-7033`) | One turn | As the model views them |
+| Tool image bytes | The session image store, through `tool_result_memory.tool_images` and `tool_image_handle` (`src/core/shared/types.zig:1320-1338`) | The session | Dropped images keep a name without bytes (`types.zig:1335-1337`). `withholdDroppedImages` turns them into notes (`src/core/images/image_attachments.zig:862-889`) |
+
+## Contracts and saved formats
+
+- `ImageInputSupport` (`model_capabilities.zig:36-40`) is in-memory only. `/model` info prints it next to `supports_vision` and `supports_file_input` (`src/core/app/app_commands.zig:3048-3050`).
+- The catalog `tags` array is an external contract that fx reads and never writes.
+- The routing decision, the withheld-image notice, and the materialized image bytes are built per request in the overlay arena and never saved (`orchestrator.zig:7494-7507`). Sessions save tool images by handle or name, as before. No saved format records image support.
+- The wire format is the AI SDK prompt with `file` parts. It doesn't change.
+
+## Callers of `image_input_support`
+
+`orchestrator.zig:5615`, `:7373`, `:7425`, `:7485`, `:7494`, `:7507`, `:7524`, and `:9849` (a suggestion in a model error), `gateway_step.zig:271-286`, `app_commands.zig:3048`, and tests in `src/core/agent/runtime/tests/gateway_flow.zig`, `tool_flow.zig`, `support.zig`, `src/core/gateway/gateway_provider.zig`, `src/core/subagent/agent_adapter.zig`, and `src/gateway/chat_completions.zig`.
+
+## Constraints
+
+- Zig 0.17, standard library only. The core imports nothing but `std`.
+- The decision runs once per model request, never at startup. The startup budget is 2 ms per CLI path (`AGENTS.md`, Benchmarks).
+- Permission handling is unchanged. Images from permission-denied results never leave the process (`vercel_protocol.zig:691-704`).
+- libfx has two surfaces, native and WebAssembly, that share this Zig code. Both must pass `sdk/tests/test-agent-images.mjs`.
+- The model never changes within a turn: `gateway_model` is always `job.model` (`orchestrator.zig:7273`, `:7300`).
+
+## Existing code that makes the wrong design look easy
+
+1. The wire part is named `file` (`vercel_protocol.zig:708`), so the `file-input` tag reads like a requirement for sending it. It isn't. The tag means documents.
+2. Three providers that have no `file-input` tag set `has_file_input = vision` to satisfy the rule: configured Chat Completions providers (`src/gateway/chat_completions.zig:235`), Codex (`src/gateway/openai_codex_models.zig:286`), and Grok subscriptions (`src/gateway/xai_grok_models.zig:364`). That kept the bug invisible everywhere except the gateway catalog.
+3. Every image test fixture pairs `vision` with `file-input`: `sdk/tests/test-agent-images.mjs:34`, `tests/e2e/file-tool-paths.test.ts:365`, `tests/e2e/vision-route-fake-gateway.test.ts:227-232`, and about 40 more (`git grep -n file-input -- tests sdk`). No test ran a vision-only catalog entry, though 73 live models are vision-only.
+4. `processQueuedPrompt routes images natively only when vision and file input are both supported` (`src/core/agent/runtime/tests/gateway_flow.zig:2508-2537`) set `image_input_support` by hand from its expectation. It stated the rule without testing where it comes from.
+5. The rule predates `ImageInputSupport`. Commit `77e62a3ac` (2026-08-30, "Hide Vision from native image models") carried `supports_vision and supports_file_input` over from the initial commit (`git show 77e62a3ac^:src/core/agent/runtime/orchestrator.zig`, lines 3462 and 3505).
+6. The tool-image re-resolve sits after the route is chosen (`orchestrator.zig:7372` against `:7485`), the easiest place to add it. When it changes support, one request takes its route and vision tool mode from the old value and its tool images from the new one.
+
+## Fakes the drivers use
+
+The only fakes are effect handlers at the edge of a shell:
+
+| Fake | Where | Stands in for |
+| --- | --- | --- |
+| The catalog reply | `tests/tla/drivers/image_route/code-to-spec.ts`, `spec-to-code.ts` | The result of the core's `resolve_capabilities` effect, and the capabilities a turn starts with, given as a catalog view the harness turns into support with the real `supportFromCatalog` |
+| Recording `send`, `fail`, and `notify` | `tests/tla/drivers/image_route/harness.zig` | Sending the request, failing the turn, and printing the notice. The harness prints the effects instead of running them |
+| A crash | `Harness.crash` in `tests/tla/drivers/image_route/lib.ts` | A process dying. The driver kills the harness process with `SIGKILL` and starts a new one |
+| The fake gateway | `startFakeGateway` (`tests/e2e/tmux-helpers.ts`) in `tests/e2e/file-tool-paths.test.ts` | The catalog and the model, for the built `fx` binary |
+| `mockGateway` | `sdk/tests/test-agent-images.mjs:79-101` | The catalog and the model, for libfx |
+
+The drivers call the real `src/core/images/image_route.zig` through the harness. They never reimplement it.
diff --git a/tests/tla/image_route/design/DESIGN.md b/tests/tla/image_route/design/DESIGN.md
new file mode 100644
index 000000000..30dc3c5b3
--- /dev/null
+++ b/tests/tla/image_route/design/DESIGN.md
@@ -0,0 +1,143 @@
+# Design: image route
+
+How fx decides, for each model request, where images go: inline, through the vision tool, or nowhere with a notice. `CONTEXT.md` describes the code on `b0a90fd3a`. Line numbers here refer to that commit too, except those marked "this change", which refer to this branch.
+
+`tests/tla/drivers/image_route/traceability.ts` reads this file. It requires every question below to be answered or listed as not applicable, every rule and law to have a row under Enforcement, and every entry there to name a check that exists.
+
+## Questions
+
+- Q1: Values cross. The catalog sends `tags` strings, the core gets a `Support` enum and five `Request` flags (`image_route.zig:94-105`, this change), and image bytes stay as session handles until the shell materializes them for the provider (`orchestrator.zig:7463-7476`, this change). Logs get the decision's tag names (`orchestrator.zig:7375-7388`, this change).
+- Q2: A core event is under 16 bytes, once per request, plus at most one capability request per turn. Images are at most 8 per result and 5 MiB encoded each (`image_data.zig:6-8`). At 100x the images per session, `requestMaxDimension` shrinks each one (`image_data.zig:168`), and the request budget withholds the rest (`request_image_budget.zig`).
+- Q3: The gateway catalog owns capability. `CapabilityResolver` caches it per process and refreshes every 60 s (`gateway_provider.zig:167-207`). The core holds one snapshot per turn and refreshes it at most once in the turn, only when images wait on unknown support.
+- Q4: The largest inline value is one tool image, 5 MiB encoded at most, bounded by `withholdRequestToolImages` (`execution_memory.zig:800`) and the request budget. Notices are fixed text cut to `max_tool_result_bytes` (`gateway_step.zig:285-293`, this change).
+- Q5: Yes. The model gets images only when it can read them, a notice only when they are withheld, and the core gets flags, never bytes.
+- Q6: One turn loop per session builds requests. Parallel tools finish before the next request is built, and subagents run their own turn loops. No two writers share a core state.
+- Q7: The turn loop is the core state's only writer (`orchestrator.zig:6888-6891`, this change), so nothing is lost.
+- Q8: A reply nothing waits for, stale or duplicated, is ignored. A request delivered while a reply is owed replaces the waiting one, and the reply answers the newest. A reply after its turn ended meets a reset state.
+- Q9: Yes, today. The route is chosen before tool images trigger a second catalog check (`orchestrator.zig:7372` against `:7485`), so one request can mix two support values. The design asks first and decides after the reply (`image_route.zig:166-190`, this change), and `OneSnapshot` checks it.
+- Q10: The resolver's catalog, which its owner already guards against concurrent readers (`gateway_provider.zig:165-166`). It is unchanged. The core's state is a turn-local value.
+- Q11: A request delivered twice runs nothing more (`DuplicateRequestIsQuiet`). Model request retries are the gateway step's, unchanged.
+- Q12: The capability request is a GET and safe to repeat, but the core never repeats it within a turn. A lost reply ends with the turn, and the next turn asks again.
+- Q13: `resolve_capabilities` is idempotent, keyed per turn by `resolved`. `notify_catalog_down` is not idempotent, keyed per turn by `notified`. `send` and `fail` happen once per request, and the core never re-emits them.
+- Q14: The catalog fetch keeps the transport's deadline. A timeout leaves the resolver failed and support unknown, so the request goes out without images and with the "could not confirm" notice. The caller assumes nothing about vision.
+- Q15: A slow, down, rate-limited, or malformed catalog leaves the resolver failed (`gateway.zig:2713-2715` rejects malformed JSON), which the core sees as unknown support. The request still goes out, without images.
+- Q16: The core's state lives in memory and dies with the process. Tool images stay in the session store, and the next process decides again from its first turn.
+- Q18: Unknown support with a down catalog: one notice per turn in the transcript (`orchestrator.zig:7493-7496`, this change), and a model-facing note that it may recover. No vision: the model is told to call the vision tool, or to ask for a vision model. User images with no route: `ModelImageCapabilityUnavailable` or `SubscriptionNativeImageUnavailable`, as before. Each recovers on a later turn once the catalog answers.
+- Q19: Nothing. A withheld image stays in the store with a notice (`NoSilentWithhold`), session-dropped images become notes (`image_attachments.zig:883-887`), and the `vision_policy` trace line now records the tool image decision (`orchestrator.zig:7375-7388`, this change).
+- Q21: None in the core. The resolver's refresh interval uses `io_mod.milliTimestamp` (`gateway_provider.zig:173`), unchanged.
+- Q22: The core has one waiting request and at most two effects per step (`Bounded`). Images in history are bounded by the existing caps in Q2.
+- Q24: One `step` call and one scan of the request's messages per model request (`requestHasToolImages`, `orchestrator.zig:6199-6208`, this change). Nothing runs at startup, per keystroke, or per token.
+- Q25: The scan is linear in the request's history, like the projections beside it that already walk every message (`withholdDroppedImages`, `materializeToolImages`).
+- Q26: One core state per turn, turns run one at a time per session, and each subagent has its own.
+- Q27: No saved format or protocol changes. `ImageInputSupport` keeps its tags and moves its definition to `image_route.Support` (`model_capabilities.zig:37`, this change). Saved sessions resume unchanged, and their images now reach vision-only models.
+- Q29: `/model` info prints image support (`app_commands.zig:3048-3050`) and now shows `native` for vision-only models. The CLI, TUI, ACP, and libfx share the code. Older releases keep the old rule.
+- Q30: The gateway controls the tags over TLS. A repository cannot set capabilities, because project `.fx.json` accepts no profile-owned keys (`config_runtime.zig` `parseProjectSafeFields`). Tool output reaches the core only as a flag that images exist.
+- Q31: Nowhere. Core events and the trace line hold only model ids and tag names.
+- Q32: No. Images from permission-denied results still never leave the process (`vercel_protocol.zig:691-704`).
+- Q33: Dropping `file_input` from one condition (`model_capabilities.zig:100` on `b0a90fd3a`) fixes the reported bug.
+- Q34: The core extraction. Without it the reported bug is still fixed, but Q9's ordering fix has no function to check against a model. The design keeps it for that reason and for G6; see R10.
+- Q35: It reuses the resolver, `projectToolImageMessages`, and the wire encoder. It replaces `visionPolicy` and the inline re-resolve, so no parallel path remains, and it drops both inherited flaws: the `file-input` rule and the late re-resolve.
+- Q36: Nothing. No setting, override, or provider table.
+- Q37: `tests/e2e/file-tool-paths.test.ts` through the built binary, `sdk/tests/test-agent-images.mjs` through libfx on both backends, the drivers on the real core, and a live run of the built binary against the gateway (`GOAL.md`, item 6).
+- Q38: The `vision_policy` trace line logs `image_support`, `route`, `mode`, `pending_images`, and `tool_images` for every request, and `image_gate` diagnostics record each failure (`orchestrator.zig:7357-7366`, this change).
+- Q39: Revert the change. No data needs migrating. Reverting `supportFromCatalog` alone (`image_route.zig:47-52`, this change) restores the old rule.
+
+Not applicable: Q17, Q20, Q23, Q28 (the core writes nothing that can be partial, holds no process, file, lock, or connection, consumes one synchronous event at a time, and changes no saved format, so nothing needs migrating).
+
+## Laws
+
+The laws `step` obeys. Each one is a named invariant or property in `spec/ImageRoute.tla`, checked by TLC over the whole model and on traces of the real core.
+
+- **L1 VisionImpliesNative**: a model the catalog lists with `vision` takes images inline, whatever its `file-input` tag says. One listed without vision does not, and an unlisted model or an unreachable catalog leaves support unknown.
+- **L2 RouteModeCoherent**: the vision tool is offered exactly on the fallback route.
+- **L3 NativeExcludesFallback**: native delivery and the vision tool never meet in one request.
+- **L4 OneSnapshot**: a request's route, vision tool mode, and tool image handling all follow the one support value the state holds after the step (ordering).
+- **L5 UnknownNeverInline**: no image goes to a model the catalog has not confirmed (ownership: the catalog decides).
+- **L6 NoSilentWithhold**: tool images are attached, or withheld with a notice the model can act on, never neither. The vision tool is required exactly while user images wait for it (`RequiredWhenPending`).
+- **L7 FailExactlyWhenUnroutable**: a request with user images and no route fails, with the reason that matches support. Nothing else fails.
+- **L8 ResolveOncePerTurn**: the core asks for capabilities only when images wait on unknown support (`ResolveOnlyWhenNeeded`), and at most once per turn (idempotence). This also makes the shell's effect loop end.
+- **L9 NotifyOncePerTurn**: the user hears about a down catalog only for tool images it withholds (`NotifyOnlyWhenDown`), and at most once per turn (idempotence).
+- **L10 DuplicateRequestIsQuiet**: a request delivered while a reply is owed runs nothing, and a reply nothing waits for changes nothing (`StaleReplyIsQuiet`) (idempotence and ordering).
+- **L11 Bounded**: at most one waiting request, and at most two effects per step, a notice and then one answer (bounds).
+- **L12 Answered**: every request that waits for a reply is answered, unless its turn ends first (liveness).
+- **L13 DecideOnlyWhenReady**: a decision comes only once no reply is owed. While one is owed, the turn has asked once and decided nothing (`PendingWaitsForReply`) (ordering).
+- **L14 TurnResets**: a new turn, and a new process after a crash, start with no request waiting and no capability request or notice spent.
+
+## Enforcement
+
+### Rules
+
+| Rule | Status | Reason | Enforced by |
+| --- | --- | --- | --- |
+| R1 | pass | Core events carry flags only. Bytes stay as session handles until the shell materializes them, and base64 exists only in the AI SDK file part at the transport (`vercel_protocol.zig:706-712`). | `zig:src/core/images/image_route.zig#requests carry flags, not image bytes`, `review:the shell's materialization and the wire encoder are unchanged; a reviewer checks any new caller of image_route passes flags, which the Request type enforces at compile time` |
+| R2 | fail | Inherited and accepted. The AI SDK prompt has no image reference form, so every request resends the images in its history, now also for vision-only models. The existing caps bound each request. | `review:per-request image bytes stay bounded by request_image_budget.zig and withholdRequestToolImages; sending once by reference would need provider-side storage, a non-goal in GOAL.md` |
+| R3 | pass | Notices are fixed text cut to the result limit. Images are bounded by the existing caps, and the core never holds bytes. | `zig:src/core/agent/runtime/gateway_step.zig#projectToolImageMessages names the dead end when no fallback exists`, `inv:Bounded` |
+| R4 | pass | The gateway catalog is the source, the resolver caches it, and the core keeps one snapshot per turn that only a reply to its own request replaces. | `inv:VisionImpliesNative`, `inv:OneSnapshot`, `prop:StaleReplyIsQuiet` |
+| R5 | pass | One event per request, at most one capability request per turn, at most two effects per step. Image bytes per request are capped as in Q2. | `inv:Bounded`, `prop:ResolveOncePerTurn`, `inv:ResolveOnlyWhenNeeded` |
+| R6 | pass | Only the capability request repeats safely, and the core still sends it once per turn. Sends, failures, and notices are never re-emitted. | `prop:DuplicateRequestIsQuiet`, `prop:NotifyOncePerTurn`, `prop:ResolveOncePerTurn` |
+| R7 | pass | Crashes, a down or missing catalog, and lost, stale, and duplicated replies are actions in the model, and the code is checked on traces that inject them. | `inv:UnknownNeverInline`, `inv:TurnResets`, `prop:Answered`, `inv:FailExactlyWhenUnroutable`, `driver:code-to-spec` |
+| R8 | n/a | No saved format or protocol changes (Q27). The routing decision is never saved. | |
+| R9 | pass | It drops two inherited flaws: the `file-input` rule and the re-resolve after the route is chosen. | `mutation:S1`, `mutation:C1`, `mutation:S2`, `mutation:C7`, `inv:OneSnapshot` |
+| R10 | fail | Accepted. The reported bug needs one line. The pure core, its harness, and the drivers exist so the ordering fix (Q9) is checkable against a model, as G6 requires. | `review:the core adds no setting, cache, or provider table; Q34 and Final design name what could be removed`, `driver:spec-to-code` |
+| R11 | n/a | No mutable resource is opened by more than one process. The core's state is a value local to one turn. | |
+
+### Laws
+
+| Law | Statement | Enforced by |
+| --- | --- | --- |
+| L1 | Vision means native | `inv:VisionImpliesNative`, `trace:VisionImpliesNative`, `mutation:S1`, `mutation:C1`, `zig:src/core/images/image_route.zig#a catalog that lists vision makes image input native with or without file input`, `zig:src/core/config/model_capabilities.zig#image input support distinguishes unknown native and non native capability`, `zig:src/core/agent/runtime/tests/gateway_flow.zig#processQueuedPrompt routes images natively whenever the catalog lists vision`, `e2e:tests/e2e/file-tool-paths.test.ts#read_file attaches a workspace image inline for a vision model without file input`, `sdk:sdk/tests/test-agent-images.mjs#A host tool's image reaches a model the catalog lists with vision but not` |
+| L2 | Vision tool only on the fallback route | `inv:RouteModeCoherent`, `trace:RouteModeCoherent`, `mutation:S18`, `mutation:C17`, `zig:src/core/images/image_route.zig#every decision reads one support value` |
+| L3 | Native excludes the vision tool | `inv:NativeExcludesFallback`, `trace:NativeExcludesFallback`, `mutation:S19`, `mutation:C18`, `sdk:sdk/tests/test-agent-images.mjs#a native image model is not offered the vision tool` |
+| L4 | One snapshot per request | `inv:OneSnapshot`, `trace:OneSnapshot`, `mutation:S2`, `mutation:C7` |
+| L5 | Unknown never inline | `inv:UnknownNeverInline`, `trace:UnknownNeverInline`, `mutation:S5`, `mutation:C4`, `zig:src/core/agent/runtime/gateway_step.zig#projectToolImageMessages tells the truth when the catalog is unavailable` |
+| L6 | No silent withhold | `inv:NoSilentWithhold`, `inv:RequiredWhenPending`, `trace:NoSilentWithhold`, `trace:RequiredWhenPending`, `mutation:S17`, `mutation:C16`, `mutation:S10`, `mutation:C10`, `zig:src/core/agent/runtime/orchestrator.zig#requestHasToolImages ignores images the session dropped`, `e2e:tests/e2e/file-tool-paths.test.ts#read_file image is withheld with guidance for a text-only model` |
+| L7 | Fail exactly when unroutable | `inv:FailExactlyWhenUnroutable`, `trace:FailExactlyWhenUnroutable`, `mutation:S8`, `mutation:C9`, `zig:src/core/images/image_route.zig#user images without a route fail the request and never send` |
+| L8 | One capability request per turn, only for images | `inv:ResolveOnlyWhenNeeded`, `prop:ResolveOncePerTurn`, `trace:ResolveOnlyWhenNeeded`, `trace:ResolveOncePerTurn`, `mutation:S3`, `mutation:C2`, `mutation:S15`, `mutation:C14`, `zig:src/core/images/image_route.zig#a turn asks for capabilities at most once and answers the request it held` |
+| L9 | One catalog-down notice per turn, only when down | `inv:NotifyOnlyWhenDown`, `prop:NotifyOncePerTurn`, `trace:NotifyOnlyWhenDown`, `trace:NotifyOncePerTurn`, `mutation:S4`, `mutation:C3`, `mutation:S16`, `mutation:C15`, `zig:src/core/images/image_route.zig#the catalog-down notice reaches the user once per turn` |
+| L10 | Duplicates and stale replies are quiet | `prop:DuplicateRequestIsQuiet`, `prop:StaleReplyIsQuiet`, `trace:DuplicateRequestIsQuiet`, `trace:StaleReplyIsQuiet`, `mutation:S6`, `mutation:C5`, `mutation:S7`, `mutation:C6` |
+| L11 | Bounded | `inv:Bounded`, `trace:Bounded`, `mutation:S12`, `mutation:C11`, `zig:src/core/images/image_route.zig#abstract maps the pending request onto a sequence of at most one` |
+| L12 | Every waiting request is answered | `prop:Answered`, `mutation:S11`, `review:a finite trace cannot show liveness; TLC proves Answered over the whole model under fairness of replies, and ConformsToSpec makes each recorded reply clear its request` |
+| L13 | Decide only when no reply is owed | `inv:DecideOnlyWhenReady`, `inv:PendingWaitsForReply`, `trace:DecideOnlyWhenReady`, `trace:PendingWaitsForReply`, `mutation:S13`, `mutation:C12`, `mutation:S14`, `mutation:C13` |
+| L14 | Turns and processes start clean | `inv:TurnResets`, `trace:TurnResets`, `mutation:S9`, `mutation:C8` |
+
+## Final design
+
+### The fix
+
+`supportFromCatalog` (`src/core/images/image_route.zig:47-52`, this change) returns `native` when the catalog lists `vision` and `non_native` when it lists the model without it, and `unknown` for a missing model or a down catalog. `file-input` plays no part. `mergeCapabilities` calls it (`src/core/config/model_capabilities.zig:97-100`, this change), so the CLI, TUI, ACP, and libfx all change at once. `ImageInputSupport` is now an alias of `image_route.Support` (`model_capabilities.zig:37`, this change).
+
+### The core
+
+`src/core/images/image_route.zig` (this change) imports only `std`.
+
+- **State** (`:107-116`): `support`, the turn's one capability snapshot; `resolved` and `notified`, the turn's spent capability request and notice; `pending`, the request waiting for a reply, if any.
+- **Events** (`:118-127`): `turn_started(Support)`, `request_ready(Request)`, and `capabilities_resolved(Support)`. Time does not enter. I/O results arrive as `capabilities_resolved`, and failures arrive as the support value they produce.
+- **Effects** (`:135-146`), a tagged union of values: `resolve_capabilities`, `notify_catalog_down`, `send(Decision)`, and `fail(FailReason)`. At most two per step, returned in a fixed buffer with no allocation (`:148-156`).
+- **`step`** (`:158-164`) dispatches to three pure functions: `onRequest` (`:166-181`), `onResolved` (`:183-190`), and `decide` (`:192-205`). `decision` (`:207-225`) maps one support value and one request to a route, a vision tool mode, and a tool image handling. Absence is `?Request`, and errors are the `fail` effect. Nothing panics, and mutation is limited to `var next` copies inside one function.
+- **`abstract`** (`:235-251`) maps a state onto the spec's `support`, `resolved`, `notified`, and `pending`.
+
+### The shell
+
+The turn loop in `processQueuedPromptLoop` is the only code that runs effects.
+
+- It starts the core's state with `turn_started` (`orchestrator.zig:6888-6891`, this change).
+- For each request, it builds the `Request` flags, including whether a tool image survives `withholdDroppedImages` (`requestHasToolImages`, `:6199-6208`).
+- It then runs the effect loop: a capability request becomes `deps.resolve_model_capabilities` and its reply event, a notice is recorded, and `send` or `fail` is taken (`:7325-7366`).
+- The decision drives the user-image projection, the vision tool mode, tool image materialization, and the notice (`:7367-7496`).
+- `projectToolImageMessages` takes the core's `ToolImages` value instead of recomputing it from support and a flag (`gateway_step.zig:264-295`, this change).
+
+`visionPolicy`, `ImageRoute`, `VisionPolicy`, and the per-turn flags `tool_image_capabilities_resolved` and `tool_image_strip_notified` are gone, along with their tests. The core's tests and the model cover the same laws.
+
+### Mechanisms added, and the answers that required them
+
+| Mechanism | Required by |
+| --- | --- |
+| Support from `vision` alone | Q1 and R9: the inherited rule reads a document tag as an image tag |
+| Asking before deciding, with the request held in `pending` | Q9: deciding first splits one request across two snapshots |
+| `pending` replaced by a newer request, and stale replies ignored | Q8 and Q11 |
+| A pure core with `abstract` and a harness | Q37 and G6: the orchestrator cannot be checked against a model, and a pure step can |
+
+### Rules this design breaks
+
+- **R2, send only what is needed.** Every request still resends the images in its history, now also to the 73 vision-only models. The AI SDK prompt offers no reference form, and the existing caps bound each request. Sending by reference would need provider-side storage, a non-goal in `GOAL.md`.
+- **R10, build only what the problem needs.** The reported bug needs only `supportFromCatalog`'s one condition. The core extraction (about 250 lines with tests), the harness, and the drivers exist for the verification this workspace is for, and they make the ordering fix (Q9) checkable. Without that requirement, the smallest design is the one-line fix plus moving the orchestrator's re-resolve ahead of `visionPolicy`.
diff --git a/tests/tla/image_route/design/GOAL.md b/tests/tla/image_route/design/GOAL.md
new file mode 100644
index 000000000..3226b0db4
--- /dev/null
+++ b/tests/tla/image_route/design/GOAL.md
@@ -0,0 +1,44 @@
+# Goal
+
+## Problem
+
+fx never sends an image, from a tool or from the user, to a model that the catalog lists with `vision` but without `file-input`. The image stays in the session, and the model gets a notice that it should call the vision tool instead. fx's own default model, `spacexai/grok-4.7`, is one of the 73 models the gateway catalog lists this way (`CONTEXT.md`, The report). A libfx user hit this when an AI SDK tool returned an image to the default model: the agent never saw the image unless they set a different model.
+
+The cause is one rule: image input counts as native only when the catalog lists both `vision` and `file-input` (`src/core/config/model_capabilities.zig:100-103` on `b0a90fd3a`). The AI Gateway uses `file-input` for documents such as PDFs. fx sends images as AI SDK file parts with an image media type, and those need only `vision`.
+
+The same code has a second flaw. When tool images appear while support is unknown, the turn asks the catalog again, but only after the request's route and vision tool mode are already chosen (`orchestrator.zig:7372` against `:7485`). That one request can mix two capability values.
+
+## Success criteria
+
+Each criterion is a check that passes on this change and failed, or could fail, before it.
+
+| # | Criterion | Check |
+| --- | --- | --- |
+| G1 | A `read_file` image reaches a model the catalog lists with the default model's exact tags, inline, as an `image/png` file part. | `tests/e2e/file-tool-paths.test.ts`, "read_file attaches a workspace image inline for a vision model without file input". It fails on `b0a90fd3a` |
+| G2 | A libfx host tool's image reaches that model inline, on the native and WebAssembly backends, and the model is not offered the vision tool. | `sdk/tests/test-agent-images.mjs native` and `wasm`. The new case fails on `b0a90fd3a` |
+| G3 | A model listed without `vision` still gets the vision tool notice, and unknown support still sends no image. | The text-only E2E case, plus `UnknownNeverInline` in `ImageRoute.tla` and on code traces |
+| G4 | Every request's route, vision tool mode, and tool image handling come from one capability value. | `OneSnapshot` in `ImageRoute.tla` and on code traces, and planted bugs S2 and C7 |
+| G5 | No extra catalog traffic: at most one capability request per turn from the image decision, and none for a request without images. | `ResolveOncePerTurn` and `ResolveOnlyWhenNeeded` |
+| G6 | The decision is one pure function, checked against its model in both directions. | `bun run verify` in `tests/tla/image_route` |
+| G7 | Nothing slows startup or adds network I/O on a path without images. | The `Startup Latency` CI job, and `ResolveOnlyWhenNeeded` |
+
+## Non-goals
+
+- Supporting documents (PDFs) as tool results. The `file-input` tag would govern that, and fx does not send documents today.
+- Changing the gateway catalog or asking for different tags.
+- Removing the `has_file_input = vision` stand-ins in the Codex, Grok subscription, and Chat Completions providers (`CONTEXT.md`, item 2). They are now harmless, and changing them changes only what `/model` info prints.
+- Sending images once and referring to them afterwards (rule R2). The AI SDK prompt has no reference form, so every request resends the images in its history, as it already does for models with `file-input`.
+- A setting or override for image support.
+
+## What 100% done means
+
+Every item below passes for the exact commit that ships.
+
+1. `bun run verify` in `tests/tla/image_route` exits 0: the model check, spec to code over every edge, code to spec, every planted bug caught, and traceability.
+2. `zig fmt --check src/` exits 0.
+3. `zig build test` exits 0.
+4. `FX_SOUND=0 bun test file-tool-paths.test.ts -t 'read_file (attaches|image is withheld)'` in `tests/e2e` passes all three cases.
+5. `node sdk/tests/test-agent-images.mjs native` and `node --experimental-wasm-jspi sdk/tests/test-agent-images.mjs wasm` pass.
+6. A live run of `./zig-out/bin/fx` with `FX_MODEL=spacexai/grok-4.7`, reading a PNG with `read_file`, answers with what the image shows, with clean stderr.
+7. CI passes for the exact commit: `Build & Test`, `E2E (deterministic)`, `Shellcheck`, `Startup Latency`, and `macOS arm64`. This needs a pushed branch, which happens only when asked.
+8. `tests/tla/README.md` lists `image_route/`. The release note belongs to the next release PR, which the maintainer writes.
diff --git a/tests/tla/image_route/design/VISION.md b/tests/tla/image_route/design/VISION.md
new file mode 100644
index 000000000..0ad290a94
--- /dev/null
+++ b/tests/tla/image_route/design/VISION.md
@@ -0,0 +1,32 @@
+# Vision
+
+## The end state
+
+fx decides how images reach the model from one catalog fact: whether the model has vision. A model with vision gets every image inline, from the user or from a tool, through the one wire form the gateway documents for images. A model without vision gets the vision tool, or a plain explanation when no vision tool exists. A model fx cannot confirm gets no images, a notice that says so, and one more catalog check in the turn.
+
+That decision is one pure function, `image_route.step(state, event)`, in `src/core/images/image_route.zig`. It reads no clock, environment, or global and performs no I/O. The orchestrator's turn loop is its shell: it runs the effects `step` returns and feeds their results back as events. A TLA+ model states the laws the function keeps, and Bun drivers check the real function against the model, in both directions, on every change.
+
+## What the system is
+
+- **One snapshot per request.** Every part of a request's image handling reads the same capability value, even when that value changes mid-turn.
+- **Honest about what it withholds.** An image that does not reach the model always leaves a notice the model can act on. The user hears about it once per turn when the catalog itself is down.
+- **Bounded.** One waiting request, at most two effects per step, and at most one catalog request per turn from the image decision.
+- **Shared by every surface.** The CLI, the TUI, ACP, and both libfx backends run the same core.
+
+## What it refuses to be
+
+- **A guess.** fx sends no image to a model the catalog does not confirm, even one whose name suggests vision. Unknown means withheld.
+- **A second catalog.** fx keeps no table of which models take images, and offers no setting to override the gateway. The catalog is the source of truth, and a wrong tag gets fixed there.
+- **A retry loop.** The core never repeats a send, a failure, or a notice, and never asks the catalog twice in a turn.
+- **Provider-aware.** The core knows support values, not provider names. Provider quirks stay in the provider code that maps a catalog to support.
+
+## Tradeoffs it makes on purpose
+
+| Choice | Over | Because |
+| --- | --- | --- |
+| Trust the `vision` tag | Also requiring `file-input`, or probing a model with a test image | The gateway defines image input as `vision`. If a vision-tagged route rejects an image, the request fails visibly instead of silently losing the image |
+| Resend images with every request | Uploading once and sending references | The AI SDK prompt has no reference form. Existing caps bound every request (`request_image_budget.zig`, `image_data.requestMaxDimension`) |
+| One catalog request per turn | Re-checking on every request | Bounded latency and traffic matter more than seeing a recovery a few seconds sooner. The next turn checks again |
+| Ask before deciding | Deciding first and re-checking for tool images | Deciding first is what split one request across two values |
+| A pure core with a thin shell | Leaving the decision inline in the orchestrator | The orchestrator cannot be model checked. A pure step with `abstract()` can be checked edge by edge against the model |
+| Tell the user once per turn | Every request, or never | Every request is noise. Never hides a down catalog the user can do something about |
diff --git a/tests/tla/image_route/mutations.json b/tests/tla/image_route/mutations.json
new file mode 100644
index 000000000..8d3caa749
--- /dev/null
+++ b/tests/tla/image_route/mutations.json
@@ -0,0 +1,266 @@
+{
+  "about": "Planted bugs. Each one breaks one guard, and the named property must fail. Spec mutations edit spec/ImageRoute.tla and run TLC on MCImageRoute.cfg. Code mutations edit a copy of src/core/images/image_route.zig, rebuild the harness from it, and run both driver directions. Each find string must occur exactly once.",
+  "spec": [
+    {
+      "id": "S1",
+      "breaks": "Image support requires file-input as well as vision: the reported bug.",
+      "find": "(IF v.vision THEN \"native\" ELSE \"non_native\")",
+      "replace": "(IF v.vision /\\ v.file_input THEN \"native\" ELSE \"non_native\")",
+      "expect": "VisionImpliesNative"
+    },
+    {
+      "id": "S2",
+      "breaks": "A reply's decision reads the support from before the reply.",
+      "find": "/\\ out' = DecideOut(s, Head(pending), notified)",
+      "replace": "/\\ out' = DecideOut(support, Head(pending), notified)",
+      "expect": "OneSnapshot"
+    },
+    {
+      "id": "S3",
+      "breaks": "A turn asks for capabilities again after it already asked.",
+      "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ (r.user_images \\/ r.tool_images)",
+      "replace": "NeedsResolve(r) == support = \"unknown\" /\\ (r.user_images \\/ r.tool_images)",
+      "expect": "ResolveOncePerTurn"
+    },
+    {
+      "id": "S4",
+      "breaks": "The catalog-down notice repeats within a turn.",
+      "find": "/\\ r.catalog_down /\\ ~n",
+      "replace": "/\\ r.catalog_down",
+      "expect": "NotifyOncePerTurn"
+    },
+    {
+      "id": "S5",
+      "breaks": "Tool images go inline while support is unknown.",
+      "find": "[] s = \"unknown\" -> \"withheld_unknown\"",
+      "replace": "[] s = \"unknown\" -> \"attached\"",
+      "expect": "UnknownNeverInline"
+    },
+    {
+      "id": "S6",
+      "breaks": "A request delivered twice asks for capabilities twice.",
+      "find": "THEN pending' = <<r>> /\\ out' = <<>> /\\ UNCHANGED <<support, resolved, notified>>",
+      "replace": "THEN pending' = <<r>> /\\ out' = <<[kind |-> \"resolve\"]>> /\\ UNCHANGED <<support, resolved, notified>>",
+      "expect": "DuplicateRequestIsQuiet"
+    },
+    {
+      "id": "S7",
+      "breaks": "A stale reply overwrites the turn's support.",
+      "find": "THEN out' = <<>> /\\ UNCHANGED <<support, resolved, notified, pending>>",
+      "replace": "THEN out' = <<>> /\\ support' = Derive(v) /\\ UNCHANGED <<resolved, notified, pending>>",
+      "expect": "StaleReplyIsQuiet"
+    },
+    {
+      "id": "S8",
+      "breaks": "User images without a route are sent anyway.",
+      "find": "Unroutable(s, r) == r.user_images /\\ Decide(s, r).route = \"unavailable\"",
+      "replace": "Unroutable(s, r) == FALSE",
+      "expect": "FailExactlyWhenUnroutable"
+    },
+    {
+      "id": "S9",
+      "breaks": "A new turn keeps the previous turn's notice flag.",
+      "find": "/\\ notified' = FALSE   \\* a new turn may tell the user again",
+      "replace": "/\\ notified' = notified",
+      "expect": "TurnResets"
+    },
+    {
+      "id": "S10",
+      "breaks": "The vision tool is optional even while user images wait.",
+      "find": "ELSE IF r.pending_images THEN \"required\" ELSE \"optional\"",
+      "replace": "ELSE \"optional\"",
+      "expect": "RequiredWhenPending"
+    },
+    {
+      "id": "S11",
+      "breaks": "A reply leaves its request waiting.",
+      "find": "/\\ support' = s\n            /\\ pending' = <<>>",
+      "replace": "/\\ support' = s\n            /\\ pending' = pending",
+      "expect": "Answered"
+    },
+    {
+      "id": "S12",
+      "breaks": "The catalog-down notice comes after the answer.",
+      "find": "ELSE IF Notifies(s, r, n) THEN <<[kind |-> \"notify\"], Decide(s, r)>>",
+      "replace": "ELSE IF Notifies(s, r, n) THEN <<Decide(s, r), [kind |-> \"notify\"]>>",
+      "expect": "Bounded"
+    },
+    {
+      "id": "S13",
+      "breaks": "A request delivered while a reply is owed is decided at once.",
+      "find": "THEN pending' = <<r>> /\\ out' = <<>> /\\ UNCHANGED <<support, resolved, notified>>",
+      "replace": "THEN pending' = <<r>> /\\ out' = DecideOut(support, r, notified) /\\ UNCHANGED <<support, resolved, notified>>",
+      "expect": "DecideOnlyWhenReady"
+    },
+    {
+      "id": "S14",
+      "breaks": "Asking for capabilities does not mark the turn as having asked.",
+      "find": "THEN /\\ resolved' = TRUE",
+      "replace": "THEN /\\ resolved' = resolved",
+      "expect": "PendingWaitsForReply"
+    },
+    {
+      "id": "S15",
+      "breaks": "The core asks for capabilities for a request without images.",
+      "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ (r.user_images \\/ r.tool_images)",
+      "replace": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved",
+      "expect": "ResolveOnlyWhenNeeded"
+    },
+    {
+      "id": "S16",
+      "breaks": "The catalog-down notice appears when the catalog is up.",
+      "find": "/\\ r.catalog_down /\\ ~n",
+      "replace": "/\\ ~n",
+      "expect": "NotifyOnlyWhenDown"
+    },
+    {
+      "id": "S17",
+      "breaks": "Tool images vanish without a notice while support is unknown.",
+      "find": "[] s = \"unknown\" -> \"withheld_unknown\"",
+      "replace": "[] s = \"unknown\" -> \"none\"",
+      "expect": "NoSilentWithhold"
+    },
+    {
+      "id": "S18",
+      "breaks": "The vision tool is offered off the fallback route.",
+      "find": "mode == IF route # \"fallback\" THEN \"unavailable\"",
+      "replace": "mode == IF route # \"fallback\" THEN \"optional\"",
+      "expect": "RouteModeCoherent"
+    },
+    {
+      "id": "S19",
+      "breaks": "A native image model is routed through the vision tool.",
+      "find": "LET route == CASE s = \"native\" -> \"native\"",
+      "replace": "LET route == CASE s = \"native\" -> (IF r.fallback THEN \"fallback\" ELSE \"native\")",
+      "expect": "NativeExcludesFallback"
+    }
+  ],
+  "code": [
+    {
+      "id": "C1",
+      "breaks": "Image support requires file-input as well as vision: the reported bug.",
+      "find": ".listed => |tags| if (tags.vision) .native else .non_native,",
+      "replace": ".listed => |tags| if (tags.vision and tags.file_input) .native else .non_native,",
+      "expect": "VisionImpliesNative"
+    },
+    {
+      "id": "C2",
+      "breaks": "A turn asks for capabilities again after it already asked.",
+      "find": "if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) {",
+      "replace": "if (state.support == .unknown and (request.user_images or request.tool_images)) {",
+      "expect": "ResolveOncePerTurn"
+    },
+    {
+      "id": "C3",
+      "breaks": "The catalog-down notice repeats within a turn.",
+      "find": "if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) {",
+      "replace": "if (chosen.tool_images == .withheld_unknown and request.catalog_down) {",
+      "expect": "NotifyOncePerTurn"
+    },
+    {
+      "id": "C4",
+      "breaks": "Tool images go inline while support is unknown.",
+      "find": ".unknown => .withheld_unknown,",
+      "replace": ".unknown => .attached,",
+      "expect": "UnknownNeverInline"
+    },
+    {
+      "id": "C5",
+      "breaks": "A request delivered twice asks for capabilities twice.",
+      "find": "next.pending = request;\n        return .{ .state = next };",
+      "replace": "next.pending = request;\n        return withEffects(next, &.{.resolve_capabilities});",
+      "expect": "DuplicateRequestIsQuiet"
+    },
+    {
+      "id": "C6",
+      "breaks": "A stale reply overwrites the turn's support.",
+      "find": "const request = state.pending orelse return .{ .state = state };",
+      "replace": "const request = state.pending orelse return .{ .state = .{ .support = support, .resolved = state.resolved, .notified = state.notified } };",
+      "expect": "StaleReplyIsQuiet"
+    },
+    {
+      "id": "C7",
+      "breaks": "A reply's decision reads the support from before the reply: the old orchestrator order.",
+      "find": "next.support = support;\n    next.pending = null;\n    return decide(next, request);",
+      "replace": "next.pending = null;\n    var stale = decide(next, request);\n    stale.state.support = support;\n    return stale;",
+      "expect": "OneSnapshot"
+    },
+    {
+      "id": "C8",
+      "breaks": "A new turn keeps the previous turn's notice flag.",
+      "find": ".turn_started => |support| .{ .state = .{ .support = support } },",
+      "replace": ".turn_started => |support| .{ .state = .{ .support = support, .notified = state.notified } },",
+      "expect": "TurnResets"
+    },
+    {
+      "id": "C9",
+      "breaks": "User images without a route are sent anyway.",
+      "find": "if (request.user_images and chosen.route == .unavailable) {",
+      "replace": "if (request.user_images and chosen.route == .unavailable and false) {",
+      "expect": "FailExactlyWhenUnroutable"
+    },
+    {
+      "id": "C10",
+      "breaks": "The vision tool is optional even while user images wait.",
+      "find": "else if (request.pending_images)\n        .required",
+      "replace": "else if (false)\n        .required",
+      "expect": "RequiredWhenPending"
+    },
+    {
+      "id": "C11",
+      "breaks": "The catalog-down notice comes after the answer.",
+      "find": "return withEffects(next, &.{ .notify_catalog_down, .{ .send = chosen } });",
+      "replace": "return withEffects(next, &.{ .{ .send = chosen }, .notify_catalog_down });",
+      "expect": "Bounded"
+    },
+    {
+      "id": "C12",
+      "breaks": "A request delivered while a reply is owed is decided at once.",
+      "find": "next.pending = request;\n        return .{ .state = next };",
+      "replace": "next.pending = request;\n        return decide(next, request);",
+      "expect": "DecideOnlyWhenReady"
+    },
+    {
+      "id": "C13",
+      "breaks": "Asking for capabilities does not mark the turn as having asked.",
+      "find": "next.resolved = true;\n        next.pending = request;",
+      "replace": "next.pending = request;",
+      "expect": "PendingWaitsForReply"
+    },
+    {
+      "id": "C14",
+      "breaks": "The core asks for capabilities for a request without images.",
+      "find": "if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) {",
+      "replace": "if (state.support == .unknown and !state.resolved) {",
+      "expect": "ResolveOnlyWhenNeeded"
+    },
+    {
+      "id": "C15",
+      "breaks": "The catalog-down notice appears when the catalog is up.",
+      "find": "if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) {",
+      "replace": "if (chosen.tool_images == .withheld_unknown and !state.notified) {",
+      "expect": "NotifyOnlyWhenDown"
+    },
+    {
+      "id": "C16",
+      "breaks": "Tool images vanish without a notice while support is unknown.",
+      "find": ".unknown => .withheld_unknown,",
+      "replace": ".unknown => .none,",
+      "expect": "NoSilentWithhold"
+    },
+    {
+      "id": "C17",
+      "breaks": "The vision tool is offered off the fallback route.",
+      "find": "const mode: VisionMode = if (route != .fallback)\n        .unavailable",
+      "replace": "const mode: VisionMode = if (route != .fallback)\n        .optional",
+      "expect": "RouteModeCoherent"
+    },
+    {
+      "id": "C18",
+      "breaks": "A native image model is routed through the vision tool.",
+      "find": ".native => .native,",
+      "replace": ".native => if (request.fallback) .fallback else .native,",
+      "expect": "NativeExcludesFallback"
+    }
+  ]
+}
diff --git a/tests/tla/image_route/package.json b/tests/tla/image_route/package.json
new file mode 100644
index 000000000..a3a94d5fe
--- /dev/null
+++ b/tests/tla/image_route/package.json
@@ -0,0 +1,8 @@
+{
+  "name": "fx-tla-image-route",
+  "private": true,
+  "type": "module",
+  "scripts": {
+    "verify": "bun ../drivers/image_route/verify.ts"
+  }
+}
diff --git a/tests/tla/image_route/spec/ImageRoute.tla b/tests/tla/image_route/spec/ImageRoute.tla
new file mode 100644
index 000000000..a37e749db
--- /dev/null
+++ b/tests/tla/image_route/spec/ImageRoute.tla
@@ -0,0 +1,256 @@
+----------------------------- MODULE ImageRoute -----------------------------
+(***************************************************************************)
+(* How images reach the model on one request: the pure core                *)
+(* `step(state, event)` in src/core/images/image_route.zig.                *)
+(*                                                                         *)
+(* Each core event is one action with the same name: TurnStarted,          *)
+(* RequestReady, and CapabilitiesResolved. The environment acts through    *)
+(* the values those events carry and through Crash:                        *)
+(*   - the catalog can be listed, missing the model, or down (a refused,   *)
+(*     slow, or garbage catalog reads as down), in any order;              *)
+(*   - a reply can be lost (the next turn starts first), duplicated, or    *)
+(*     stale (CapabilitiesResolved with nothing waiting);                  *)
+(*   - a request can be delivered twice (RequestReady while a reply is     *)
+(*     owed);                                                              *)
+(*   - the process can crash at any step, which drops all core state.      *)
+(* A second process is not modeled: core state lives in one turn of one    *)
+(* process and nothing else can read or write it.                          *)
+(*                                                                         *)
+(* support, resolved, notified, and pending are `abstract(state)` in the   *)
+(* code. out is the effects the step returned, and act is the event the    *)
+(* step took, recorded so the laws can name it.                            *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+Supports == {"unknown", "non_native", "native"}
+Routes == {"native", "fallback", "unavailable"}
+Modes == {"unavailable", "optional", "required"}
+ToolImages == {"none", "attached", "withheld_fallback", "withheld_dead_end", "withheld_unknown"}
+Reasons == {"capability_unknown", "no_native_image"}
+
+Views == [kind: {"listed"}, vision: BOOLEAN, file_input: BOOLEAN]
+         \cup [kind: {"missing", "down"}, vision: {FALSE}, file_input: {FALSE}]
+
+Requests == {r \in [user_images: BOOLEAN, pending_images: BOOLEAN, tool_images: BOOLEAN,
+                    fallback: BOOLEAN, catalog_down: BOOLEAN] :
+               r.pending_images => r.user_images}
+
+Sends == [kind: {"send"}, route: Routes, mode: Modes, tool_images: ToolImages]
+Effects == [kind: {"resolve", "notify"}] \cup Sends \cup [kind: {"fail"}, reason: Reasons]
+
+\* At most one request; the core's `?Request`.
+Pending == {<<>>} \cup {<<r>> : r \in Requests}
+
+Acts == [name: {"Init", "Crash"}]
+        \cup [name: {"TurnStarted"}, view: Views]
+        \cup [name: {"RequestReady"}, req: Requests]
+        \cup [name: {"CapabilitiesResolved"}, view: Views, answered: Pending]
+
+VARIABLES support, resolved, notified, pending, out, act
+
+vars == <<support, resolved, notified, pending, out, act>>
+
+\* `supportFromCatalog`.
+Derive(v) == IF v.kind = "listed" THEN (IF v.vision THEN "native" ELSE "non_native") ELSE "unknown"
+
+\* `decision`.
+Decide(s, r) ==
+    LET route == CASE s = "native" -> "native"
+                   [] s = "unknown" -> "unavailable"
+                   [] OTHER -> IF r.fallback THEN "fallback" ELSE "unavailable"
+        mode == IF route # "fallback" THEN "unavailable"
+                ELSE IF r.pending_images THEN "required" ELSE "optional"
+        tool == IF ~r.tool_images THEN "none"
+                ELSE CASE s = "native" -> "attached"
+                       [] s = "unknown" -> "withheld_unknown"
+                       [] OTHER -> IF route = "fallback" THEN "withheld_fallback" ELSE "withheld_dead_end"
+    IN [kind |-> "send", route |-> route, mode |-> mode, tool_images |-> tool]
+
+Unroutable(s, r) == r.user_images /\ Decide(s, r).route = "unavailable"
+Notifies(s, r, n) == ~Unroutable(s, r) /\ Decide(s, r).tool_images = "withheld_unknown" /\ r.catalog_down /\ ~n
+
+\* `decide`: the effects of deciding r under s, and the next notified flag.
+DecideOut(s, r, n) ==
+    IF Unroutable(s, r)
+    THEN <<[kind |-> "fail", reason |-> IF s = "unknown" THEN "capability_unknown" ELSE "no_native_image"]>>
+    ELSE IF Notifies(s, r, n) THEN <<[kind |-> "notify"], Decide(s, r)>>
+    ELSE <<Decide(s, r)>>
+
+DecideNotified(s, r, n) == n \/ Notifies(s, r, n)
+
+NeedsResolve(r) == support = "unknown" /\ ~resolved /\ (r.user_images \/ r.tool_images)
+
+Init ==
+    /\ support = "unknown"
+    /\ resolved = FALSE
+    /\ notified = FALSE
+    /\ pending = <<>>
+    /\ out = <<>>
+    /\ act = [name |-> "Init"]
+
+TurnStarted(v) ==
+    /\ act' = [name |-> "TurnStarted", view |-> v]
+    /\ support' = Derive(v)
+    /\ resolved' = FALSE   \* a new turn may ask again
+    /\ notified' = FALSE   \* a new turn may tell the user again
+    /\ pending' = <<>>
+    /\ out' = <<>>
+
+RequestReady(r) ==
+    /\ act' = [name |-> "RequestReady", req |-> r]
+    /\ IF pending # <<>>
+       THEN pending' = <<r>> /\ out' = <<>> /\ UNCHANGED <<support, resolved, notified>>
+       ELSE IF NeedsResolve(r)
+       THEN /\ resolved' = TRUE
+            /\ pending' = <<r>>
+            /\ out' = <<[kind |-> "resolve"]>>
+            /\ UNCHANGED <<support, notified>>
+       ELSE /\ out' = DecideOut(support, r, notified)
+            /\ notified' = DecideNotified(support, r, notified)
+            /\ UNCHANGED <<support, resolved, pending>>
+
+CapabilitiesResolved(v) ==
+    /\ act' = [name |-> "CapabilitiesResolved", view |-> v, answered |-> pending]
+    /\ IF pending = <<>>
+       THEN out' = <<>> /\ UNCHANGED <<support, resolved, notified, pending>>
+       ELSE LET s == Derive(v) IN
+            /\ support' = s
+            /\ pending' = <<>>
+            /\ out' = DecideOut(s, Head(pending), notified)
+            /\ notified' = DecideNotified(s, Head(pending), notified)
+            /\ UNCHANGED resolved
+
+\* The process dies; the next process starts from the core's zero state.
+Crash ==
+    /\ act' = [name |-> "Crash"]
+    /\ support' = "unknown"
+    /\ resolved' = FALSE
+    /\ notified' = FALSE
+    /\ pending' = <<>>
+    /\ out' = <<>>
+
+Reply == pending # <<>> /\ \E v \in Views : CapabilitiesResolved(v)
+
+Next ==
+    \/ \E v \in Views : TurnStarted(v)
+    \/ \E r \in Requests : RequestReady(r)
+    \/ \E v \in Views : CapabilitiesResolved(v)
+    \/ Crash
+
+\* A reply the shell waits for arrives unless the turn ends first.
+Spec == Init /\ [][Next]_vars /\ WF_vars(Reply)
+
+-----------------------------------------------------------------------------
+(* Laws. DESIGN.md names each one and where it is enforced.                *)
+
+HasKind(k) == \E i \in 1..Len(out) : out[i].kind = k
+SendsOut == {out[i] : i \in {j \in 1..Len(out) : out[j].kind = "send"}}
+FailsOut == {out[i] : i \in {j \in 1..Len(out) : out[j].kind = "fail"}}
+\* The request this step decided, as a sequence of at most one.
+Decided == IF act.name = "RequestReady" THEN <<act.req>>
+           ELSE IF act.name = "CapabilitiesResolved" THEN act.answered
+           ELSE <<>>
+
+TypeOK ==
+    /\ support \in Supports
+    /\ resolved \in BOOLEAN
+    /\ notified \in BOOLEAN
+    /\ pending \in Pending
+    /\ Len(out) <= 2 /\ \A i \in 1..Len(out) : out[i] \in Effects
+    /\ act \in Acts
+
+\* L11: one waiting request, and at most a notice then one answer.
+Bounded ==
+    /\ Len(pending) <= 1
+    /\ Len(out) <= 2
+    /\ Len(out) = 2 => (out[1].kind = "notify" /\ out[2].kind = "send")
+
+\* L1: a model the catalog lists with vision takes images inline, whatever
+\* its file-input tag says; one listed without vision does not; an unlisted
+\* model or an unreachable catalog leaves support unknown.
+VisionImpliesNative ==
+    (act.name = "TurnStarted" \/ (act.name = "CapabilitiesResolved" /\ act.answered # <<>>)) =>
+        /\ (act.view.kind = "listed" /\ act.view.vision) => support = "native"
+        /\ (act.view.kind = "listed" /\ ~act.view.vision) => support = "non_native"
+        /\ act.view.kind # "listed" => support = "unknown"
+
+\* L5: no image goes to a model the catalog has not confirmed.
+UnknownNeverInline == \A e \in SendsOut : e.tool_images = "attached" => support = "native"
+
+\* L4: route, mode, and tool images all follow the one support value the
+\* state holds after the step.
+OneSnapshot ==
+    \A e \in SendsOut :
+        /\ (e.route = "native") <=> (support = "native")
+        /\ e.tool_images = "withheld_unknown" => support = "unknown"
+        /\ e.tool_images = "withheld_fallback" => (support = "non_native" /\ e.route = "fallback")
+        /\ e.tool_images = "withheld_dead_end" => (support = "non_native" /\ e.route = "unavailable")
+
+\* L2: the vision tool is offered exactly on the fallback route.
+RouteModeCoherent == \A e \in SendsOut : (e.route = "fallback") <=> (e.mode # "unavailable")
+
+\* L3: native delivery and the vision tool never meet.
+NativeExcludesFallback == \A e \in SendsOut : support = "native" => (e.route = "native" /\ e.mode = "unavailable")
+
+\* L6: tool images are attached or withheld with a notice; never neither.
+NoSilentWithhold ==
+    \A e \in SendsOut : Decided # <<>> /\ (Head(Decided).tool_images <=> e.tool_images # "none")
+
+\* L6: the vision tool is required exactly while user images wait.
+RequiredWhenPending ==
+    \A e \in SendsOut : e.route = "fallback" => ((e.mode = "required") <=> Head(Decided).pending_images)
+
+\* L7: user images without a route fail the request; nothing else does.
+FailExactlyWhenUnroutable ==
+    /\ \A e \in FailsOut :
+          /\ Decided # <<>>
+          /\ Head(Decided).user_images
+          /\ (support = "unknown" \/ (support = "non_native" /\ ~Head(Decided).fallback))
+          /\ e.reason = IF support = "unknown" THEN "capability_unknown" ELSE "no_native_image"
+    /\ \A e \in SendsOut : Head(Decided).user_images => e.route # "unavailable"
+
+\* L8: the core asks for capabilities only when images wait on unknown support.
+ResolveOnlyWhenNeeded ==
+    HasKind("resolve") =>
+        /\ act.name = "RequestReady"
+        /\ support = "unknown"
+        /\ (act.req.user_images \/ act.req.tool_images)
+        /\ pending = <<act.req>>
+
+\* L9: the user hears about a down catalog only for tool images it withholds.
+NotifyOnlyWhenDown ==
+    HasKind("notify") =>
+        /\ \E e \in SendsOut : e.tool_images = "withheld_unknown"
+        /\ Head(Decided).catalog_down
+
+\* L13: a decision comes only once no reply is owed.
+DecideOnlyWhenReady ==
+    (HasKind("send") \/ HasKind("fail")) =>
+        /\ pending = <<>>
+        /\ (act.name = "RequestReady" \/ (act.name = "CapabilitiesResolved" /\ act.answered # <<>>))
+
+\* L14: a new turn, or a new process, starts clean.
+TurnResets ==
+    act.name \in {"TurnStarted", "Crash"} => (~resolved /\ ~notified /\ pending = <<>> /\ out = <<>>)
+
+\* L13: while a reply is owed, the core has asked once and decided nothing.
+PendingWaitsForReply ==
+    pending # <<>> => (resolved /\ support = "unknown" /\ (out = <<>> \/ out = <<[kind |-> "resolve"]>>))
+
+\* L8: at most one capability request per turn.
+ResolveOncePerTurn == [][(\E i \in 1..Len(out') : out'[i].kind = "resolve") => ~resolved]_vars
+
+\* L9: at most one catalog-down notice per turn.
+NotifyOncePerTurn == [][(\E i \in 1..Len(out') : out'[i].kind = "notify") => ~notified]_vars
+
+\* L10: a request delivered while a reply is owed runs nothing.
+DuplicateRequestIsQuiet == [][(act'.name = "RequestReady" /\ pending # <<>>) => out' = <<>>]_vars
+
+\* L10: a reply nothing waits for changes nothing.
+StaleReplyIsQuiet ==
+    [][(act'.name = "CapabilitiesResolved" /\ pending = <<>>) =>
+          (out' = <<>> /\ UNCHANGED <<support, resolved, notified, pending>>)]_vars
+
+\* L12: every request that waits is answered, unless its turn ends.
+Answered == (pending # <<>>) ~> (pending = <<>>)
+=============================================================================
diff --git a/tests/tla/image_route/spec/MCImageRoute.cfg b/tests/tla/image_route/spec/MCImageRoute.cfg
new file mode 100644
index 000000000..94bb4f0cb
--- /dev/null
+++ b/tests/tla/image_route/spec/MCImageRoute.cfg
@@ -0,0 +1,27 @@
+\* Every law of ImageRoute.tla over its whole state space. The model has no
+\* constants: every set it ranges over is finite by construction, so TLC
+\* checks all of it. More specific invariants come first, since TLC names the
+\* first one a state breaks.
+SPECIFICATION Spec
+INVARIANT
+    TypeOK
+    Bounded
+    VisionImpliesNative
+    UnknownNeverInline
+    OneSnapshot
+    RouteModeCoherent
+    NativeExcludesFallback
+    NoSilentWithhold
+    RequiredWhenPending
+    FailExactlyWhenUnroutable
+    ResolveOnlyWhenNeeded
+    NotifyOnlyWhenDown
+    DecideOnlyWhenReady
+    TurnResets
+    PendingWaitsForReply
+PROPERTY
+    ResolveOncePerTurn
+    NotifyOncePerTurn
+    DuplicateRequestIsQuiet
+    StaleReplyIsQuiet
+    Answered
diff --git a/tests/tla/image_route/spec/TraceImageRoute.cfg b/tests/tla/image_route/spec/TraceImageRoute.cfg
new file mode 100644
index 000000000..4712d15bd
--- /dev/null
+++ b/tests/tla/image_route/spec/TraceImageRoute.cfg
@@ -0,0 +1,30 @@
+\* Every safety law of ImageRoute, on traces of the real core. Answered is a
+\* liveness property and cannot be judged on a finite trace: here
+\* ConformsToSpec makes each reply clear the request it answers, and
+\* MCImageRoute.cfg proves Answered over the whole model. TraceData.tla is
+\* generated next to this file for each run.
+SPECIFICATION TraceSpec
+CHECK_DEADLOCK FALSE
+INVARIANT
+    StartsAtInit
+    TypeOK
+    Bounded
+    VisionImpliesNative
+    UnknownNeverInline
+    OneSnapshot
+    RouteModeCoherent
+    NativeExcludesFallback
+    NoSilentWithhold
+    RequiredWhenPending
+    FailExactlyWhenUnroutable
+    ResolveOnlyWhenNeeded
+    NotifyOnlyWhenDown
+    DecideOnlyWhenReady
+    TurnResets
+    PendingWaitsForReply
+PROPERTY
+    ResolveOncePerTurn
+    NotifyOncePerTurn
+    DuplicateRequestIsQuiet
+    StaleReplyIsQuiet
+    ConformsToSpec
diff --git a/tests/tla/image_route/spec/TraceImageRoute.tla b/tests/tla/image_route/spec/TraceImageRoute.tla
new file mode 100644
index 000000000..b4fd9891a
--- /dev/null
+++ b/tests/tla/image_route/spec/TraceImageRoute.tla
@@ -0,0 +1,76 @@
+--------------------------- MODULE TraceImageRoute ---------------------------
+(***************************************************************************)
+(* Checks traces the real core produced against ImageRoute.                *)
+(*                                                                         *)
+(* tests/tla/drivers/image_route/code-to-spec.ts runs event sequences,     *)
+(* with crashes, duplicates, stale replies, and catalog outages, through   *)
+(* the harness around src/core/images/image_route.zig and writes each run  *)
+(* as one sequence of states into TraceData.tla. Each state is what the    *)
+(* core showed (abstract(state) and the effects of the step) plus the      *)
+(* event the driver sent.                                                  *)
+(*                                                                         *)
+(* TLC walks every trace. ConformsToSpec holds when every recorded step is *)
+(* a step of ImageRoute's Next, so each trace is a behavior of the model;  *)
+(* the law names below re-export the model's laws, checked on what the     *)
+(* code did.                                                               *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, TraceData
+
+VARIABLES support, resolved, notified, pending, out, act, trace, at
+
+IR == INSTANCE ImageRoute
+
+vars == <<support, resolved, notified, pending, out, act>>
+
+Load(s) ==
+    /\ support = s.support
+    /\ resolved = s.resolved
+    /\ notified = s.notified
+    /\ pending = s.pending
+    /\ out = s.out
+    /\ act = s.act
+
+LoadNext(s) ==
+    /\ support' = s.support
+    /\ resolved' = s.resolved
+    /\ notified' = s.notified
+    /\ pending' = s.pending
+    /\ out' = s.out
+    /\ act' = s.act
+
+TraceInit == trace \in 1..Len(Traces) /\ at = 1 /\ Load(Traces[trace][1])
+
+TraceNext ==
+    /\ at < Len(Traces[trace])
+    /\ at' = at + 1
+    /\ trace' = trace
+    /\ LoadNext(Traces[trace][at + 1])
+
+TraceSpec == TraceInit /\ [][TraceNext]_<<vars, trace, at>>
+
+\* Every trace starts where the model starts.
+StartsAtInit == at = 1 => IR!Init
+
+\* Every recorded step is a step of the model.
+ConformsToSpec == [][IR!Next]_vars
+
+TypeOK == IR!TypeOK
+Bounded == IR!Bounded
+VisionImpliesNative == IR!VisionImpliesNative
+UnknownNeverInline == IR!UnknownNeverInline
+OneSnapshot == IR!OneSnapshot
+RouteModeCoherent == IR!RouteModeCoherent
+NativeExcludesFallback == IR!NativeExcludesFallback
+NoSilentWithhold == IR!NoSilentWithhold
+RequiredWhenPending == IR!RequiredWhenPending
+FailExactlyWhenUnroutable == IR!FailExactlyWhenUnroutable
+ResolveOnlyWhenNeeded == IR!ResolveOnlyWhenNeeded
+NotifyOnlyWhenDown == IR!NotifyOnlyWhenDown
+DecideOnlyWhenReady == IR!DecideOnlyWhenReady
+TurnResets == IR!TurnResets
+PendingWaitsForReply == IR!PendingWaitsForReply
+ResolveOncePerTurn == IR!ResolveOncePerTurn
+NotifyOncePerTurn == IR!NotifyOncePerTurn
+DuplicateRequestIsQuiet == IR!DuplicateRequestIsQuiet
+StaleReplyIsQuiet == IR!StaleReplyIsQuiet
+=============================================================================