v0.12.0 — Tauri desktop app default, security hardening, formal verification
Summary
Changes since v0.11.0 (6 commits / PRs #526–#528).
The Tauri desktop app becomes the only start path: start now builds and launches the native Seiso Forge desktop wrapper instead of opening a browser (web UI seiso forge and TUI seiso tui remain CLI commands). The desktop wrapper was fixed end-to-end so it actually runs and renders, the wrapper and startup path were security-hardened from a dedicated review, and the security-critical logic is now formally verified in Lean 4 + mathlib4.
What's new
Tauri desktop app as the default startup path (#526)
start/./scripts/start.shlaunch the Seiso Forge desktop app (Tauri) — the only startup path- Fixed the wrapper so it actually works: startup panic (
plugins.shell.sidecar→open), white screen (missingcustom-protocolfeature — release now embeds the UI), "load failed" after auth (webview now navigates to the backend origin soSameSite=Strictsession cookies are same-origin; polls/healthfirst) - CORS allowlist for the Tauri webview origins; absolute API base under Tauri; forgotten-key reset uses an in-app dialog instead of
window.confirm(a no-op in WKWebView); sidecar env forwarding
Security hardening (#527)
- Removed unscoped
shell:allow-spawn/execute/openpermissions (arbitrary RCE primitive the webview never used) - Worktree path traversal closed (canonicalize + require containment under the data dir, re-validated before every write)
- Enforced agent runtime cap (was dead code — heartbeat could bypass stall detection),
MAX_CONCURRENT_AGENTS, and string length caps - Validated persisted
swarm_runs.jsonrestore; atomic persist (temp + rename); hardened sidecar (execs the venvseisodirectly, no env-controlledactivatesourcing);get_backend_statusreports real sidecar state; CSP hardened; bundle targets restricted to unix - Resolved all GitHub Dependabot alerts (ghost alerts from a stale
uv.lockdismissed; glib has no upstream fix — version-locked tray stack)
Formal verification (#528)
- New
formal/Lean 4 + mathlib4 project: 30 machine-checked theorems proving the invariants of the swarm orchestrator (stall detection, agent cap, path containment, truncation, atomic persist), frontend/backend control flow (redirect target, API base, CORS, CSRF), and the startup path (build-then-launch, port agreement) - Verification confirms the security fixes are correct; found no additional bugs
Notes
- Custom
SEISO_PORTis honored by the sidecar but not by the webview redirect/CSP (both hardcode 8765) — custom ports are out of scope for the current design - Desktop wrapper is new; first
startcompiles the Rust host (can take several minutes)