ProofRail: Deterministic Verification for AI Agents

ProofRail verifies AI agents' "done" claims with deterministic PASS/FAIL checks on real evidence. Optional Nemotron (via Nebius) drafts checks and explains failures; it can never change a verdict.

Comment

Inspiration

AI coding agents love to say "done." Too often the code doesn't build, the tests fail, or the fix never happened. We wanted a referee that checks the claim against real evidence, and that no model, including the one that wrote the code, can talk out of a result.

What it does

ProofRail turns a task into a contract of checks (files, JSON fields, hashes, and approved test-command profiles) and runs them to produce a deterministic PASS, FAIL, or INCONCLUSIVE, with the evidence recorded: exit code, timings, and output.

  • PASS and FAIL are separate from INCONCLUSIVE, which means "we couldn't establish the result" (missing evidence, timeout, unsafe path). It is never silently treated as a pass.
  • Nemotron on Nebius is an optional assistant. propose drafts a contract from a plain-English task, and explain turns a result into plain language. Neither can set or change a verdict.
  • A web UI (built from Stitch designs) shows the live result of each run, and a no-key demo mode shows the same workflow with clearly labelled simulated AI output.

How we built it

  • Python standard library only, with no third-party dependencies. The engine, a strict contract validator, and a CLI.
  • Command checks use trusted profiles defined in code, not shell strings. The first is pytest, with an argument allowlist, a scrubbed environment, timeouts, bounded output, and resource limits (Windows Job Objects, Linux rlimits). An optional Linux mode isolates the network and filesystem with bubblewrap.
  • Hardened file access: path confinement, symlink and junction rejection, and race-resistant opens. Contract-supplied regexes run in a killed-on-timeout child process to prevent ReDoS.
  • The AI layer is a standard-library client for Nebius Token Factory (default model nvidia/nemotron-3-super-120b-a12b). Model replies are untrusted: strict JSON validation, every proposed check re-validated by the engine's own contract validator, rejects never repaired, drafts that require human review, and explanations written to separate files.
  • Over 300 automated Python tests plus JavaScript tests for the UI's result handling.

Challenges we ran into

  • Making "AI-assisted" and "deterministic" coexist. We kept the assistant out of the verification path entirely, and tests prove the engine never imports it.
  • Tests exposed real bugs: orphaned processes keeping output pipes open past a timeout, pytest not installed being reported as a test failure, and a contract validator that accepted ../ paths a model could have proposed.
  • Cross-platform security. Windows and Linux needed different race and process-limit mechanisms, and symlink tests needed Linux (WSL) to run for real.
  • Honest scoping: deciding what we could truthfully call isolated, signed, or tested.

Accomplishments that we're proud of

  • A verdict that cannot be influenced by any model, enforced by structure and by tests rather than by promises.
  • Strict handling of untrusted model output, including a hostile-provider test that tries to change verdicts and fails.
  • Security work we could demonstrate: negative-control tests that prove each mitigation actually catches the attack.
  • Everything runs offline with no credentials, and demo output is labelled as simulated everywhere it appears.

What we learned

  • Treat a model as an advisor, never the judge: validate its output with the same rules you apply to any untrusted input.
  • "Exit code 0" is not proof. A workspace's own code can fake a pass, so we label that limit instead of hiding it.
  • Tests that include a deliberately broken control are the fastest way to find a weak mitigation.

What's next for ProofRail: Deterministic Verification for AI Agents

  • Run and report on the live Nebius/Nemotron integration. So far it is tested against a local fake of the API.
  • More command profiles (JavaScript, type checkers, linters) and OS isolation by default instead of opt-in.
  • Show command evidence and AI explanations in the web UI.
  • Signed, tamper-evident results, and a CI integration that gates agent pull requests on a ProofRail verdict.
  • A contract editor, so humans review AI-proposed checks in the UI.

Built With

Share this project:

Updates

Submission history