For eval, post-training & RL teams

Turn licensed codebases into verifier-backed SWE tasks.

Proof reconstructs the intended behavior around a software component, maps its dependencies and failure modes, and ships versioned task data with deterministic checks, ready for evaluations, post-training, and RL environments.

Download the public sample Pilot on your codebase →

proof-jsonparser-sample-v1.zip · 442 KB · v1.0.1 · sha256 04b646a3…ca96729 · checksum file

Input: A codebase you own or license
Output: Intent graph + tasks + verifiers
Use: Evals · RL · failure analysis
Pilot: One component · 2–3 weeks

01 · Input → output

What goes in. What ships.

You supply one component of a codebase you are authorized to use. Proof builds the graph around it. What ships is the graph as versioned files, with the checks that decide each task.

You supply

A codebase you own or license
One component of it, named and bounded
Its history: commits, tickets, incidents
Its tests and build steps

Proof builds

Approved requirements and their dependencies
Failure modes and hazards, graded per requirement
Code and test links, machine-readable
Verified defect records with reproducers

What ships

A versioned dataset with deterministic checks
Tasks with graders: one command, exit code is the verdict
Environment material: what the task can see and run
Provenance: licence, subject commit, per-file hashes

Fig. 01 · Left to right: the input, the graph, the package. The sample lower on this page is one unit of the right-hand column, built from a public MIT subject.

02 · The task unit

One codebase task, end to end.

Every value below is read from the public sample. The task is the silent data-loss defect in jsonparser’s Set helper: the requirement it broke, the context an agent receives, the verifier, and what counts as success.

DEFECT-260727-WWWY

fixed · pin green on the packaged tree

Kindepisode ep-DEFECT-260727-WWWY · task_family bug_fix · split demo · difficulty hard · reward type toolchain

Task

Fix Set() so that a beyond-length array index appends instead of destroying the array.

reproducer from the record: Set({"a":[1,2,3]}, 99, "a", "[9]") returned {"a":[99]} before the fix and {"a":[1,2,3,99]} after

Subject

github.com/buger/jsonparser @ 6454f95de679fdd0c623a6183f7cff82da56b442 · MIT

the packaged, post-fix tree; the affected revision is historical and public, outside the zip

Intent

SYS-REQ-110 · approved · reviewed_by human:buger, 2026-07-26

When Set targets an array index [N] with N >= len(array), the parser shall append at the end and return the mutated document, not overwrite existing elements or panic.

rests on STK-REQ-005 · formalized in FRETish · the promise this defect broke

Failure class

boundary · silent data loss · severity high

hazard row on SYS-REQ-110; the record's surface is data_integrity. Sibling hazards on the same requirement: nested_mutation (medium), element_type_partition (high)

Available context

the requirement neighbourhood: SYS-REQ-110, SYS-REQ-009, STK-REQ-005 · the implementation: parser.go Set · the historical failure: DEFECT-260727-WWWY, with KI-4 as the separate top-level partition · the public tests named in the record

Verifier

go test -count=1 -timeout 120s -run 'TestSetBeyondLengthScalarArrayPreservesElements_SYS110|TestMCDC_SYS_REQ_110' .

deterministic go test pin, no LLM judge, exit code is the verdict · run through re-run/verify.sh --pin DEFECT-260727-WWWY

Success

the known witness passes: TestSetBeyondLengthScalarArrayPreservesElements_SYS110 · the requirement’s MC/DC obligation row passes · the sibling partition (KI-4, top-level arrays) carries its own explicit status

holds on the packaged tree; a red-before run needs the pre-fix commit

Provenance

PROVENANCE.json: source licence (MIT) · subject commit · producer (Proof / ReqProof) · review policy · content-root SHA-256 and per-file SHA-256 for all 201 payload files

The packaged tree is post-fix. The affected revision is historical and public, outside the zip. findings/INDEX.md says how to reach it. Green on the packaged tree means the fixed tree still holds the pinned claim.

Real record · Read from findings/problem-reports/DEFECT-260727-WWWY.yaml, hierarchy/SYS-REQ-110.req.yaml, serialization/episodes.jsonl, re-run/verify.sh and PROVENANCE.json in proof-jsonparser-sample-v1, version 1.0.1. The same files are on the public repository: the defect record ↗ · the requirement ↗

The same node, fully wired, on the full page → The postmortem behind this defect →

03 · Package schema

The package, as files.

One directory tree, versioned, with a manifest that hashes every file. The tree below is what the public sample ships today. The production layout is a target and is labelled as one.

Package schema as shipped in v1.0.1

proof-jsonparser-sample-v1/ · as shipped in v1.0.1 · 201 payload files

README.md            the entry point
PROVENANCE.json      subject commit · licence · producer · review policy · content-root + per-file SHA-256
INVENTORY.json       the counts
LICENSE              MIT, the subject's licence
NOTICE.md
serialization/       requirements.jsonl · findings.jsonl · traces_and_hazards.jsonl · episodes.jsonl · SCHEMA.md
re-run/              verify.sh · README.md
findings/            INDEX.md · problem-reports/ (8) · known-issues/ (4) · evidence/ (3)
hazards/             GRADED_HAZARDS.md
hierarchy/           OVERVIEW.md · STK-REQ-005 · SYS-REQ-009 · SYS-REQ-110 (the gold unit)
mcdc/                README.md
rl/                  ENVIRONMENT.md
corpus/              specs/ (123 requirement files) · proof/ · source/ · tests/ · docs/

Join keys are in serialization/SCHEMA.md: finding → requirement through affected_requirements[], finding → pin through reward_pin.command, requirement → test and code through the trace rows.

production package · target layout · does not ship today

task/  repo/  intent/  environment/  verifier/  provenance/
with reset.sh · hidden_checks · scoring.json

This is the layout a pilot package is scoped against. It does not ship today. The public sample ships the tree above it, and nothing in this second block.

04 · Quality controls

What a pilot package declares.

A production package answers each of these in its provenance and environment files, per package. The tag on each line says whether the public sample answers it today.

Whether the repository was ever public. answered by the public sample
Whether the task appeared in commits or issue text. pilot package
Whether future commits are reachable. pilot package
Whether outbound network is disabled. answered by the public sample
Whether hidden tests are visible to the agent. pilot package
Whether the agent can modify the verifier. pilot package
How reference patches are isolated. pilot package
How task families are split. pilot package
Which checks detect special-casing or reward hacking. pilot package

What the public sample answers today: the repository is public, under MIT. verify.sh needs no network. No LLM judge sits in the verdict path. Every pin is named, in findings/INDEX.md and in re-run/verify.sh. The sample does not answer the rest, and this page does not claim it does.

What the pilot reports

Requirements proposed / accepted / rejected
Tasks generated / accepted / rejected
Reproducer determinism
Verifier agreement
Environment reset success
Human-review time
Known grader exploits

These are the fields of the quality report a pilot returns. The numbers come from the pilot on your component. None are published here.

05 · The public sample

The public label-and-evidence sample.

One unit of the product, free to evaluate, built from the public audit of jsonparser, a zero-allocation Go JSON library long in production. Everything in the zip comes off the fixed master tree.

123 requirements · 7 stakeholder + 116 system · 116 carry a FRETish formula
12 findings serialized · 7 primary fixed defects + 1 related · 8 problem-report files · 4 known-issue records
8 episodes serialized · task_family bug_fix · reward type toolchain · 7 in the demo split, 1 in the eval split
670 trace-and-hazard rows · 201 payload files · MC/DC 100% decisions and conditions
re-run/verify.sh · Go 1.21+ · no network · no LLM judge
rl/ENVIRONMENT.md · what the demo episodes are and what they lack

proof-jsonparser-sample-v1
version 1.0.1 · created 2026-08-05 · 442 KB zip

Download the public sample

sha256 04b646a3ea14fb3938e14db8153d850e2acdaed7ecc309415b7bb3a30ca96729
checksum sidecar · the full technical page →

The public download demonstrates the schema, provenance, evidence graph, and deterministic post-fix checks. A production RL environment additionally packages the affected base revision, a reset mechanism, an isolated toolchain, and a hidden grader.

Rerun the verdicts Go 1.21+ · no network · no LLM judge

the rerun path, from the zip

$ unzip proof-jsonparser-sample-v1.zip && cd proof-jsonparser-sample-v1
$ ./re-run/verify.sh                             # all eight pins
$ ./re-run/verify.sh --pin DEFECT-260727-WWWY    # the task above
$ ./re-run/verify.sh --list                      # the pin ids

Go 1.21+ and nothing else. The script stages the packaged sources and tests into a temp module and runs go test. No network. No LLM judge. The exit code is the verdict: 0 pass, 1 test failure, 2 bad arguments. Green means the fixed tree still holds the pinned claim. A red-before run needs the pre-fix subject commit, public and outside the zip.

06 · Pilot

Pilot on your codebase.

One component, a fixed box, and a report you can check.

Input: One component of a codebase you are authorized to use: a buyer-licensed codebase, or a clearly licensable open-source slice.
Duration: 2–3 weeks of calendar time.
Commercial: Fixed fee, quoted in the first reply. Complexity or exclusivity changes the quote before work starts.
Pilot success: Accepted tasks per component

Verifier determinism

Environment reset reliability

Task rejection rate

Expert-review minutes per accepted task

Exploit / reward-hacking findings

Cost per accepted task or environment
Out of scope: Monorepo dumps. Third-party finding dumps as samples. Client or private audit work. The sale of Proof’s own product history.

Email is enough to start. hello@reqproof.com is the whole ask.

The first reply carries the fixed fee and the questions we need answered before work starts: which component, what licence you hold on it, and what the task data is for.

The long version, for due diligence: correctness labels · trust · about