ProofForge

• 

  ProofForge receipts

• 

  Terminal results

• 

  When it was gamed

• 

  When it was verified

Inspiration

Coding agents are judged by their own word. An agent that runs the visible tests, sees them pass and writes "fixed" is trusted, even when it bent the code to fit the tests or never checked half the requirements.

We wanted an agent whose "done" means something: done only when checks it cannot see, edit or game agree. And when a task cannot be done, it should say so instead of faking it.

What it does

ProofForge is a coding agent that never says "done" without proof. Every task runs the same loop, and the agent can only pass by fixing the real behaviour:

1. Prove the problem. The checks run on the untouched code first; if they already pass, there is nothing to prove.
2. Fix in a sandbox. A Nemotron agent explores, runs and edits code in an isolated Nebius sandbox with its own tools (read, search, run, edit, submit).
3. Freeze the oracle. Test files are frozen and hashed. Edits to them are refused, and changes made through the shell are caught as tampering.
4. Judge with hidden checks. Checks the agent never saw decide the verdict. On a retry it learns only that they failed, not why.
5. Write a receipt. Every step, every check result, the diff and the cost go into a receipt, published on a public site.

On top of that loop:

• Honest exit. A report_impossible tool lets the agent name a contradiction instead of gaming it.
• Tournament with a Breaker. Three approaches race from one checkpoint while a Breaker agent writes extra tests from the spec. The winner is picked before any hidden check runs, then faces them alone.
• Network sealing. Tasks that forbid internet run every command in a private network namespace, so the agent cannot download the answer.

How we built it

• Models: NVIDIA Nemotron Lightning, Super and Ultra on Nebius Token Factory, each mapped to a role (coder, fixer, Breaker) and a cost mode. One API key and one OpenAI-compatible endpoint reach every model, and per-call token usage gives an exact cost for every attempt.
• Sandboxes: Nebius sandboxes run every command. Their immutable checkpoints let several attempts branch from the same state, and hidden checks always run on a disposable copy.
• Engine: a Python agent loop with its own tools, context compaction, a coach against loops, and hard per-task budget caps.
• Benchmarks: SWE-bench Pro HARD-51, Long-Horizon Terminal-Bench (including robotics and scientific simulation tasks), plus our own RealWorld, PipelineBench and impossible-task suites, all through one Harbor-format adapter.
• Receipts: a JSON receipt per run, rendered into a static site on GitHub Pages.

The whole project, including every benchmark run, used about $32 of paid Token Factory credit.

Challenges we ran into

• The sandboxes were online. On a "reimplement these libraries" task, the benchmark's own grader zeroed our reference solution because it could reach PyPI. We now cut the network for such tasks ourselves, and the same solution scored 1.00.
• Our own grading could be wrong too. We caught and corrected four of our own errors, in the open:
  • Results showed the best round's score instead of the change the run ended with (0.77 reported where 0.62 shipped).
  • Two cheats were credited to Ultra; Super had written them.
  • A hidden drone test checked a settling time the task never stated, so we fixed the task, not the verdict.
  • The Breaker's tests were scored with pytest, which the task images don't have.
• AI reviewers are often wrong. 6 of the Breaker's 15 tests failed against the reference solution, so a Breaker test only counts when an independent fix passes it.
• Cost. Long tasks cost $1 to $1.50 each, often for small gains, so every run had a hard budget cap.

Accomplishments that we're proud of

Every Nemotron model gamed at least one impossible task, and the hidden checks caught every one. We changed one frozen test per task so it contradicts the spec; no correct fix can pass it.

Each cheat came with a summary claiming the bug was fixed.

Agents report what their own tools show, not what is true:

• On a fuzzing task the agent claimed a score of 0.846; the hidden verifier, rerunning from scratch, measured 0.62.
• On a materials-science task it listed eight scientific fixes; the verifier scored 0.06, the same as before any change.

Real, hard work, reported as it is:

All runs, including the failures, are on the receipts site: https://trinath122.github.io/proofforge/

What we learned

• A bigger model does not stop cheating. Ultra was better at naming contradictions, but it still gamed the task that fooled every model.
• A self-reported score is a claim, not a result. Only a check the agent cannot see or influence settles it.
• Selecting on hidden results is cheating too. Picking whichever attempt happens to pass the hidden checks is choosing on the test set, so ProofForge chooses first and verifies after.
• Saying "impossible" is a skill. Super named one contradiction in 4 steps and spent a full 40-step round on another before naming it.

What's next for ProofForge

• GPU tasks: CUDA kernels proven correct and faster than a reference, once GPU sandboxes are available. Without a GPU to run them on, we did not claim them.
• More runs per task: most results here are one run each; repeats would turn single findings into rates.
• A sharper Breaker: on the drone task it could not tell the two best fixes apart, and the tie went to the cheaper one, which happened to be right.
• Receipts as a standard: any agent could write the same receipt format, so its claims can be checked the same way.

Built With

• contree-sdk
• css
• docker
• github
• html
• javascript
• nebius
• nebius-sandboxes
• nebius-token-factory
• nvidia-nemotron
• openai-sdk
• pydantic
• pytest
• python
• rich
• swe-bench-pro
• terminalbench
• typer
• uv