We build the instruments we audit with.
An audit is only as deep as what it can reach. Most of the defects worth finding sit in places a human reader runs out of patience before reaching, and where ordinary tooling has no reason to look. So we build the instruments ourselves, and where the instrument is general we publish it.
At the centre is Proof, our own audit engine. It's proprietary and it stays that way. Around it sit instruments we've published, because a tool that is general is more useful in the open, and because a tool nobody can run is a claim rather than an instrument.
The published ones you can clone and run against your own code today, before you talk to us about anything.
# the published instruments git clone https://github.com/probelabs/probe code context at enterprise scale git clone https://github.com/probelabs/json-fuzz structure-aware JSON fuzzing git clone https://github.com/probelabs/graphql-fuzz the same method over GraphQL proof is not in this list. The engine is commercial and not public.
Proof is the backbone of a Continuous Correctness Audit.
It holds the requirements model, drives the verification chain, carries the obligation catalog that grows with every engagement, and produces the evidence corpus that ends up in your repository.
It's what makes the audit continuous rather than a one-time report. The requirements, the reproducers, and the regression witnesses are durable objects, so the next release is checked against everything established before it instead of being read from scratch. An audit that ends when the invoice clears is a snapshot. This one accumulates.
Each engagement also leaves something in the catalog. An obligation written to close one escape becomes a question we ask of the next component, in the next language, on the next engagement.
Modified Condition/Decision Coverage: evidence that each condition in a decision can independently change that decision's outcome. Standard in avionics and automotive work, and rare outside them. We built ours for Go because nothing we could run met the bar. Line coverage tells you a statement ran. This tells you a compound boolean was exercised.
Kind2 checks whether a set of requirements can be satisfied at all, before anyone writes code against them. A specification that can't be implemented is much cheaper to find in week one.
Z3 for properties that admit a proof rather than a sample. Not claimed for every component by default, and we state where it applies and where it doesn't.
One command over specification, code, tests, and documentation, running in your CI on your runners. This is what makes the audit re-runnable after handover, and it is the difference between a report and a corpus.
What's ours, and what you depend on
Proof is commercial and it is not public. We'd rather say that plainly than imply an openness that doesn't exist.
What you receive isn't access to the engine, and it also isn't a dependency on it. The requirements, reproducers, regression tests, and the gate that runs them are plain files in your repository, and they keep working whether or not we do.
probe, the first instrument we published.
A code and markdown context engine built to work on enterprise-scale codebases. It's the instrument that makes auditing a large unfamiliar repository tractable.
Most tooling reads code as text: grep some files, open some lines, hope the relevant part was in the window. That holds up on a small project and falls apart on a real one, which is exactly the kind we get asked to audit. probe treats code as code. AST parsing understands structure, semantic search finds what matters, and a single call returns complete context instead of a dozen rounds of guessing.
This is upstream of every other instrument here. You can't audit behavior you were never able to locate, and on a codebase of any size, locating it is most of the work.
Why it matters for an audit
AST-aware, so a call site is a call site and not a string match.
Built for repositories too large to hold in any single context.
Semantic search over the whole tree instead of sampled reading.
Every path that touches an audited behavior gets found, not the first few.
The eighth panic site in §6 is the argument for this in miniature: the same unsafe assumption survived behind different syntax, where a text search had already reported all clear.
json-fuzz mutates where meaning changes.
A grammar-driven JSON fuzzer that mutates at structural boundaries rather than at random byte offsets, and that checks far more than whether the process stayed alive.
jsonparser had already been through OSS-Fuzz, which found a real Delete
panic. It still missed several defect classes, and the reason is worth stating precisely,
because it is the reason this tool exists. The harness mutated JSON bytes while holding key
paths fixed at values like "test". No amount of byte mutation reaches a panic
that requires an empty path component when the path itself never varies.
json-fuzz generates valid JSON from a grammar, then mutates where meaning changes: after a colon, inside a Unicode escape, before a closing delimiter, in an adversarial key path.
The aliasing gate exists because of a real defect:
Set and Delete could corrupt a caller's input through
append on a slice with spare capacity. The returned slice looked correct while
the original backing array had been overwritten.
What it asserts, beyond "did it crash"
encoding/json.
graphql-fuzz applies the same idea to a different grammar.
Generation over GraphQL operations, schemas, and Federation directives, rather than byte mutation over serialized text.
Grammar-aware generation reaches shapes that random mutation effectively never produces. A malformed brace is easy to stumble into. A schema whose type extensions interact in a specific order is not.
Work aimed at hardening a ten-year-old JSON parser produced a method that transferred to a different language, a different runtime, and a different protocol. That transfer is the argument for building instruments.
The tools do the reading. Review does the judging.
We're proud of this toolchain and it's why an audit can go deeper and keep running. It isn't why an audit is correct.
keys[depth:][0][0].
The search reported all clear while the same assumption survived behind different syntax. Matching a pattern finds instances. Closing a class needs someone who understands the class.
The wrong input category entered a branch coverage had confirmed was reachable. Coverage knew the branch could execute and had nothing to say about which output was semantically correct. We published that as a blameless proof-gap postmortem instead of hardening the tool in private, and turned each escape into a new obligation.
This is the honest shape of the thing. The instruments give reach and repeatability. A named reviewer decides what is a defect, what it means, and what it's worth. That's what expert-signed, machine-verified means in practice: every finding is validated by a named reviewer before it reaches you.
Assurance is bounded: within a declared scope, for declared behaviors, with evidence commensurate to the consequence of failure. No instrument on this page changes that.
What you keep.
Proof and the obligation catalog stay ours. Everything the engagement produces about your software is yours.
What you keep from an engagement is the part that matters to you: the approved requirements, the reproducers, the regression tests, the known-issue register, and a gate that runs without us. Plain files in your repository. If we disappear, none of it stops working.