Numerical verification for heterogeneous compute · reference vs candidate
Prove your kernel agrees with your reference. To the ULP.
Two implementations of the same computation — a CUDA, Metal, Triton or hand-written kernel and the
reference you trust — and they disagree. SemanticCompute tells you where, by how many ULPs, and
the likely cause (FMA contraction, reduction order, denormal flush, NaN) — classified with
evidence, not guessed — and whether a tolerance actually makes sense. Any two arrays, whatever produced them:
CPU↔GPU · GPU↔GPU · kernel↔reference · backend↔backend.
And because two backends can agree on the same wrong answer, where a family ships a
higher-precision ground truth (as CompensatedSum does) the same doctor checks the answer is
right, not merely reproducible.
It doesn't rewrite your kernel. It classifies the cause, prescribes the fix, and re-verifies yours worked — diagnose → prescribe → re-verify. Where the divergence is legitimate approximation, it prescribes a stated tolerance, not a change.
The kill-shot
Silent divergence, caught — and localised.
Point it at any two arrays — a CUDA, Metal, or hand-written kernel result and
the reference you trust, whatever produced them. It tells you where they diverge, by how many
ULPs, and the likely cause (classified, with evidence), and which tolerance tolerates what.
Four canonical culprits — and the classification is not a heuristic left unexamined: it is tested
against a failure lab of engineered specimens, each with a declared cause the doctor must
recover (--zoo all), in CI and in the free binary on your machine:
Diagnose → prescribe → you apply → re-verify.
Every classified cause carries a mechanical remedy — force or disable FMA, apply the max-shift, pin the reduction order, disable flush-to-zero — and the verification report makes each divergence selectable: click one, get its diagnosis and its prescription. Your agent applies the fix through the MCP server; the doctor then re-proves the result against your reference. SemanticCompute never edits your kernel, and that is a design decision, not a gap: a verifier that writes the fix and then certifies it is grading its own work, and the independence that makes the verdict worth anything is gone. Where it can go further, it does — it recognises a known operation in your source (heuristically, with a confidence and a line number) and points you at a whole implementation that is already parity-proven across backends. You substitute it; it is re-proved against your reference. A lead you can check, never a silent rewrite.
Bring two arrays. Nothing to adopt.
It never rewrites your kernel and never asks you to adopt a runtime or framework — it judges outputs. Comparisons are float32, whole-buffer. And it is the oracle, not the input generator: you supply the arrays, so pair it with your own shape and input sweep. It can emit specimen kernels of its own, but parity diagnosis is the product.
| idx | reference | candidate | Δ | cause | policy |
|---|---|---|---|---|---|
| 0 | 0.75481230 | 0.75481236 | 1 ULP | FMA contraction (one rounding vs two) → force/disable FMA, or state ulp(1) | |
| 1 | 1.4e−45 | 0.0 | 1 ULP | denormal flushed to zero → disable flush-to-zero, or widen the tolerance | |
| 2 | 0.00000000 | NaN | special | unguarded 0/0 (reference masks it) → guard the divide, then re-verify | |
| 3 | 1000000.0 | 1000000.125 | 2 ULP | ULP drift at magnitude 1e6 — abs err 0.125 → the relative bar accepts it; ulp(1) flags it — pick the policy that fits | |
| 4 + | — | — | 0 ULP | the rest agree | pass |
Click a tolerance policy — watch what it tolerates:
Each → prescribed fix follows from the diagnosed cause — a code fix for the unguarded NaN, a stated tolerance for legitimate rounding; SemanticCompute prescribes it and re-verifies, it doesn't rewrite your kernel. (The smallest denormal and 0 are adjacent floats, so the flush is exactly 1 ULP.)
Same four culprits, live from the
failure lab,
runnable from the CLI binary: semanticcompute-parity --zoo 01-fma-contraction
Provenance-agnostic array comparison: it compares any producer's output — Triton · PyTorch · CUDA · vLLM · FlashAttention — against your reference; no integration with, or backend for, any of them is claimed. Worked examples reproduce each one's documented numerical failure mode — diagnosed and classified.
Any check can emit a self-contained HTML verification report — a shareable audit artifact. This one is the KernelBench loop closing: a generated softmax kernel diverged, then verified after the fix.
One IR · three executed targets in-core + a hardware-verified CUDA runner
The same kernel, lowered four ways — every way proven to agree.
The four backends are not a compiler pitch — they are how the doctor is tested against itself: the same kernel, lowered four ways and executed, must agree with the CPU reference before we ask you to trust a verdict about yours. A single optimising front door feeds every backend; the target is chosen only at the final emit. The parity contract, by target: Metal and portable C execute the full family suite on-host, diffed against the CPU truth; WGSL/WebGPU is validated on every specimen by a real WebGPU front end and executed on-device for the affine and matmul kernels (full-family WGSL execution in progress); CUDA is emitted by the core and executed by the optional NVIDIA runner — 16 on-device parity comparisons per board (odd extents, the folded-4D dispatch, branches, NaN/±∞ semantics, uint marshalling, loops, and the float-vector layer with an association-discriminating dot), run twice on independent GPUs under a stated no-fast-math contract, with the evidence log published (and the GPU-free NVRTC compile-gate log beside it). Verified for the covered specimens on recorded configurations — the core itself ships no CUDA runtime, and says so.
typed semantic IRlegalise · fold · CSE · DCE
Tolerance is stated, never hidden
Compare under exact, a default abs/rel bar, or ulp(n) — agreement to within
n representable floats, at any magnitude. The scale-free, gold-standard bar.
The edge cases that break agreement
FMA contraction, denormal flush-to-zero, NaN-skipping fmin/fmax, ties-away
rounding, signed zero — reproduced in the reference so the two sides actually agree.
Passes are on-device parity tests
The compiler's optimisation passes are verified semantics-preserving by running before/after on the GPU and comparing bit-for-bit. 1,137 tests across 245 suites, green on macOS & Linux; three executed backends in-core (Metal, C, WebGPU) plus the CUDA runner's on-device matrix — 17 tests per GPU, run on two boards, evidence committed.
Every line above is verbatim from the published evidence log — nothing staged, nothing summarised. The same file the CUDA claims on this page link to.
Measured, not asserted
Where the GPU wins — and where it honestly doesn't.
Batch DSP on an Apple M3 Pro, release build, against a fair multithreaded CPU baseline. Reported the way you'd want a vendor to report: with the losses in the table.
Why show the losses? Because the product is trust. The wins are real and large where the work is compute-bound and batched; they collapse toward a wash on memory-bound ops and lose outright at real-time sizes. An earlier draft mis-measured against a debug build; it was caught and corrected. That is the whole point of the tool.
The substrate · grown by consumer demand
151 kernel families — each one carrying its own proof.
A family is not a kernel in a zip: it is a CPU reference, a stated contract, and a GPU lowering that must agree — under a tolerance that is measured and justified, never inherited. Four gates hold the library honest: a symbol index in which every kernel-emitting implementation is claimed exactly once, a compile sweep across all 352 programs, a catalogue pin a new family cannot dodge, and the parity suite itself. A family lands only when a real pipeline measured the need — and ships only when every gate passes.
Counts are the
shipped catalogue at v1.13.0, pinned by a test — the page cannot claim families the binary does not
carry. Browse them from any MCP client: sc_list_families
returns each family's reference, contract and lowering signatures.
From decode to detection geometry
Surface distance (HD/HD95/ASSD), marching cubes, affine resample, mutual information, 3D IoU/ROIAlign, and a fused labelwise scatter whose bbox is contractually in absolute volume coordinates — because a consumer lost a day to a crop origin that wasn't.
A ported trunk that stays ported
Conv3D, transposed conv, instance norm and LeakyReLU in PyTorch's exact conventions — eps-inside-sqrt and cross-correlation pinned by tests chosen so no tolerance can blur which convention is implemented. Checkpoints drop in without a transpose pass.
Filters that stay positive-definite
Batched EKF in Joseph form, IMM mixing with the spread term, RTS smoothing, particle resampling with the ESS gate that decides whether to resample at all.
Percussion that stops lying
Constant-Q/Variable-Q spectrograms with per-bin Q-matched windows, and the five phase-aware onset functions — built after two independent drum models failed the same kick/conga discrimination and the defect turned out to be the spectrogram, not the models.
Signed & notarised · free to evaluate
Hand it to your agent, or run the CLI.
The MCP server and CLI ship as signed, notarised macOS binaries and prebuilt x86-64 + arm64 Linux binaries — the CLI, MCP, and library build and pass their test suite on both platforms. Free to evaluate and for non-production use, plus a 7-day production trial; production beyond that needs a commercial licence. The source is closed; serious evaluators can review it under NDA. A hosted verification service — parity CI against your own kernels — is in early access.
Prefer a manual binary? Grab one from Releases. Per-client setup (Claude Desktop · Claude Code · Cursor) is in the install guide.
Run the MCP server so an agent can verify numerics, classify the cause, and get the prescribed
fix — mid-task. Diagnosis returns a typed remediesByCause map, so the agent applies
the fix and re-verifies; a generate → verify → prescribe → re-verify loop closes automatically:
Plus MCP resources — the family catalogue and the failure lab as browsable context
(semanticcompute://families, semanticcompute://zoo) — and prompt
workflows: verify-kernel, diagnose-divergence, find-existing-family,
verify-and-prescribe.
The MCP server + CLI
The verification substrate as signed, notarised macOS binaries (+ x86-64 & arm64 Linux) — the parity doctor, the cause classifier, ULP tolerance, and measured accuracy vs a higher-precision truth. Free to evaluate; a commercial licence for production; source review under NDA.
The failure lab
A runnable catalogue of the canonical silent CPU↔GPU divergences — ships in the free download,
no licence needed: --zoo reproduces each one, so you can confirm what the doctor
catches on your own machine, without the source.
Hosted verification — get in touch
Parity CI, cross-vendor execution, and audit-trail reports for teams who have to prove their numerics — metrology, audio-ML, and regulated compute. Not yet a purchasable product.