updates

ober

834bc53ffca7e6c8f0ea08646f88297d454442bc

diff --git a/docs/FORGE.md b/docs/FORGE.md
index d4e1fd0..f98fb63 100644
--- a/docs/FORGE.md
+++ b/docs/FORGE.md
@@ -33,7 +33,7 @@ see [`FORGE_PORT_PLAN.md`](FORGE_PORT_PLAN.md).
 | `/forge verify` | Describe + self-test the verify-gate (ATLAS verify + repair). |
 | `/forge bestofk` · `/forge best-of-k` | Describe + self-test best-of-k diverse generation. |
 | `/forge breaker` · `/forge no-progress` | Describe + self-test the no-progress loop breaker. |
-| `/forge run <task>` | Verify-gated coding on the **live** model (edit → verify → done). |
+| `/forge run [opts] <task>` | Verify-gated coding on the **live** model (edit → verify → done). Options: `--verify`, `--bestof`, `--cwd`, `--write-scope`. |
 
 The `workflow` / `proxy` / `ablation` / `verify` / `bestofk` / `breaker`
 self-tests run real code against scripted inputs (no live model), so they double
@@ -52,7 +52,7 @@ HTTP endpoint. See [The proxy](#the-openai-compatible-proxy) below.
 ### `jcode verified` (subcommand)
 
 ```bash
-jcode verified "<task>" [--bestof K] [--verify CMD] [--cwd DIR]
+jcode verified "<task>" [--bestof K] [--verify CMD] [--cwd DIR] [--write-scope PATHS]
 ```
 
 Runs the [verify-gate](#verify-gate) on the live model — edit → run `CMD` →
@@ -141,12 +141,18 @@ output is fed back as a tool result for the model to repair. The run ends
 
 ```bash
 jcode verified "make the failing parser test pass" --verify "make test"
+jcode verified "add static Tetris board" --verify "make tetris-static-contract" \
+  --write-scope "src/tetris/,tests/tetris/" --bestof 2
 ```
 
 Also available interactively as `/forge run <task>`. The gate holds even when an
 earlier candidate looked plausible: the run finishes after a *passing* verify,
 not the first edit.
 
+The same runner is exposed as the `verified` tool, so a skill such as
+`/strict-ladder` can launch one scoped rung from inside an ordinary jcode
+session without requiring project-specific `jcode.json` agent variants.
+
 ### Best-of-k
 
 `core/best-of-k.ss` generates `K` diverse candidates (varied sampling), verifies
diff --git a/docs/README.md b/docs/README.md
index 5015c6f..69ff018 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -18,6 +18,9 @@ elevator pitch.
   `doc-explorer`, `implementer`), enforced write scopes, per-agent model
   routing, the gated BLUEPRINT → EXECUTE protocol, and the plan-lifecycle
   skills (`/create-plan` … `/resume-plan`).
+- **[Strict ladder howto](strict-ladder.md)** — practical workflow for using
+  `/strict-ladder`, runtime `write_scope`, and scoped verified runs to make hard
+  local-model tasks succeed one rung at a time.
 - **[TUI](tui.md)** — the terminal UI: layout, the full keybinding table,
   themes, and the markdown / syntax / diff renderers.
 
diff --git a/docs/agents.md b/docs/agents.md
index e812f12..3268161 100644
--- a/docs/agents.md
+++ b/docs/agents.md
@@ -38,6 +38,7 @@ You can also steer explicitly — these phrasings work well:
 › use a delegate to find every caller of refresh-system-prompt
 › have the implementer blueprint this change first, then show me the plan
 › spawn doc-explorer to write docs/modules/provider.md
+› use implementer with write_scope "src/tetris/,tests/tetris/" to blueprint the next rung
 ```
 
 `/agents` lists the roles (and any variants you configured) at any time.
@@ -66,6 +67,23 @@ blueprint is wrong, reply with objections in another BLUEPRINT call on the
 same `task_id` instead of approving.
 
 Task sessions live in memory for the jcode process (most recent 32 kept).
+Runtime `write_scope` sticks to the resumable session, so an EXECUTE call cannot
+silently widen a scoped BLUEPRINT session.
+
+## Runtime Write Scopes
+
+For portable strict control, pass `write_scope` on the task itself instead of
+creating project-specific agent variants:
+
+```text
+task(agent: "delegate", write_scope: "none", prompt: "Inspect the Qt examples...")
+task(agent: "implementer", task_id: "rung-2", write_scope: "src/tetris/,tests/tetris/",
+     prompt: "MODE: BLUEPRINT\nImplement the static-board rung...")
+```
+
+Values are `"none"`, `"all"`, or comma-separated relative path prefixes. Scopes
+only narrow: a `delegate` remains read-only even if a wider scope is requested,
+and nested/resumed tasks cannot escape their previous scope.
 
 ## Plan workflow: multi-session work that survives restarts
 
diff --git a/docs/cli.md b/docs/cli.md
index 47ed4e6..e14d68e 100644
--- a/docs/cli.md
+++ b/docs/cli.md
@@ -78,12 +78,14 @@ jcode connect HOST:PORT --host NAME [--token T] # controller side
 ### `verified`
 
 ```
-jcode verified "<task>" [--bestof K] [--verify CMD] [--cwd DIR]
+jcode verified "<task>" [--bestof K] [--verify CMD] [--cwd DIR] [--write-scope PATHS]
 ```
 
 Runs an edit→verify→done loop on the live model: it edits, runs `--verify CMD`
 (e.g. `make test`), and only declares success once the command passes —
-optionally drawing the best of `K` diverse candidates. See
+optionally drawing the best of `K` diverse candidates. `--write-scope` accepts
+`all`, `none`, or comma-separated path prefixes such as `src/tetris/,tests/`.
+See
 [FORGE.md](FORGE.md#verify-gate).
 
 ## Slash commands (interactive)
@@ -125,6 +127,12 @@ Available in the REPL and TUI.
 | `/skills` | List built-in and user skills. |
 | `/<skill-name> [args]` | Run a skill (built-in or a user `SKILL.md`). |
 
+Useful built-in workflow skill:
+
+| Command | Effect |
+|---|---|
+| `/strict-ladder <goal>` | Break a hard local-model task into scoped verified rungs using agents plus the `verified` tool. |
+
 ### `/forge` — reliability control
 
 | Command | Effect |
@@ -138,7 +146,7 @@ Available in the REPL and TUI.
 | `/forge verify` | Describe + self-test the verify-gate. |
 | `/forge bestofk` · `/forge best-of-k` | Describe + self-test best-of-k generation. |
 | `/forge breaker` · `/forge no-progress` | Describe + self-test the no-progress breaker. |
-| `/forge run <task>` | Verify-gated coding on the live model. |
+| `/forge run [opts] <task>` | Verify-gated coding on the live model. Supports `--verify`, `--bestof`, `--cwd`, and `--write-scope`. |
 
 Each `/forge` self-test runs real code against scripted inputs (no live model),
 so it doubles as a smoke test. Full semantics in [FORGE.md](FORGE.md).
diff --git a/docs/getting-started.md b/docs/getting-started.md
index b79e888..f704bf5 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -105,7 +105,8 @@ make android          # build the thin-client APK in Termux (see docs/remote.md)
   "model": "claude-sonnet-4-20250514",
   "providers": {
     "anthropic": { "api_key": "sk-ant-..." },
-    "mlx":       {}
+    "mlx":       {},
+    "mlx2":      { "base_url": "http://192.168.6.84:8000/v1" }
   },
   "mcpServers": {
     "jerboa": { "command": "jerboa-mcp", "args": [] }
@@ -119,6 +120,8 @@ make android          # build the thin-client APK in Termux (see docs/remote.md)
   `--provider` / `--model`, or live with `/provider` / `/model`.
 - **`providers.<name>.api_key`** — a plaintext key (lowest precedence; prefer
   the encrypted store or env vars).
+- **`providers.mlx*` / `providers.ollama*`** — keyless local-provider aliases.
+  For example, `mlx2` can point at a second MLX server via `base_url`.
 - **`mcpServers`** — external [MCP](tools.md#mcp-tools) servers to launch.
 
 > ⚠️ A `jcode.json` in the project root holds live keys. It is git-ignored —
diff --git a/docs/providers.md b/docs/providers.md
index 4565beb..1b14ce0 100644
--- a/docs/providers.md
+++ b/docs/providers.md
@@ -100,6 +100,21 @@ Serve a model with `mlx_lm.server` (default `http://127.0.0.1:8080/v1`), then:
 MLX gets sane sampling defaults automatically (see below) — without them, small
 quantized models loop on greetings or truncate XML mid-stream.
 
+You can configure multiple MLX endpoints by adding provider names that start
+with `mlx`; they appear in the provider picker, require no API key, and use the
+same OpenAI-compatible MLX request path:
+
+```json
+{
+  "provider": "mlx2",
+  "model": "/path/to/your/mlx-model-dir",
+  "providers": {
+    "mlx":  { "base_url": "http://127.0.0.1:8000/v1" },
+    "mlx2": { "base_url": "http://192.168.6.84:8000/v1" }
+  }
+}
+```
+
 ### Prompt caching
 
 `jcode` uses provider-specific cache controls instead of spraying one field at
diff --git a/docs/tools.md b/docs/tools.md
index 8e41d4f..3c51166 100644
--- a/docs/tools.md
+++ b/docs/tools.md
@@ -46,6 +46,7 @@ page is the catalogue plus the safety model that wraps every call.
 | `todowrite` | Update the visible task plan in the TUI sidebar | `todos[]` of `{content,status,priority?}` |
 | `batch` | Run several tool calls in parallel (green threads) | `calls[]` of `{tool,args}` |
 | `task` | Spawn a sub-agent with its own context | `description`, `prompt`, `system?`, `agent?`, `task_id?` |
+| `verified` | Run a scoped ATLAS edit→verify→repair sub-run | `task`, `verify_command?`, `cwd?`, `best_of?`, `write_scope?`, `max_iterations?` |
 | `repomap` | Condensed project map (top files by PageRank + key symbols) | *(none)* |
 
 `todowrite` is for multi-step work. The model sends the complete current list
@@ -74,8 +75,15 @@ Write scopes are enforced in the tool layer (`agent-defs.ss` +
 `file.ss`/`apply-patch.ss`), not just by prompt — and nesting can only
 *narrow*: a scoped sub-agent spawning another task can never widen access.
 
-Variants live in `jcode.json` under `"agents"`; `extends` inherits a
-built-in's prompt/scope while pinning a different model:
+For portable one-off control, pass `write_scope` directly to the `task` tool:
+`"none"`, `"all"`, or comma-separated path prefixes such as
+`"src/tetris/,tests/tetris/"`. Runtime scopes can only narrow the named
+agent's configured scope, and resumable `task_id` sessions keep their scope
+across BLUEPRINT → EXECUTE.
+
+Variants still live in `jcode.json` under `"agents"` when you want a reusable
+role. `extends` inherits a built-in's prompt/scope while pinning a different
+model:
 
 ```json
 "agents": {
@@ -102,6 +110,25 @@ The plan-lifecycle skills (`/skills`: `create-plan`, `resume-plan`,
 `execute-work-package`, `review-plan`, `generate-handover`) drive this
 protocol against persistent `plans/<name>/` artifacts that survive sessions.
 
+### Verify-gated sub-runs (`verified`)
+
+The `verified` tool gives skills and agents the same ATLAS gate as
+`jcode verified` and `/forge run`: the sub-run receives only
+`read`/`edit`/`verify`/`done`, must pass `verify_command` before `done`, and
+can be restricted with a per-call `write_scope`.
+
+Use it from skills for strict agentic steps:
+
+```json
+{
+  "task": "Implement rung 2: draw a static Qt board only.",
+  "verify_command": "make tetris-static-contract",
+  "cwd": ".",
+  "best_of": 2,
+  "write_scope": "src/tetris/,tests/tetris/"
+}
+```
+
 ## The safety model
 
 Four layers gate what the agent can do. They apply to every call regardless of
@@ -114,7 +141,7 @@ removed from the schema the model sees *and* rejected at execution time; in
 **BUILD** mode everything is available. The write set is:
 
 ```
-write  edit  edit_block  multi-edit  patch  apply_patch  bash  git_commit
+write  edit  edit_block  multi-edit  patch  apply_patch  bash  git_commit  verified
 ```
 
 Switch with `/plan` · `/build` or **Shift-Tab** in the TUI.
@@ -138,10 +165,14 @@ installed.
 The external-LLM sandbox is tight by design: it can read system roots, write
 only `cwd` / `/tmp` / the chosen provider's auth dir (`~/.claude`, `~/.gemini`,
 `~/.codex`, `~/.config/opencode`, **`~/.grok`**), and exec only from standard
-bin paths. Every other provider's credentials plus `~/.ssh`, `~/.aws`,
-`~/.gnupg`, `~/.netrc`, `~/.config/gh`, `~/.docker` are denied. The deny list is
-symmetric: when the chosen CLI is `claude`, `~/.grok` is denied; when the chosen
-CLI is `grok`, `~/.claude` is denied; no CLI can read another's bearer token.
+bin paths plus the selected CLI's resolved executable path. Symlinked CLIs and
+Node shebang wrappers are resolved before launch so `sandbox-exec` receives an
+absolute argv and the real binary/interpreter path is allowed. The child gets a
+minimal environment (`PATH`, `HOME`, locale, temp/XDG basics), not ambient API
+keys. Every other provider's credentials plus `~/.ssh`, `~/.aws`, `~/.gnupg`,
+`~/.netrc`, `~/.config/gh`, `~/.docker` are denied. The deny list is symmetric:
+when the chosen CLI is `claude`, `~/.grok` is denied; when the chosen CLI is
+`grok`, `~/.claude` is denied; no CLI can read another's bearer token.
 
 ### 4. Generated-artifact protection
 
diff --git a/src/jcode/core/agent-defs.ss b/src/jcode/core/agent-defs.ss
index 270c824..ed85468 100644
--- a/src/jcode/core/agent-defs.ss
+++ b/src/jcode/core/agent-defs.ss
@@ -148,12 +148,19 @@
 ;; ── Config merge ─────────────────────────────────────────────────────
 
 (def (parse-write-scope v)
-  "Normalize a config write_scope value: \"all\" -> #f (unrestricted),
-   \"none\" -> 'none, list of strings -> that list. Anything else -> #f."
+  "Normalize a write_scope value: \"all\" -> #f (unrestricted),
+   \"none\" -> 'none, list of strings -> that list, comma-separated string
+   -> list of path prefixes. Anything else -> #f."
   (cond
     ((equal? v "none") 'none)
     ((equal? v "all") #f)
-    ((and (list? v) (pair? v) (string? (car v))) v)
+    ((string? v)
+     (let ((parts (filter (lambda (s) (not (string=? s "")))
+                          (map string-trim (string-split v ",")))))
+       (if (null? parts) #f parts)))
+    ((and (list? v) (pair? v) (string? (car v)))
+     (filter (lambda (s) (and (string? s) (not (string=? s ""))))
+             (map string-trim v)))
     (else #f)))
 
 (def (parse-agent-def name spec base)
@@ -235,6 +242,17 @@
       (substring p (string-length cwd) (string-length p))
       p)))
 
+(def (scope-entry-allows? prefix rel)
+  "Prefix match with path-boundary semantics. A scope entry `src` allows
+   `src` and `src/foo.ss`, but not `src-old/foo.ss`; an entry ending in `/`
+   allows only descendants under that directory."
+  (cond
+    ((string=? prefix rel) #t)
+    ((string-suffix? "/" prefix)
+     (string-prefix? prefix rel))
+    (else
+      (string-prefix? (string-append prefix "/") rel))))
+
 (def (write-scope-allows? scope path)
   "Does SCOPE permit writing PATH? #f scope = everything; 'none = nothing;
    list = path must fall under one of the prefixes."
@@ -247,7 +265,7 @@
         (let loop ((prefixes scope))
           (cond
             ((null? prefixes) #f)
-            ((string-prefix? (car prefixes) rel) #t)
+            ((scope-entry-allows? (car prefixes) rel) #t)
             (else (loop (cdr prefixes)))))))))
 
 (def (write-scope-intersect parent child)
@@ -265,7 +283,7 @@
                       (let loop ((ps parent))
                         (cond
                           ((null? ps) #f)
-                          ((string-prefix? (car ps) c) #t)
+                          ((scope-entry-allows? (car ps) c) #t)
                           (else (loop (cdr ps))))))
                     child)))
         (if (null? kept) 'none kept)))))
diff --git a/src/jcode/core/agent.ss b/src/jcode/core/agent.ss
index c7102ac..059c7c0 100644
--- a/src/jcode/core/agent.ss
+++ b/src/jcode/core/agent.ss
@@ -56,6 +56,7 @@
 
 (def *small-context-tools*
   '("todowrite"
+    "verified"
     "apply_patch" "bash" "batch" "edit" "edit_block" "multi-edit" "patch"
     "read" "write" "ls" "glob" "grep" "repomap"
     "git_status" "git_diff" "git_log" "git_show" "git_commit"
diff --git a/src/jcode/core/builtin-skills.ss b/src/jcode/core/builtin-skills.ss
index 742007c..d7a740d 100644
--- a/src/jcode/core/builtin-skills.ss
+++ b/src/jcode/core/builtin-skills.ss
@@ -219,6 +219,49 @@
 "\n"
 "Never git-commit from the sub-agent; commits belong to the user.\n"))
 
+(def *strict-ladder-prompt*
+  (string-append
+"Run a portable strict ladder for a hard agentic coding goal. This workflow is\n"
+"for local/small models and fragile stacks: make success mechanical by using\n"
+"small rungs, scoped writes, and verifier-owned evidence.\n"
+"\n"
+"Core rules:\n"
+"- Do not attempt the final app directly. Split the goal into 3-8 increasing\n"
+"  rungs, each with one concrete verifier command.\n"
+"- Use `task` with agent=\"delegate\" and write_scope=\"none\" for read-only\n"
+"  discovery before editing. Ask it for exact files, APIs, and risks.\n"
+"- For documentation/planning, use agent=\"doc-explorer\" with a runtime\n"
+"  write_scope under plans/ and docs/.\n"
+"- For implementation, prefer the `verified` tool. Always set\n"
+"  verify_command, cwd, best_of, and write_scope. The write_scope must be the\n"
+"  smallest comma-separated path list that can satisfy the rung.\n"
+"- A rung is done only when the verifier passes. If verify fails, repair inside\n"
+"  the same verified run; do not mark success from prose.\n"
+"- GUI rungs need verifier-owned screenshots, snapshot checks, or pixel/state\n"
+"  evidence. A screenshot existing is not enough.\n"
+"- Only one rung may be active at a time. Do not run parallel writers against\n"
+"  the same tree.\n"
+"\n"
+"Recommended loop:\n"
+"1. Use todowrite to list discovery, ladder, current rung, verification, docs.\n"
+"2. Delegate discovery: repo structure, available GUI APIs, build commands,\n"
+"   and the smallest useful first rung.\n"
+"3. Write/update plans/<short-name>/plan.md and phases if the goal is more\n"
+"   than one rung. Keep it concise.\n"
+"4. For the current rung, call `verified` with:\n"
+"   - task: exact deliverable for this rung only\n"
+"   - verify_command: the behavior verifier for this rung\n"
+"   - cwd: repository root or relevant package root\n"
+"   - best_of: 1 for easy rungs, 2-3 for hard rungs\n"
+"   - write_scope: allowed source/test/docs paths only\n"
+"5. Inspect the verified result and changed files. If needed, create a smaller\n"
+"   next rung or strengthen the verifier before proceeding.\n"
+"6. Update the plan/docs with what passed, what failed, and the next rung.\n"
+"\n"
+"When dynamic path scope is missing from a requested operation, stop and ask\n"
+"for a narrower allowed-path list. Do not fall back to broad unrestricted\n"
+"edits unless the user explicitly approves.\n"))
+
 (def *builtin-skills*
   (list
     (cons "create-plan"          *create-plan-prompt*)
@@ -226,7 +269,8 @@
     (cons "generate-handover"    *generate-handover-prompt*)
     (cons "resume-plan"          *resume-plan-prompt*)
     (cons "review-plan"          *review-plan-prompt*)
-    (cons "save-discoveries"     *save-discoveries-prompt*)))
+    (cons "save-discoveries"     *save-discoveries-prompt*)
+    (cons "strict-ladder"        *strict-ladder-prompt*)))
 
 (def (builtin-skill name)
   "Return the prompt text for the builtin skill NAME, or #f if not builtin."
diff --git a/src/jcode/core/config.ss b/src/jcode/core/config.ss
index fa54f9f..eab66e9 100644
--- a/src/jcode/core/config.ss
+++ b/src/jcode/core/config.ss
@@ -84,6 +84,7 @@
                         (call-with-input-file (car paths) read-json))))
                (else (loop (cdr paths) acc)))))
          (config (merge-env-config file-config)))
+    (register-configured-providers! config)
     (*config* config)
     config))
 
diff --git a/src/jcode/core/message.ss b/src/jcode/core/message.ss
index 2a84cf3..6e44415 100644
--- a/src/jcode/core/message.ss
+++ b/src/jcode/core/message.ss
@@ -93,6 +93,22 @@
       (hash-put! ht "tool_call_id" (message-tool-call-id msg)))
     ht))
 
+(def (assoc-args? args)
+  (and (pair? args) (pair? (car args))))
+
+(def (assoc-args->hash args)
+  (let ((ht (make-hash-table)))
+    (for-each (lambda (kv) (hash-put! ht (car kv) (cdr kv))) args)
+    ht))
+
+(def (tool-call-arguments->json-string args)
+  (cond
+    ((string? args) args)
+    ((hash-table? args) (json-object->string args))
+    ((null? args) "{}")
+    ((assoc-args? args) (json-object->string (assoc-args->hash args)))
+    (else (json-object->string args))))
+
 (def (tool-call->json tc)
   (let ((ht (make-hash-table))
         (fn (make-hash-table)))
@@ -100,9 +116,7 @@
     (hash-put! ht "type" "function")
     (hash-put! fn "name" (tool-call-name tc))
     (hash-put! fn "arguments"
-      (if (string? (tool-call-arguments tc))
-        (tool-call-arguments tc)
-        (json-object->string (tool-call-arguments tc))))
+      (tool-call-arguments->json-string (tool-call-arguments tc)))
     (hash-put! ht "function" fn)
     ht))
 
diff --git a/src/jcode/core/models.ss b/src/jcode/core/models.ss
index 239c82c..4f4aafb 100644
--- a/src/jcode/core/models.ss
+++ b/src/jcode/core/models.ss
@@ -5,6 +5,9 @@
 (export provider-models
         filter-models
         all-providers
+        register-configured-providers!
+        provider-kind
+        local-provider?
         provider-display-name
         provider-default-model
         provider-default-models
@@ -28,32 +31,72 @@
 
 ;; ---- Provider metadata ----
 
-(def (all-providers)
+(def *builtin-providers*
   ;; "grok" is the Grok CLI session-token provider (~/.grok/auth.json), kept
   ;; distinct from "xai" (api.x.ai API-key) and "groq" (Groq Inc., separate).
   '("anthropic" "openai" "openrouter" "deepseek" "google" "ollama" "mlx"
     "xai" "grok" "groq" "mistral" "together" "cerebras" "perplexity"))
 
-(def (provider-display-name p)
-  (case (string->symbol p)
-    ((anthropic)   "Anthropic")
-    ((openai)      "OpenAI")
-    ((openrouter)  "OpenRouter")
-    ((deepseek)    "DeepSeek")
-    ((google)      "Google")
-    ((ollama)      "Ollama (local)")
-    ((mlx)         "MLX (local)")
-    ((xai)         "xAI (Grok)")
-    ((grok)        "Grok CLI")
-    ((groq)        "Groq")
-    ((mistral)     "Mistral")
-    ((together)    "Together AI")
-    ((cerebras)    "Cerebras")
-    ((perplexity)  "Perplexity")
+(def *configured-providers* (make-parameter '()))
+
+(def (register-configured-providers! config)
+  "Record provider names from the loaded config so UI pickers include aliases
+   such as mlx2. Built-ins keep their fixed order; configured extras are sorted
+   for deterministic display."
+  (let ((providers (and (hash-table? config) (hash-get config "providers"))))
+    (*configured-providers*
+      (if (hash-table? providers)
+        (sort string<? (filter string? (hash-keys providers)))
+        '()))))
+
+(def (append-missing base extras)
+  (let loop ((xs extras) (acc base))
+    (cond
+      ((null? xs) acc)
+      ((member (car xs) acc) (loop (cdr xs) acc))
+      (else (loop (cdr xs) (append acc (list (car xs))))))))
+
+(def (all-providers)
+  (append-missing *builtin-providers* (*configured-providers*)))
+
+(def (provider-kind p)
+  "Return the built-in provider behavior used by provider name P. Names like
+   mlx2 are treated as MLX aliases so multiple local/remote MLX servers can be
+   configured independently."
+  (cond
+    ((member p *builtin-providers*) p)
+    ((string-prefix? "mlx" p) "mlx")
+    ((string-prefix? "ollama" p) "ollama")
     (else p)))
 
+(def (local-provider? p)
+  (let ((kind (provider-kind p)))
+    (or (equal? kind "mlx")
+        (equal? kind "ollama"))))
+
+(def (provider-display-name p)
+  (let* ((kind (provider-kind p))
+         (base
+           (case (string->symbol kind)
+             ((anthropic)   "Anthropic")
+             ((openai)      "OpenAI")
+             ((openrouter)  "OpenRouter")
+             ((deepseek)    "DeepSeek")
+             ((google)      "Google")
+             ((ollama)      "Ollama (local)")
+             ((mlx)         "MLX (local)")
+             ((xai)         "xAI (Grok)")
+             ((grok)        "Grok CLI")
+             ((groq)        "Groq")
+             ((mistral)     "Mistral")
+             ((together)    "Together AI")
+             ((cerebras)    "Cerebras")
+             ((perplexity)  "Perplexity")
+             (else p))))
+    (if (equal? p kind) base (format "~a (~a)" base p))))
+
 (def (provider-default-model provider)
-  (case (string->symbol provider)
+  (case (string->symbol (provider-kind provider))
     ((anthropic)   "claude-sonnet-4-20250514")
     ((openai)      "gpt-4o")
     ((openrouter)  "anthropic/claude-sonnet-4")
@@ -100,7 +143,7 @@
       (filter (lambda (m) (model-search-hit? m terms)) models))))
 
 (def (provider-default-models provider)
-  (case (string->symbol provider)
+  (case (string->symbol (provider-kind provider))
     ((anthropic)   anthropic-models)
     ((openai)      openai-models)
     ((deepseek)    deepseek-models)
diff --git a/src/jcode/core/verified-run.ss b/src/jcode/core/verified-run.ss
index 5672c91..e52c63b 100644
--- a/src/jcode/core/verified-run.ss
+++ b/src/jcode/core/verified-run.ss
@@ -22,6 +22,7 @@
 (import :std/os/aproc
         :std/misc/string
         :std/misc/ports
+        :jcode/core/agent-defs
         :jcode/core/workflow
         :jcode/core/verified
         :jcode/core/best-of-k
@@ -65,47 +66,1206 @@
 (def (arg-ref args key default)
   (let ((p (assoc key args))) (if p (cdr p) default)))
 
+(def (arg-int args key default)
+  (let ((v (arg-ref args key default)))
+    (cond
+      ((integer? v) v)
+      ((number? v) (inexact->exact (floor v)))
+      ((string? v) (or (string->number v) default))
+      (else default))))
+
 (def (abs-path cwd path)
   (if (and (> (string-length path) 0) (char=? (string-ref path 0) #\/))
     path
     (string-append cwd "/" path)))
 
+(def current-pending-ss-create-repair
+  (make-parameter #f))
+
+(def current-after-failed-verify?
+  (make-parameter #f))
+
+(def current-inspections-after-failed-verify
+  (make-parameter 0))
+
+(def inspection-after-failed-verify-limit 12)
+
+(def (reset-failed-verify-inspections!)
+  (current-after-failed-verify? #f)
+  (current-inspections-after-failed-verify 0))
+
+(def (record-verify-result! result)
+  (current-after-failed-verify? (not (and (pair? result) (car result))))
+  (current-inspections-after-failed-verify 0)
+  result)
+
+(def (note-inspection-after-failed-verify! who)
+  (when (current-after-failed-verify?)
+    (let ((n (+ (current-inspections-after-failed-verify) 1)))
+      (current-inspections-after-failed-verify n)
+      (when (> n inspection-after-failed-verify-limit)
+        (error who
+               "inspection limit reached after failed verify. Stop inspecting and call line_edit, replace_range, replace_def, or edit with the concrete repair now.")))))
+
+(def (same-verified-path? cwd a b)
+  (and (string? a)
+       (string? b)
+       (string=? (abs-path cwd a) (abs-path cwd b))))
+
+(def (ss-repair-instruction path)
+  (string-append
+    "The file was not written. Next tool call must be edit with complete corrected contents for "
+    path
+    ". Do not call run/list/read/balance/verify until that file exists."))
+
+(def (pending-ss-create-repair-message cwd)
+  (let ((path (current-pending-ss-create-repair)))
+    (and path
+         (not (file-exists? (abs-path cwd path)))
+         (string-append
+           "A previous edit for " path
+           " was rejected by the Jerboa syntax guard and the file still does not exist. "
+           (ss-repair-instruction path)))))
+
+(def (clear-pending-ss-create-repair! cwd path)
+  (let ((pending (current-pending-ss-create-repair)))
+    (when (and pending
+               (same-verified-path? cwd pending path)
+               (file-exists? (abs-path cwd path)))
+      (current-pending-ss-create-repair #f))))
+
+(def (absolute-path-string? path)
+  (and (string? path)
+       (> (string-length path) 0)
+       (char=? (string-ref path 0) #\/)))
+
+(def (path-components path)
+  (filter (lambda (part) (not (string=? part "")))
+          (string-split path #\/)))
+
+(def (components-prefix? prefix comps)
+  (cond
+    ((null? prefix) #t)
+    ((null? comps) #f)
+    ((string=? (car prefix) (car comps))
+     (components-prefix? (cdr prefix) (cdr comps)))
+    (else #f)))
+
+(def (drop-components comps n)
+  (if (or (<= n 0) (null? comps))
+    comps
+    (drop-components (cdr comps) (- n 1))))
+
+(def (normalize-components comps)
+  (let loop ((rest comps) (stack '()) (escaped? #f))
+    (cond
+      ((null? rest) (values escaped? (reverse stack)))
+      ((or (string=? (car rest) "") (string=? (car rest) "."))
+       (loop (cdr rest) stack escaped?))
+      ((string=? (car rest) "..")
+       (if (null? stack)
+         (loop (cdr rest) stack #t)
+         (loop (cdr rest) (cdr stack) escaped?)))
+      (else
+       (loop (cdr rest) (cons (car rest) stack) escaped?)))))
+
+(def (components->relative comps)
+  (if (null? comps) "." (string-join comps "/")))
+
+(def (normalize-relative-scope path)
+  (let-values (((escaped? comps) (normalize-components (path-components path))))
+    (let ((rel (components->relative comps)))
+      (if escaped?
+        (string-append "../" rel)
+        rel))))
+
+(def (scope-path cwd path)
+  (cond
+    ((not (string? path)) path)
+    ((absolute-path-string? path)
+     (let ((cwd-comps (path-components cwd))
+           (path-comps (path-components path)))
+       (if (components-prefix? cwd-comps path-comps)
+         (normalize-relative-scope
+           (components->relative
+             (drop-components path-comps (length cwd-comps))))
+         path)))
+    (else
+     (normalize-relative-scope path))))
+
+(def (absolute-components->path comps)
+  (string-append "/" (string-join comps "/")))
+
+(def (symlink-path? path)
+  (and (file-exists? path) (file-symbolic-link? path)))
+
+(def (path-has-symlink-component? cwd path)
+  (let* ((target-comps (path-components (abs-path cwd path)))
+         (cwd-comps (path-components cwd))
+         (under-cwd? (components-prefix? cwd-comps target-comps))
+         (seen0 (if under-cwd? cwd-comps '()))
+         (rest0 (if under-cwd?
+                  (drop-components target-comps (length cwd-comps))
+                  target-comps)))
+    (let loop ((seen seen0) (rest rest0))
+      (cond
+        ((null? rest) #f)
+        (else
+         (let* ((next-seen (append seen (list (car rest))))
+                (candidate (absolute-components->path next-seen)))
+           (if (symlink-path? candidate)
+             #t
+             (loop next-seen (cdr rest)))))))))
+
+(def (mkdir-p dir)
+  (when (and dir (not (equal? dir "")) (not (file-exists? dir)))
+    (let ((parent (path-directory dir)))
+      (when (and parent (not (equal? parent dir)) (not (file-exists? parent)))
+        (mkdir-p parent)))
+    (mkdir dir)))
+
+(def (drop-up-to xs n)
+  (let loop ((xs xs) (n n))
+    (cond
+      ((or (<= n 0) (null? xs)) xs)
+      (else (loop (cdr xs) (- n 1))))))
+
+(def (take-up-to xs n)
+  (let loop ((xs xs) (n n) (acc '()))
+    (cond
+      ((or (<= n 0) (null? xs)) (reverse acc))
+      (else (loop (cdr xs) (- n 1) (cons (car xs) acc))))))
+
+(def (last-up-to xs n)
+  (let ((len (length xs)))
+    (drop-up-to xs (max 0 (- len n)))))
+
+(def (slice-content content args)
+  (let* ((line-no (arg-int args "line" 0))
+         (start-line (arg-int args "start" 0))
+         (end-line (arg-int args "end" 0))
+         (range-start (cond
+                        ((> start-line 0) start-line)
+                        ((> line-no 0) line-no)
+                        (else 0)))
+         (offset (if (> range-start 0)
+                   (- range-start 1)
+                   (arg-int args "offset" 0)))
+         (limit (cond
+                  ((and (> range-start 0) (>= end-line range-start))
+                   (+ (- end-line range-start) 1))
+                  ((> range-start 0) 1)
+                  (else (arg-int args "limit" 0)))))
+    (if (and (= offset 0) (<= limit 0))
+      content
+      (let* ((lines (string-split content #\newline))
+             (tail (drop-up-to lines (max 0 offset)))
+             (shown (if (> limit 0) (take-up-to tail limit) tail)))
+        (string-join shown "\n")))))
+
 (def (do-read args cwd)
+  (note-inspection-after-failed-verify! 'read)
   (let ((path (arg-ref args "path" #f)))
     (if (not path) (error 'read "missing path arg")
       (let ((p (abs-path cwd path)))
-        (if (file-exists? p) (read-file-string p)
-          (string-append "(file does not exist: " path ")"))))))
+        (cond
+          ((pending-ss-create-repair-message cwd) => (lambda (msg) msg))
+          ((not (file-exists? p))
+           (string-append "(file does not exist: " path ")"))
+          ((file-directory? p)
+           (string-append "(path is a directory: " path "; use list)"))
+          (else (slice-content (read-file-string p) args)))))))
+
+(def (do-list args cwd)
+  (note-inspection-after-failed-verify! 'list)
+  (let* ((path (or (arg-ref args "path" #f) "."))
+         (p (abs-path cwd path)))
+    (cond
+      ((pending-ss-create-repair-message cwd) => (lambda (msg) msg))
+      ((not (file-exists? p))
+       (string-append "(path does not exist: " path ")"))
+      ((not (file-directory? p))
+       (string-append "(not a directory: " path ")"))
+      (else
+       (let* ((entries (list-sort string<? (directory-list p)))
+              (shown (take entries (min 200 (length entries))))
+              (suffix (if (> (length entries) 200)
+                        (format "\n... ~a more" (- (length entries) 200))
+                        "")))
+         (if (null? shown)
+           (string-append "(empty directory: " path ")")
+           (string-append (string-join shown "\n") suffix)))))))
+
+(def (shell-unavailable _args)
+  "Arbitrary shell commands are unavailable in this verified workflow. Use list/read for inspection, grep for file search, edit for scoped writes, verify to run the configured verifier, and done only after verify passes.")
+
+(def (split-command s)
+  (let ((n (string-length s)))
+    (let loop ((i 0) (cur '()) (words '()) (quote-ch #f) (esc? #f) (in-word? #f))
+      (cond
+        ((= i n)
+         (reverse
+           (if in-word?
+             (cons (list->string (reverse cur)) words)
+             words)))
+        (else
+         (let ((ch (string-ref s i)))
+           (cond
+             (esc?
+              (loop (+ i 1) (cons ch cur) words quote-ch #f #t))
+             ((char=? ch #\\)
+              (loop (+ i 1) cur words quote-ch #t #t))
+             (quote-ch
+              (if (char=? ch quote-ch)
+                (loop (+ i 1) cur words #f #f #t)
+                (loop (+ i 1) (cons ch cur) words quote-ch #f #t)))
+             ((or (char=? ch #\") (char=? ch #\'))
+              (loop (+ i 1) cur words ch #f #t))
+             ((char-whitespace? ch)
+              (if in-word?
+                (loop (+ i 1) '() (cons (list->string (reverse cur)) words) #f #f #f)
+                (loop (+ i 1) cur words #f #f #f)))
+             (else
+              (loop (+ i 1) (cons ch cur) words #f #f #t)))))))))
+
+(def (first-path-arg words)
+  (let loop ((ws words))
+    (cond
+      ((null? ws) #f)
+      ((string=? (car ws) "|") #f)
+      ((string-prefix? "-" (car ws)) (loop (cdr ws)))
+      (else (car ws)))))
+
+(def (numeric-flag-value flag default)
+  (if (and (> (string-length flag) 1)
+           (char=? (string-ref flag 0) #\-))
+    (or (string->number (substring flag 1 (string-length flag))) default)
+    default))
+
+(def (read-lines-at path cwd mode n)
+  (let ((content (do-read (list (cons "path" path)) cwd)))
+    (if (read-error-text? content)
+      content
+      (let* ((lines (string-split content #\newline))
+             (chosen (if (equal? mode 'tail)
+                       (last-up-to lines n)
+                       (take-up-to lines n))))
+        (string-join chosen "\n")))))
+
+(def (tail-head-args words default-n)
+  (cond
+    ((and (pair? words) (string=? (car words) "-n") (pair? (cdr words)))
+     (values (or (string->number (cadr words)) default-n)
+             (and (pair? (cddr words)) (car (cddr words)))))
+    ((and (pair? words) (string-prefix? "-" (car words)))
+     (values (numeric-flag-value (car words) default-n)
+             (and (pair? (cdr words)) (cadr words))))
+    (else
+     (values default-n (first-path-arg words)))))
+
+(def (starts-at-zero? s prefix)
+  (let ((idx (string-contains s prefix)))
+    (and idx (= idx 0))))
+
+(def (read-error-text? s)
+  (or (starts-at-zero? s "(file does not exist:")
+      (starts-at-zero? s "(path is a directory:")
+      (starts-at-zero? s "(not a directory:")
+      (starts-at-zero? s "A previous edit for ")))
+
+(def (line-count-for path cwd)
+  (let ((content (do-read (list (cons "path" path)) cwd)))
+    (if (read-error-text? content)
+      content
+      (number->string (length (string-split content #\newline))))))
+
+(def (open-delim? ch)
+  (or (char=? ch #\()
+      (char=? ch #\[)
+      (char=? ch #\{)))
+
+(def (close-delim? ch)
+  (or (char=? ch #\))
+      (char=? ch #\])
+      (char=? ch #\})))
+
+(def (matching-delim? open close)
+  (or (and (char=? open #\() (char=? close #\)))
+      (and (char=? open #\[) (char=? close #\]))
+      (and (char=? open #\{) (char=? close #\}))))
+
+(def (balance-report content path)
+  (let ((n (string-length content)))
+    (let loop ((i 0)
+               (line 1)
+               (col 1)
+               (stack '())
+               (in-string? #f)
+               (escape? #f)
+               (in-comment? #f))
+      (cond
+        ((= i n)
+         (if (null? stack)
+           (string-append "Balance OK: " path)
+           (let ((top (car stack)))
+             (format "Unclosed ~a opened at line ~a, column ~a in ~a"
+                     (car top) (cadr top) (caddr top) path))))
+        (else
+         (let* ((ch (string-ref content i))
+                (newline? (char=? ch #\newline))
+                (next-line (if newline? (+ line 1) line))
+                (next-col (if newline? 1 (+ col 1))))
+           (cond
+             (in-comment?
+              (loop (+ i 1) next-line next-col stack #f #f
+                    (and (not newline?) in-comment?)))
+             (in-string?
+              (cond
+                (escape?
+                 (loop (+ i 1) next-line next-col stack #t #f #f))
+                ((char=? ch #\\)
+                 (loop (+ i 1) next-line next-col stack #t #t #f))
+                ((char=? ch #\")
+                 (loop (+ i 1) next-line next-col stack #f #f #f))
+                (else
+                 (loop (+ i 1) next-line next-col stack #t #f #f))))
+             ((char=? ch #\;)
+              (loop (+ i 1) next-line next-col stack #f #f #t))
+             ((char=? ch #\")
+              (loop (+ i 1) next-line next-col stack #t #f #f))
+             ((open-delim? ch)
+              (loop (+ i 1) next-line next-col
+                    (cons (list ch line col) stack) #f #f #f))
+             ((close-delim? ch)
+              (cond
+                ((null? stack)
+                 (format "Unexpected close ~a at line ~a, column ~a in ~a"
+                         ch line col path))
+                ((matching-delim? (caar stack) ch)
+                 (loop (+ i 1) next-line next-col (cdr stack) #f #f #f))
+                (else
+                 (let ((top (car stack)))
+                   (format "Mismatched close ~a at line ~a, column ~a in ~a; top opener is ~a from line ~a, column ~a"
+                           ch line col path
+                           (car top) (cadr top) (caddr top))))))
+             (else
+              (loop (+ i 1) next-line next-col stack #f #f #f)))))))))
+
+(def (balance-file args cwd)
+  (note-inspection-after-failed-verify! 'balance)
+  (let ((path (arg-ref args "path" #f)))
+    (cond
+      ((not path) "balance: missing path")
+      ((pending-ss-create-repair-message cwd) => (lambda (msg) msg))
+      (else
+       (let ((content (do-read (list (cons "path" path)) cwd)))
+         (if (read-error-text? content)
+           content
+           (balance-report content path)))))))
+
+(def (grep-args words)
+  (let loop ((ws words))
+    (cond
+      ((null? ws) (values #f #f))
+      ((string-prefix? "-" (car ws)) (loop (cdr ws)))
+      (else
+       (values (strip-shell-quotes (car ws)) (first-path-arg (cdr ws)))))))
+
+(def (grep-lines pattern path cwd)
+  (let ((content (do-read (list (cons "path" path)) cwd)))
+    (if (read-error-text? content)
+      content
+      (let loop ((lines (string-split content #\newline))
+                 (line-no 1)
+                 (acc '()))
+        (cond
+          ((null? lines)
+           (if (null? acc)
+             "(no matches)"
+             (string-join (reverse acc) "\n")))
+          ((string-contains (car lines) pattern)
+           (loop (cdr lines) (+ line-no 1)
+                 (cons (format "~a:~a" line-no (car lines)) acc)))
+          (else
+           (loop (cdr lines) (+ line-no 1) acc)))))))
+
+(def (strip-shell-quotes s)
+  (let ((n (string-length s)))
+    (if (and (>= n 2)
+             (or (and (char=? (string-ref s 0) #\')
+                      (char=? (string-ref s (- n 1)) #\'))
+                 (and (char=? (string-ref s 0) #\")
+                      (char=? (string-ref s (- n 1)) #\"))))
+      (substring s 1 (- n 1))
+      s)))
+
+(def (sed-range-bounds token)
+  (let* ((clean (strip-shell-quotes token))
+         (n (string-length clean)))
+    (if (and (> n 1) (string-suffix? "p" clean))
+      (let* ((body (substring clean 0 (- n 1)))
+             (parts (string-split body #\,)))
+        (cond
+          ((= (length parts) 1)
+           (let ((line (string->number (car parts))))
+             (if line
+               (values line line)
+               (values #f #f))))
+          ((= (length parts) 2)
+           (let ((start (string->number (car parts)))
+                 (end (string->number (cadr parts))))
+             (if (and start end (<= start end))
+               (values start end)
+               (values #f #f))))
+          (else (values #f #f))))
+      (values #f #f))))