Correctness-data enrichment · Coding / RL data teams
Move the source of truth to the requirement level.
You already license source code. What is scarce is a full intent hierarchy with formal specs, hazard analysis, and code/test links — not bug tags bolted on after the fact. We recover what the system was supposed to do at every level, write machine-checkable FRETish formulas where claims formalize, grade how they can fail, and wire every claim to implementation and evidence. That graph is the gold.
Proof is a correctness-audit engine. For data teams we use it as an enrichment layer: you supply a codebase you already have rights to; we return hierarchy, FRETish specs, hazards, annotations, evidence, and findings — each human-reviewed before it ships.
Asset: proof-jsonparser-sample-v1.zip — label graph (JSONL) · provenance · re-run pins · SHA-256
Bug pairs teach “broken → fixed.” Agents need the middle layer.
Agents that specify, implement, and verify need what ordinary coding data almost never labels: intent hierarchy + graded failure modes + grounded annotations.
01 · today
What you have
Licensed trees, preference pairs, unit tests, LLM judges. Intent is latent in commits and tickets. Failure modes appear only after incidents. Models rarely see “why → what → how it fails → which test proves it.”
02 · gold
What Proof adds
Source of truth moves to requirements. A full hierarchy of specs; each claim carries hazard analysis (worst case + severity); each is annotated to the code that implements it and the tests that verify it — human-signed, re-checkable.
What we are not selling.
Not bulk unlabeled code
You already license trees. We do not compete with scrapers or corpus brokers.
Not unverified agent output
Every shipped item is machine-checked where we claim checks, and named-human reviewed.
Not our product source history
We enrich your licensed component. We do not resell Proof’s own repo as training data.
Not a bug — a linked claim.
One training-grade unit is a requirement node with edges. Bugs and reproducers hang off it; they are not the whole product.
01 · need
Stakeholder intent
Why the product exists — acceptance-level needs.
02 · system
What must always hold
System requirements — product-level guarantees.
03 · design
Component contracts
Software and interface levels when the graph needs them.
04 · hazards
How this claim fails
Worst case and severity on every shipped requirement.
05 · edges
Code + test annotations
Implements / verifies links — machine-readable, not wiki.
06 · formal
FRETish formula + evidence
Machine-checkable claims carry a FRETish formula, checked for realizability / consistency / vacuity; then coverage, findings, human sign-off.
That multi-hop supervision is what raw code and plain defect pairs do not ship.
Full stack of specs — source of truth.
We do not stop at a comment near a function. We excavate and write a stack of requirements so models (and humans) can reason from user need down to component contract.
STK · SYS
Stakeholder → system
Why · who · acceptance, then what the product must do.
SW · INT
Software → interface
How a component does it, and cross-boundary contracts when needed.
Parent/child links are explicit. Implementation and tests hang off the levels that matter — usually system and software — so the graph is queryable: pick any requirement → children, code, tests, hazards, evidence.
Why this matters for training: agents learn multi-hop structure — “this acceptance need decomposes into these system guarantees, which this package implements” — not a flat bag of bug labels.
Every machine-checkable requirement carries a FRETish formula.
Prose alone is not the bar. Requirements that are formalized are written in structured English and compiled through FRETish — a template language descended from NASA’s FRET — into temporal-logic properties that a model checker can discharge. Structural ambiguity fails at compile time; what the author meant is still read by a person.
01
Formula on the node
The requirement file holds a FRETish formula beside the prose, hazards, and links — one artifact, not a separate formalization pile.
02
Spec checked before code
Realizability, consistency, and vacuity are discharged at spec time (Kind2 / Z3 where that path is live). A contradictory or vacuous claim never enters the audit as if it were gold.
03
Then evidence on the code
Condition-level coverage (MC/DC), formal checks where mature, and findings with reproducers hang off the same requirement ID — re-runnable after delivery.
On the public jsonparser sample, 116 of 123 requirements carry a machine-checkable formal specification — FRETish compiled to temporal logic — so the “gold unit” is not only a label in English; it is a formula the toolchain has already stress-tested. Methodology · Instruments · jsonparser case
Hazard analysis is first-class gold.
A requirement without failure modes is half a label. Every shipped requirement is walked against a failure-mode catalog: which hazards apply, what a violation would cost here, and how severe that is.
What each hazard carries
Class — reusable failure type (panic-free input, path traversal, fail-open control…). Worst case — concrete consequence on this requirement, not a generic slogan. Severity — low / medium / high / critical as authored triage — not a CVSS score.
Why labs pay for this
Structured negative knowledge: how a conforming-looking implementation still fails under edge conditions happy-path tests never force. Fuel for agents that must hunt fail-open controls, silent data loss, and false assurance — before a CVE exists.
Public example on jsonparser: a system requirement’s hazard names silent data-loss in Set when an array index is beyond length — mutated document, no error. Severity high. That prose lives on the requirement, next to code and test links — not only in a separate bug ticket. The case study · the corpus ↗
The gold edges.
The hierarchy alone is not enough. Every important claim is wired into code and tests — machine-readable edges, not wiki prose.
01
Requirement is source of truth
Structured YAML: intent, parent links, hazards, FRETish formula where formalized, human review. Versioned with the repo.
02
Code implements it
Implementation sites annotated with the governing requirement ID.
03
Tests verify it
Tests name the requirement — and often the hazard or coverage cell they discharge.
Buyer takeaway: you are licensing a requirement-centric knowledge graph grounded in real source — not a PDF audit and not a pile of unlabeled snippets. Formal specs are part of the graph, not a side document.
One requirement → obligations → code → tests.
Public sample. Not a mock. One system requirement with graded obligations, an implementation site, and named tests that discharge each class.
jsonparser · public
SYS-REQ-110 · Set beyond array length shall append — never silently overwrite
Parent intent under mutation helpers. Sibling general Set contract: SYS-REQ-009 (boundary, idempotency, malformed input, nested mutation). SYS-REQ-110 is the leaf partition for the data-loss class that still had 100% MC/DC on the decision path.
Implementation: parser.go · Set() — annotated with the governing requirement IDs.
boundary · high
Silent overwrite
Beyond-length index destroys elements with no error. Discharged by MC/DC and negative boundary tests on SYS-REQ-110.
nested · medium
Wrong offset in containers
Beyond-length index inside a nested container scaffolds at the wrong offset — sibling overwrite or malformed JSON.
partition · high
Scalar-array path
Scalar-first arrays used to take a replace-container branch — entire array destroyed. Fixed; regression locked under the same claim.
Same pattern on the parent claim SYS-REQ-009. Write-up of the miss under full MC/DC: proof-gap-root-cause.md ↗. Specs live under specs/ ↗.
This is the gold unit for training: not “here is a bug,” but requirement + graded obligations + implementation edge + discharging tests per class, human-approved and re-runnable.
Archaeology → hierarchy → hazards → annotations → force.
01
Dig into history
Code · commits · PRs · tickets when available.
02
Recover hierarchy
STK → SYS → SW → INT, with FRETish on formalizable claims.
03
Grade hazards
Worst case · severity on each claim.
04
Annotate + force
Links · MC/DC · formal evidence · findings.
05
Human-signed graph
Re-checkable package you can query and re-run.
You keep the source. We deliver the requirement graph, hazards, annotations, and evidence. Condition-level coverage (MC/DC) is one evidence layer under the hierarchy — necessary, not sufficient. Hazards and intent catch classes (like silent data-loss) that coverage alone misses.
Not raw code. Not opinion tags.
Typical coding data today
- Source trees (scraped or licensed)
- Human bug tags / preference pairs
- Unit tests or LLM-as-judge rewards
- No multi-level intent hierarchy
- No graded worst-case hazards on claims
- Hard to re-verify after delivery
Models see symptoms, not contracts.
Proof correctness package
- Full requirement hierarchy (need → system → design)
- FRETish formal specs on machine-checkable claims, validated before code is graded
- Hazard analysis on each claim (worst case + severity)
- Annotations: requirement ↔ code ↔ tests
- Condition-level coverage + formal checks where mature
- Findings with reproducers, hanging off the same graph
- Named human sign-off on what ships
Source of truth at the requirement level.
Two products. One engine.
Everything above ships in two forms. Both are the same graph; they differ in what you do with it.
01 · labels
Correctness label packages
The requirement graph over a codebase you license: hierarchy, FRETish formulas, hazards, annotations, evidence, findings with reproducers. Versioned files, re-checkable after delivery. Priced per package; exclusivity changes the box — never silently.
02 · environments
Verifiable-reward environments
The same graph turned into a training harness: task in, toolchain verdict out. Scoped after a label pilot proves the graph is worth scaling.
Why the reward signal is different: agents game graders — they read future commits, special-case test inputs, and search out judge blind spots. A machine verdict cannot be gamed that way. FRETish specs compile to temporal properties checked with SMT-backed model checking (Kind2) where that path is live; condition-level coverage (MC/DC) and mutation adequacy carry the rest. High reward means the property held — re-runnable on delivery, and any day after.
jsonparser — one unit of the product, not a brochure.
Mature zero-allocation Go JSON library, long in production, heavy community use and fuzzing. The public audit is open file by file — and packaged below as a downloadable correctness-label unit a data or RL team can load, hash-check, and re-run.
123
Requirements
7 stakeholder + 116 system; 116 carry FRETish formal specs.
100%
MC/DC
Decisions and conditions measured.
7
Real bugs
Found and fixed — plus a published miss under full MC/DC.
proof-jsonparser-sample-v1.zip · v1.0.1
Sample package download
One product unit: full hierarchy, graded hazards, seven primary bugs with executable pins, MC/DC notes, RL / formal-verdict write-up — plus the three things a data buyer needs to say yes:
- Label graph + demo episodes —
requirements.jsonl,findings.jsonl,episodes.jsonl, traces & hazards - Provenance manifest — subject commit, license, producer, content-root + per-file SHA-256
- Re-run path —
re-run/verify.sh/--pin FINDING_ID(Go pins; green on the fixed tree)
Checksum: SHA-256 sidecar · start at README.md inside the zip
live
Same graph, other surfaces
Prefer browsing over a zip? The corpus stays current on GitHub; the register is live in the portal.
Why hierarchy + hazards beat coverage alone: silent data-loss in Set with no error. Affected decision paths had complete condition-level coverage; the requirement’s hazard worst-case names exactly that failure mode; the finding hangs off the same node as the code and tests.
Excerpt from the public requirement node (verbatim fields from the corpus):
id: SYS-REQ-009
status: approved
priority: shall
component: parser
fretish: the parser shall always satisfy !set_path_is_provided | set_target_exists | set_creates_missing_path | set_returns_updated_document | set_returns_not_found_error
formalization_strategy: fretish
traces:
satisfies:
- STK-REQ-005
verified_by_extra:
- mcdc_supplement_test.go
- set_spec_test.go
reviewed_by: human:buger
obligation_hazards:
- class: boundary
worst_case: 'Set on an array-index path component [N] where N >= len(array) silently overwrites element 0 or another existing element the caller did not address, destroying data and returning a mutated document with no error (PR #286 regression class).'
severity: high
Full node: SYS-REQ-009.req.yaml ↗ · Case study · Findings ledger · Live register ↗
Who operates this — and where it has been run.
Data buyers should know the process is not a research demo. The same discipline has been applied on production systems by people who ship infrastructure.
Operator
Leonid Bugaev: 20+ years in IT, 15 years in lead engineering roles, currently Head of Engineering at Tyk API Management; founder of Proof. About the practice →
Public quality sample
jsonparser: full hierarchy, hazards, annotations, 100% MC/DC, seven real bugs, and a published miss under full coverage — download as a product unit or inspect on GitHub.
Infrastructure depth
Among people leading the rsync 3.5 release effort: deep archaeology on decades-old infrastructure, including long-latent high-impact defects, with fixes landing in release. Method and outcome at that level — not a dump of unpublished finding lists.
Scale dogfood
Same process on large enterprise-grade open-source systems (e.g. API management and GraphQL router stacks). Those findings stay private; they prove volume and realism, not marketing.
Ownership stays clean.
You own the code
You supply a codebase you already licensed. Input provenance stays on your side. We do not resell your source.
We license the labels
Derived annotations and evidence only. Provenance = machine check + human sign-off under the pilot agreement. The verdict layer has no model dependency — it is deterministic tooling. If your policy restricts which models may touch the drafting pipeline, it runs on the stack you allow. Every shipped item carries a named human reviewer and a re-runnable machine check.
How a first engagement is shaped.
One component of a buyer-licensed codebase (or a clearly licensable OSS slice). History dig → structured requirements → code/test links → condition-level coverage and hazard analysis → findings with reproducers → named human review on every shipped item.
duration
2–3 weeks
Calendar time for a tight pilot box — not a monorepo firehose.
commercial
Fixed fee, quoted first
The first reply includes a quoted fixed fee for the pilot box. Complexity or exclusivity changes the quote — never silently after work starts.
success
Quality + unit economics
Your qualitative review of label quality, plus cost per verified pair vs market rates.
Out of scope for a pilot: entire monorepo dumps; unpublished third-party finding dumps as “samples”; sale of Proof’s own product history. Environments (verifiable-reward harnesses) are the second SKU — see § 11 — scoped after a label pilot proves the graph is worth scaling.
The same engine powers engineering Continuous Correctness Audits for product teams. Data enrichment is the same discipline aimed at training-grade labels. The engagement for product teams →
Talk about a pilot.
Email is enough to start: [email protected]. If you already know the codebase and component, say so — we ask the rest by email. We reply personally, and the first reply includes a quoted fixed fee for the pilot box. For engineering audits (not data packages), use the engagement form.
Case study · Methodology · Instruments · Trust · About