Batch release covering six PRs (the first tag since v0.3.8 — v0.3.9 shipped untagged). Gated on a full real-model saga via the local flow rig (propose → scripted rejection → re-propose → review → publish, all stage and prompt assertions green, 118¢), plus the lean4 canary against the real pinned image under real podman.
Lean 4 proof checking goes live (#104). verify_via: proof_checker stops being a promise. A formalization chunk pins a merged .lean file, the work-unit sandbox runs lean <entrypoint> (Lean 4.10.0, core prelude — no mathlib in v1), and the compiler's exit code becomes the recorded verdict: green auto-accepts the chunk, red returns it to the pool with the full diagnostics preserved as a compiler_output artifact that the next agent's prompt hydrates. The sorry hole is closed at the interpreter — lean exits 0 on a sorried declaration, so the warning is treated as a failed check. A timed-out check is salvaged as a progress contribution, never silently released. Resolving a conjecture stays an admin act; the target does not flip.
Any container engine, and the sandbox line tells the truth (#106). The work-unit sandbox runs on podman or docker, auto-detected (podman first), forced with GIVEWORK_CONTAINER_ENGINE. The detection probes the daemon rather than the binary — podman --version exits 0 with the machine stopped, which would have promised a sandbox that then failed every task and, after three failures, aborted the whole run loop including model work. A stopped engine now reads as not-found and falls through to one that answers. The failure-path container reap follows the resolved engine too, so docker-only hosts stop leaking containers.
Durable video pipeline (#105) and the films gallery (#103). Canonical tools in video/ plus a conjecture-video skill; the site gains a data-driven gallery of conjecture explainers.
Autopilot hygiene (#101). Synthesized work-unit summaries, refusal to point a stub executor at a remote control plane, strict CLI flag parsing.
Analytics on the managed reverse proxy (#102). Browser analytics ride v.givework.dev.
564 tests.