Inspiration
Coding agents can produce large changes quickly, but integration is where confidence breaks down. A repository may already contain unrelated local work, platform-specific dependencies, tests that hang, stale baselines, and generated artifacts that make a green run difficult to reproduce. ProofRun was built to make those risks explicit and executable. Football Universe predates Build Week and is the demanding real-world validation target. The submitted product is the developer-tool workflow around it.
What it does
ProofRun turns each Codex-assisted change into a declared transaction. A package fixes the baseline commit, exact file allowlist, before-and-after SHA-256 hashes, validation profiles, review requirements, and proposed commit message. Packages cannot supply shell commands or escape their file scope. ProofRun accepts trusted local packages; its detached worktree is a Git-isolation boundary, not an operating-system sandbox.
Before mutation, the runner validates Git identity and integrity, repository governance, schema, hashes, dependencies, Python, process-tree control, UTF-8 subprocess behavior, temporary-worktree capacity, and the Windows path budget. One nonblocking OS lock serializes mutating commands per project root. After PASS_COMMIT_DEFERRED, an atomic report- and byte-bound reservation prevents another package from taking over Main before the human decision is resolved.
Every long-running profile emits a start marker, heartbeats, a bounded timeout, and a typed PASS, FAIL, TIMEOUT, or ABORTED result. Independent safe checks can continue after ordinary failures, while trust failures stop mutation immediately. Every non-pass path produces one readable, hash-verified evidence archive. Only a completely green sandbox can reach the main worktree. ProofRun promotes byte-identical payloads, rechecks the complete Git status before Main apply, proves unrelated files were preserved, and rolls back if main validation fails. Even a successful run never commits automatically: the human keeps final authority.
How we built it
The runner is a Python standard-library orchestrator backed by a versioned JSON contract, strict package schema, Git detached worktrees, deterministic profile ordering, owned process-tree termination, atomic reports, and SHA-256 evidence verification. GPT-5.6 Sol in Codex was used to inspect the large repository, implement bounded changes, write regression tests, analyze failures from real package runs, coordinate commit boundaries, and prepare the judge-facing evidence.
Challenges
The hardest problems were Windows path limits, safe cleanup of owned process trees, stale duplicated test fixtures, preserving unrelated work, distinguishing ordinary failures from trust failures, closing the gap between validation and deferred commit, and making every terminal path produce stable evidence.
Accomplishments
The filmed v1.7.3 release passes 74 of 74 runner tests, and its disposable demo package passes all eight declared profiles. That demo intentionally ends at PASS_COMMIT_DEFERRED. The later v1.8.0 security package passed all eight profiles, plus 96 of 96 runner tests, 30 of 30 Codex integration tests, and 12 of 12 public self-tests; its reviewed bytes were committed as 95d9322.
The current v1.9.0 source passes 115 of 115 canonical runner tests and 12 of 12 public self-tests. Its exclusive-lock and pending-reservation package passed all seven declared profiles and was committed as dfff776 after technical review. Finally, this judge-guide package itself passed all eight profiles and was committed as 889046a.
What we learned
A coding agent should not be its own judge. Repository governance, isolation, evidence, rollback, concurrency ownership, and commit authority become more trustworthy when they are independent executable constraints.
What's next
We plan to add more package templates, portable CI adapters, richer evidence viewers, and additional platform profiles while preserving the same human-controlled commit boundary.
Log in or sign up for Devpost to join the conversation.