Add proof worker pool routing

4-Infrastructure/infra/deploy_language_proof_server.sh

@@ -116,7 +116,7 @@ fi
 export HOME=/var/lib/language-proof-server
 export PATH="$HOME/.elan/bin:$PATH"
 cd /srv/research-stack/0-Core-Formalism/lean/Semantics
-runuser -u proofsrv -- sh -lc "cd /srv/research-stack/0-Core-Formalism/lean/Semantics && export PATH=/var/lib/language-proof-server/.elan/bin:\$PATH && elan toolchain install \"\$(cat lean-toolchain)\" && lake update"
+runuser -u proofsrv -- sh -lc "cd /srv/research-stack/0-Core-Formalism/lean/Semantics && export PATH=/var/lib/language-proof-server/.elan/bin:\$PATH && elan toolchain install \"\$(cat lean-toolchain)\" || true; lake update"
 systemctl daemon-reload
 systemctl enable --now language-proof-server.service
 systemctl --no-pager --full status language-proof-server.service | sed -n "1,18p"

4-Infrastructure/infra/language_proof_server.py

@@ -105,6 +105,11 @@ def command_env() -> dict[str, str]:
     return env
 
 
+def command_prefix() -> list[str]:
+    raw = os.environ.get("PROOF_COMMAND_PREFIX", "").strip()
+    return shlex.split(raw) if raw else []
+
+
 def run_command(
     command: list[str],
     cwd: Path,
@@ -112,10 +117,11 @@ def run_command(
     timeout_s: int,
 ) -> dict[str, Any]:
     started = time.time()
-    command_display = " ".join(shlex.quote(part) for part in command)
+    full_command = command_prefix() + command
+    command_display = " ".join(shlex.quote(part) for part in full_command)
     try:
         proc = subprocess.run(
-            command,
+            full_command,
             cwd=str(cwd),
             env=command_env(),
             text=True,
@@ -178,6 +184,7 @@ def health() -> dict[str, Any]:
     checks: dict[str, Any] = {
         "repo_dir": str(repo_dir()),
         "lean_root": str(root),
+        "proof_command_prefix": command_prefix(),
         "lean_root_exists": root.exists(),
         "lakefile_exists": (root / "lakefile.toml").exists(),
         "lean_toolchain_exists": (root / "lean-toolchain").exists(),

4-Infrastructure/infra/remote_lean_proof_mcp.py

@@ -3,6 +3,7 @@
 
 from __future__ import annotations
 
+import hashlib
 import json
 import os
 import sys
@@ -38,7 +39,29 @@ def base_url() -> str:
     return os.environ.get("PROOF_SERVER_URL", DEFAULT_URL).rstrip("/")
 
 
-def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int = 120) -> dict[str, Any]:
+def proof_urls() -> list[str]:
+    raw = os.environ.get("PROOF_SERVER_URLS", "").strip()
+    urls = [item.strip().rstrip("/") for item in raw.split(",") if item.strip()]
+    if not urls:
+        urls = [base_url()]
+    return list(dict.fromkeys(urls))
+
+
+def ordered_urls(payload: dict[str, Any] | None = None) -> list[str]:
+    urls = proof_urls()
+    if len(urls) <= 1 or payload is None:
+        return urls
+    key = str(payload.get("name") or payload.get("target") or payload.get("agent") or "")
+    offset = int(hashlib.sha256(key.encode("utf-8")).hexdigest(), 16) % len(urls)
+    return urls[offset:] + urls[:offset]
+
+
+def request_json_from(
+    url: str,
+    path: str,
+    payload: dict[str, Any] | None = None,
+    timeout: int = 120,
+) -> dict[str, Any]:
     headers = {"Accept": "application/json", "User-Agent": f"{SERVER_NAME}/{SERVER_VERSION}"}
     body = None
     method = "GET"
@@ -49,10 +72,13 @@ def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int
         auth = token()
         if auth:
             headers["Authorization"] = f"Bearer {auth}"
-    req = urllib.request.Request(f"{base_url()}{path}", data=body, headers=headers, method=method)
+    req = urllib.request.Request(f"{url}{path}", data=body, headers=headers, method=method)
     try:
         with urllib.request.urlopen(req, timeout=timeout) as response:
-            return json.loads(response.read().decode("utf-8"))
+            data = json.loads(response.read().decode("utf-8"))
+            if isinstance(data, dict):
+                data.setdefault("proof_server_url", url)
+            return data
     except urllib.error.HTTPError as exc:
         text = exc.read().decode("utf-8", errors="replace")
         try:
@@ -61,20 +87,34 @@ def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int
             data = {"error": text}
         data["http_status"] = exc.code
         data["ok"] = False
+        data["proof_server_url"] = url
         return data
     except Exception as exc:
-        return {"ok": False, "error": f"{type(exc).__name__}: {exc}"}
+        return {"ok": False, "error": f"{type(exc).__name__}: {exc}", "proof_server_url": url}
+
+
+def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int = 120) -> dict[str, Any]:
+    failures = []
+    for url in ordered_urls(payload):
+        data = request_json_from(url, path, payload, timeout)
+        if data.get("ok"):
+            return data
+        failures.append(data)
+    return {"ok": False, "error": "all proof servers failed", "failures": failures}
 
 
 def tool_status(_: dict[str, Any]) -> dict[str, Any]:
-    health = request_json("/health", timeout=10)
+    nodes = [request_json_from(url, "/health", timeout=10) for url in proof_urls()]
+    healthy = [node for node in nodes if node.get("ok")]
     return {
-        "ok": bool(health.get("ok")),
+        "ok": bool(healthy),
         "server": SERVER_NAME,
         "version": SERVER_VERSION,
         "proof_server_url": base_url(),
+        "proof_server_urls": proof_urls(),
         "token_configured": bool(token()),
-        "health": health,
+        "health": healthy[0] if healthy else (nodes[0] if nodes else {"ok": False}),
+        "nodes": nodes,
     }
 
 

AGENTS.md

@@ -229,6 +229,15 @@ slow or unavailable. The MCP server fronts the dedicated proof service at
 `~/.config/ene/language-proof-server.token`, and returns receipt-bearing
 responses.
 
+Active proof-worker pool:
+
+```text
+http://54.236.176.28:8787     AWS EC2 dedicated proof server
+http://100.110.163.82:8787    361395-1 Netcup proof worker
+http://100.102.173.61:8787    nixos-laptop proof worker
+http://100.85.244.73:8787     nixos-steamdeck-1 proof worker
+```
+
 Primary tools:
 
 - `proof_status` for health and token wiring.

opencode.json

@@ -31,6 +31,7 @@
       ],
       "environment": {
         "PROOF_SERVER_URL": "http://54.236.176.28:8787",
+        "PROOF_SERVER_URLS": "http://54.236.176.28:8787,http://100.110.163.82:8787,http://100.102.173.61:8787,http://100.85.244.73:8787",
         "PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
       },
       "enabled": true