Numerical verification for heterogeneous compute · reference vs candidate
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.
Current release · licensed, exact, agent-ready
Version 1.23.0 grows the catalogue to 188 families, adds exact storage and checkout evidence, exposes 20 bounded MCP tools, and puts every native commercial executable behind the same expiring, revocable entitlement. CPU reference truth, contracts, lowering, and parity remain aligned.
The parity CLI, MCP server, and Live service check a stamped build, entitlement expiry, credits, and device ceiling before paid work executes. Help, version, discovery, and health remain available.
The service stores only peppered key hashes and hashed installation IDs. Administrators can inspect, renew, revoke, or reset devices, with every mutation recorded in an audit ledger.
APFS checksum validation, variable-span overlap, CSR components, stable sparse assignment, growth evidence, lexical scans, segmented UInt64 ranks, and bounded span search avoid Float/JSON precision loss and return explicit refusal states.
Filesystem traversal, normalisation, persistence, deletion policy, and UI virtualisation stay with the host. SemanticCompute accelerates bounded evidence, never the decision to delete or merge.
One validated MCPB manifest advertises all 20 tools to Claude, Codex, Gemini, and editor agents. A licensed non-root Docker MCP image carries the exact source commit, a persistent device identity, SBOM, provenance, and a signed multi-architecture digest.
The bounded Live service and D1 control plane are runtime-tested locally. The public browser remains disabled until a pinned hosted runner produces its own canary receipt.
1.23 evidence and distribution additions
Public control plane · execution gate closed pending hosted runner
semanticcompute-live exposes a bounded, bearer-protected
POST /v1/check/bytes endpoint. It runs the exact Compatibility Doctor, returns the first
differing byte, and records service, engine and build identity in a versioned receipt. A Cloudflare
Worker/D1 front door now issues bounded trial tokens, reserves one credit, forwards to that Swift
process, and returns the receipt. The complete local Worker → D1 → runner path passes; the public browser
stays disabled until a hosted runner has produced its own canary receipt.
The client supplies canonical Base64 reference and candidate bytes. The service refuses unknown fields and oversized input, then reports compatibility, compared bytes, mismatch count and first mismatch offset.
Every receipt carries serviceVersion, engineVersion,
engineBuildCommit, execution target and request digest, so a deployment cannot silently
redefine the engine result.
D1 stores token hashes and expiring limits. Executed compatible and incompatible results both cost one credit; unavailable or malformed runner responses are refunded. Cloudflare's permissive rate limiter is used for abuse control, while the durable ledger remains the accounting source.
The Worker, secrets and migrated D1 ledger are publicly deployed. Health reports
control-plane-only: Cloudflare refused the CPU Container rollout because Containers require
Workers Paid. No public runner execution or chargeable public receipt is claimed. Signed receipts and
controlled GPU runners remain later gates.
The kill-shot
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 licensed binary on your machine:
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.
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.
Proof in pictures · recorded, illustrative and pending states stay distinct
A plausible image can still violate its numerical contract. These labs expose the reference, candidate, residual, boundary rule and tolerance together. Each page identifies whether it is replaying a deterministic illustration, reporting a captured local run, or waiting for a consumer execution receipt.
Switch between candidate, reference and deviation views; compare exact, ULP and mixed tolerance policies; then download the deterministic fixture statistics. This browser lab demonstrates the reporting model and does not assert that a GPU ran.
A 48 × 48 SeparableConv2D fixture makes implicit zero padding visible against the declared clamp-to-edge contract. The page preserves the historical engine version and separates its recorded family/MCP statistics from the explanatory browser canvases.
A public synthetic mask specifies the CPU reference, requested Metal route, exact binary residual, fallback disclosure and timing scope. It remains visibly pending until AssistantApp exports the first completed runtime receipt.
The extended ledger reports release-mode local family measurements from HEAD 55ae773
plus a recorded dirty-source digest, including faster, slower and parity-preserving outcomes. Its
MacResilience after-column remains empty until the same 36-checkout fixture is replayed against an
identified build.
One IR · three executed targets in-core + recorded CUDA hardware evidence
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 — 17 tests across
three suites on an RTX 4070 Ti SUPER at source checkpoint f183b0d, covering odd extents,
folded-4D dispatch, branches, NaN/±∞ semantics, uint marshalling, loops, and the float-vector layer under
a stated no-fast-math contract. Earlier RTX 5080 and RTX 5060 Ti runs provide historical device breadth. 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.
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.
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.
The compiler's optimisation passes are verified semantics-preserving by running before/after on the
GPU and comparing bit-for-bit. 1,385 tests are green on macOS (1,374 across 294 Swift Testing suites,
plus 11 XCTest cases); three backends execute in-core (Metal, C, WebGPU). The optional CUDA runner has
17 tests across three suites recorded green on an RTX 4070 Ti SUPER at source checkpoint
f183b0d. The 1.23.0 tag had no online NVIDIA runner, so families added after that checkpoint
are not claimed as freshly NVIDIA-executed in this release.
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
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
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 391 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
1.23.0 catalogue, pinned by a test — the page cannot claim families the source does not
carry. Browse them from any MCP client: sc_list_families
returns each family's reference, contract and lowering signatures.
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.
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.
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.
Twelve exact-integer families flatten recursive values under explicit limits, validate UTF-8 and CBOR structure, order canonical keys, hash bytes, encode varints and run bounded CDDL checks — while context loading, dynamic maps and diagnostic construction stay with the CPU reference.
Variable-span set overlap keeps exact numerators and denominators; sparse assignment keeps each UInt64 cost component explainable; CSR analysis exposes WCC/SCC, cycles and topological strata; irregular-time growth detection abstains when coverage, identity, timing or counters stop being comparable. These are evidence surfaces, never deletion or merge decisions.
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.
Release artifacts · licence controlled
The complete 1.23.0 distribution ships the MCP server, parity CLI, and Live service as signed, notarised universal macOS binaries and native x86-64 + AArch64 Linux archives. Every binary carries the exact tagged source commit; the release also includes checksums, an SBOM, licence notice and CUDA evidence. This release checks an expiring, revocable entitlement before CLI, MCP, or Live compute operations. Bounded trial keys can carry job and installation limits; paid keys follow their subscription. The source is closed; serious evaluators can review it under NDA. Earlier downloaded artifacts predate this gate and remain governed by their licence terms.
Prefer a manual binary? Grab one from Releases. Read the detailed 1.23.0 notes or the complete changelog. Per-client setup (Claude Desktop · Claude Code · Codex · Gemini · VS Code · Cursor · Windsurf) 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 published 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. The installer registers the same checksum-verified executable with Claude Code, Codex and Gemini CLI; Claude Desktop uses the bundled MCPB, while VS Code, Cursor and Windsurf use their native local-MCP setup paths. New distribution builds require an active trial or subscription key; source review is available under NDA.
A runnable catalogue of the canonical silent CPU↔GPU divergences. An active trial or subscription
key lets --zoo reproduce each one so you can confirm what the doctor catches on your own
machine, without the source.
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.