moshcode work: 50 AI Agents, One Verifier, One Inbox

When people run thousands of AI agents to prove mathematical theorems, they aren't staring at thousands of agents. The proof checker is the one staring. Lean gives a yes or no to every attempt, wrong attempts are discarded, and humans only look at two things: what passed, and where things got stuck.

Our previous agent tools took a different path. A "herd" was one terminal pane per agent, a "swarm" was a few panes. The ceiling depended on how many panes a person could read, roughly ten.

So moshcode 0.117.0 adds moshcode work. Each task carries a verify command, and exit code 0 is the only definition of "done." Workers are headless processes, each in its own git worktree. The engine's self-assessment of its own work is recorded but never accepted.

moshcode work from-tests fix-tests                 # one task per failing test file
moshcode work run fix-tests -n 50 --engine claude  # fifty workers
moshcode work status fix-tests                     # numbers, not transcripts
moshcode work inbox fix-tests                      # only tasks that failed every attempt
moshcode work apply fix-tests                      # merge passing patches

A failed attempt goes back into the queue with its verification output, feeding into the next prompt. After three failures, the task goes into the inbox along with its worktree. A task that has already passed only needs one verification and consumes no tokens. Task claiming is an atomic file rename, so multiple runs on the same queue can split tasks. Each run is recorded as an OpenFleet swarm.

First Run: Practice on moshcode Itself

We had 139 tests failing locally but passing in CI. from-tests ran each file separately and found only one real failure. The other 138 were PWA tests that crashed when the PWA's own dependencies weren't installed, instead of skipping like their neighbors.

That was 19 tasks. Verification for each PWA file ran twice: without dependencies (must skip) and with dependencies (must pass). 50 Claude workers processed them in parallel.

All 19 tasks passed on the first attempt. The inbox stayed empty. No assertions were added or removed. Local failures dropped from 139 to 0.

The one real failure was the best find. A moshcode mcp install test inherited the host's PATH and HOME, so any coding engine installed on the machine would join the run and execute a real mcp add against my own config. The worker made it use only a stub engine.

The next queue needs a different verifier from tests: type-check errors, URLs that must return 200, eventually Lean.

moshcode upgrade self gets it. Source and PRD: https://github.com/moshcoder/moshcode/releases/tag/v0.117.0

What makes PWA (Progressive Web App) tests special is their dependency environment: when the PWA's own dependencies aren't installed, tests usually skip rather than fail, but in some cases they crash outright. The 138 PWA test failures mentioned in the article were precisely because missing dependencies caused crashes, and the verification condition required "must skip when there are no dependencies, must pass when there are dependencies," ensuring consistent behavior across environments. This dual verification strategy avoids false positives caused by environment differences and is one of the key designs of verifier-driven workflows.

Core Design: Verifier-Driven, Not Human-Supervised

The design philosophy of moshcode work draws directly from practice in the field of mathematical proofs. There, humans don't need to review every agent's reasoning process because the Lean proof checker provides an objective, non-negotiable pass/fail signal. moshcode ports this pattern to software development tasks: the verify command is your Lean.

This means the agent's self-assessment is deliberately marginalized. The engine might say "I'm done," but only exit code 0 counts. This design eliminates the risk of agent overconfidence or hallucinated completion. Verification output from failed attempts feeds into the next attempt's prompt, forming an iterative improvement loop based on objective signals.

Lean is an interactive theorem prover and also a programming language. Its core feature is the ability to machine-check mathematical proofs: users write proofs, Lean verifies their correctness line by line, and ultimately returns "pass" or points to the error location. This check is objective and non-negotiable, independent of the prover's self-assessment. In the field of mathematical formalization, Lean has been used to verify complex theorems (such as fragments of Fermat's Last Theorem), and its strict checking mechanism ensures the reliability of proofs. moshcode work ports this paradigm to software development, using the verify command (such as test runs, type checks) to simulate Lean's checker role, thereby downgrading the agent's self-assessment to reference information.

Parallelization and Task Splitting

By isolating each worker with a git worktree, moshcode work avoids file conflicts between agents. Task claiming is implemented through atomic file renames, allowing multiple runs to safely share the same queue. This provides the foundation for horizontal scaling: you can run 50, 100, or even more workers, and the bottleneck is no longer human reading capacity but the execution speed of the verification command.

The inbox mechanism is another key design. Only tasks that have exhausted all attempts (three by default) and still fail enter the inbox, retaining their worktree for human inspection. This ensures human attention is focused on genuinely difficult problems rather than being overwhelmed by a flood of successful cases.

Git worktree allows multiple branches to be checked out simultaneously into different directories within the same repository. Each worktree has its own working area and index but shares the same .git directory. This enables multiple processes to modify code in parallel without interfering with each other, while keeping commit history unified. In moshcode work, each worker runs in its own git worktree, and after a task completes, patches are merged via the apply command. This isolation avoids file conflicts while preserving the full version control context for inspecting worktree state on failure.

Real-World Results and Insights

On moshcode's own test suite, 50 Claude workers processed 19 tasks in parallel, all passing on the first attempt, reducing local failures from 139 to 0. More importantly, it found a hidden test defect: a test inadvertently inherited the host's environment variables, causing a real mcp add operation to be executed. Such problems are easily overlooked in traditional manual review.

This case demonstrates two core advantages of verifier-driven agent workflows: scaling and discovering deep problems. When verification is objective, you can parallelize with confidence; when humans only inspect failure cases, you can find defects that success has masked.

The next challenge is extending the verifier from tests to type checks, HTTP status code checks, and ultimately formal proofs. Each step requires a different verification strategy, but the core pattern remains the same: an objective verifier, a large number of headless workers, and an inbox that only shows tasks that are truly stuck.

One-line Summary

moshcode work uses the verify command's exit code 0 as the completion standard, enabling 50 parallel agents while humans only see failures.

Paragraph Summary

moshcode 0.117.0 introduces moshcode work, borrowing the Lean checker pattern from mathematical proofs to use the verify command's exit code 0 as the sole criterion for task completion, ignoring the AI engine's self-assessment. Each worker is a headless process running in an independent git worktree, with task claiming via atomic file renames supporting multiple runs sharing a queue. Failed attempts feed verification output into the next prompt; after three failures, tasks enter the inbox with their worktree preserved for human inspection. In moshcode's own tests, 50 Claude workers processed 19 tasks in parallel, all passing on the first attempt, reducing local failures from 139 to 0 and uncovering a hidden test defect. The pattern can extend to type checks, URL validation, and Lean proofs.