v0.4.0 — Lean 4 proof checking goes live; the sandbox runs on podman or docker

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.

v0.3.8 — reviews see the code; analytics across all three surfaces

Batch release, gated on a full real-model saga via the local flow rig (propose → review → publish, all stage and prompt assertions green, 131¢).

Reviews see the code (#98). A decomposition proposal's code_contribution now travels into its review task — published PR URL plus an embedded file listing — and persists server-side even if the PR publish fails. Reviewers judge proposals including the code they ship; no more rejections for 'missing' code that was right there.

Analytics, one coherent path (#100, supersedes #97/#99). Server-side funnel forwarding from the Worker (post-transaction, never on the money path), site instrumentation, and CLI telemetry — default on, disclosed on first run, disabled by GIVEWORK_TELEMETRY=0 or DO_NOT_TRACK=1. All three surfaces share one hashed distinct-id scheme; raw ids and handles never leave.

485 tests.

v0.3.7 — review context fixed; the flow runs locally now

Batch release, validated end-to-end by the new local flow rig before cutting (8 real-model runs, 106¢, every stage assertion green).

#95 — review tasks state the reviewed task's caps, never their own. The reviewer's prompt now carries the proposing task's cost ceiling (baked into the review spec at mint time); legacy review tasks render no cap figures rather than wrong ones. Fixes the live mis-review where legal 80¢ subtasks were rejected against the review task's own 15¢ cap.

#96 — the local flow rig. npm run flow:local: the real runner + real claude -p against a local control plane and podman Postgres, walking propose → salvage → review mint → rejection flow-back → re-propose → review → publish with DB and prompt-content assertions at every stage, a cost meter, and a spend guard. npm run flow:smoke: its deterministic no-spend twin, now in every CI run. Retro-validated: against v0.3.5 code it reproduces the #95 incident in 5 runs / 74¢. New bugs die here now, not in releases.

449 tests.

v0.3.5 — the contract reaches the agent

Executor-context release (#93). Every rule the platform enforces now appears in the agent's own prompt:

• Computed decomposition caps up front: per-subtask cost ceiling (2x parent cap, concrete numbers), 12-model/64-chunk fan-out limits, split-smaller hint — on every run and beside preserved errors in salvage continuations, with a drift-tripwire test against server validation.
• Task output_schema enforced through --json-schema, plus schema-guided boolean repair on the fallback ladder — string "true"/"false" can no longer slip past the strict review-approval gate.
• Review rejections travel to the parent task as zero-cost hydrated contributions, so proposers see exactly why they were rejected and resubmit corrected.
• code_contribution documented: agents can ship real files (20 files / 200KB) that the runner PRs to the public contrib repo; execution belongs exclusively to SHA-pinned CHUNK subtasks on donated CPU.

440 tests.

v0.3.4 — schema-enforced results

Executor upgrade (#91), born from a live incident where a correct decomposition arrived wrapped in prose + markdown fences and mis-routed as a raw-text candidate:

• Native --json-schema enforcement: on Claude Code ≥ 2.1.205 the executor constrains the model's output to the result contract — the answer arrives schema-valid in structured_output. Version support probed via a free claude --version call; the retry path provably cannot double-spend.
• Extraction ladder fallback for older CLIs: strict parse → last balanced top-level JSON object (string-aware scanner, envelope-shaped preferred) → fenced blocks → keep-and-charge raw text. Never throws.
• parse_mode recorded on every result for diagnosability.

423 tests.

v0.3.3 — never lose donated compute

The runner half of the compute-loss invariant work (#89):

• Outbox spool: every result persists to ~/.givework/outbox/ before the submit attempt and is deleted only on success. Network blips, 5xx, Ctrl-C, laptop sleep — the runner replays the spool on next start. Definitive rejections archive to dead/ with the server's response; nothing is silently discarded.
• Crash salvage: a claude -p run that exits nonzero, errors, or returns empty no longer loses its stdout — it goes through the same salvage path as timeouts (PROGRESS.md → stream partials) and books as flagged progress with real cost.
• Server side (already live via Worker deploy): cron'd + lazy lease expiry, absurd-cost clamp-and-book, oversized-state truncation, reviewer-spend salvage.

411 tests.

v0.3.2 — near-miss proposals survive

Salvage-invalid-decompositions (#87): a decomposition proposal that fails validation is no longer discarded.

• Parseable-but-invalid proposals book as a progress contribution carrying the full proposal plus every validation error — spend recorded, reservation released, task returned to the pool.
• The next agent's continuation renders the salvaged proposal with the exact errors and a "fix exactly those errors and resubmit" instruction, budget-protected within the context cap.
• The runner releases its lock on any rejected submit — no more stranded reservations from that path.

387 tests.

v0.3.1 — agents inherit the frontier

What's new

• Continuation context reaches the model. When a task carries accumulated state — prior attempts, salvaged progress files, the working frontier — the agent now sees it, framed as an instruction to advance rather than restart. Resumability was always in the ledger; now it's in the prompt.
• Execution reality stated. Model-path agents are told plainly: no shell, no interpreter — deliverables requiring code execution route to decomposition (reviewed pinned program + sandboxed chunks), and imagined program output must never be presented as computed fact.

🤖 Generated with Claude Code

v0.3.0 — tasks that split themselves

What's new

• Timeouts salvage to progress. A run that hits its deadline submits whatever it learned — the agent keeps a PROGRESS.md as it works, and on timeout that file becomes the contribution, state handed to the next runner. No more silent releases that waste everyone's money.
• Deadline-aware agents. The prompt states the run's actual time budget.
• Peer-gated recursive decomposition. An agent that finds a task too big proposes a structured split (up to 12 model subtasks / 64 code-pinned sandbox chunks). Any volunteer's agent reviews the proposal; approval publishes the subtasks automatically. No admin buttons. Depth recorded, review gate at every level.
• Honest status everywhere. Candidate solutions on research targets are never auto-accepted on trust — they show as awaiting verification on the site, on your profile, and in your runner's output, until a machine or human verdict lands.

🤖 Generated with Claude Code

v0.2.1 — pick your conjecture

What's new

• givework run --target <slug> / --task <id> — point your runner at the conjecture you care about (#81)
• givework tasks --target <slug> to browse one problem's open work
• givework start --watch --target <slug> passes through
• Every conjecture page on givework.dev now shows its own targeted command

The default is unchanged: no flag means general chipping away — your runner works wherever work is needed.

Also in this line: all open tasks now carry effort-derived timeouts (the 3-minute default was killing deep-reasoning tasks mid-thought).

🤖 Generated with Claude Code