KernelProof

A correctness-first verifier, profiler, and reward generator for AI-written Triton kernels.

KernelProof treats every accelerator optimization as an untrusted hypothesis. A candidate receives no performance reward until it reproduces a higher-precision reference across deterministic edge cases, emits finite output, and repeats exactly. Passing candidates are measured with CUDA events, scored with a versioned reward contract, and optionally captured with Nsight Systems after JIT compilation and warm-up have finished.

This is not another peak-TFLOPS chart. It is the missing layer between “the model produced a kernel” and “this change is credible enough to train on or ship.”

Project status: working research prototype. RMSNorm, SwiGLU, and row-wise softmax are implemented. The RTX 5090 evidence section is populated only from committed machine-generated reports; unsupported formats and future operators are labelled as roadmap items.

Why this exists

Frontier-model development increasingly joins two loops:

1. models generate code, tool calls, or optimization proposals;
2. automated environments decide which proposals are correct and useful enough to reinforce.

GPU kernels make that decision unusually unforgiving. A candidate can be spectacularly fast because it silently mishandles a tail, overflows a reduction, assumes contiguous storage, or never executes the intended workload. It can also be correct but slower once compilation, launch variance, or the actual shape distribution is measured honestly.

Public engineering signals make this a concrete workload rather than a speculative one:

• OpenAI Triton demonstrates why specialized kernels and fusion matter for neural-network efficiency.
• OpenAI gpt-oss provides public PyTorch and Triton inference paths, BF16 activations, and native MXFP4 MoE weights.
• Anthropic publicly describes accelerator RL environments in which models learn to write correct, fast accelerator code.
• Both organizations publicly recruit for numerical validation, performance regression detection, low-precision kernels, profiling, and inference-runtime optimization.

KernelProof complements the model. It supplies the verifier, measurements, diagnostics, and reward signal that make model-generated performance work usable.

KernelProof is an independent open-source project and is not affiliated with or endorsed by OpenAI, Anthropic, or NVIDIA.

The contract

flowchart LR
A["Candidate Triton kernel"] --> B["Compile outside measurement"]
B --> C["Deterministic edge cases"]
C --> D["FP32-reference comparison"]
D -->|"fail"| E["Typed failure + reward -1"]
D -->|"pass"| F["Exact replay check"]
F -->|"pass"| G["CUDA-event distributions"]
G --> H["Versioned reward"]
H --> I["JSON training trajectory"]
H --> J["Markdown audit report"]
G --> K["Measured-only Nsight trace"]

Loading

The ordering is intentional. KernelProof does not benchmark known-wrong output and does not allow a speed score to compensate for a correctness failure.

What is implemented

Capability	Status	Evidence
FP32-oracle comparison	Implemented	Absolute, relative, mean, RMSE, cosine and mismatch count
Typed failure semantics	Implemented	Compile, runtime, shape, non-finite, tolerance and determinism verdicts
CUDA synchronization	Implemented	Candidate output synchronized before validation
CUDA-event timing	Implemented	Median, p95, minimum, maximum, mean and coefficient of variation
JIT/warm-up exclusion	Implemented	Compilation and configurable warm-ups precede measurement
Measured-only Nsight capture	Implemented	cudaProfilerApi brackets candidate samples only
Versioned RL reward	Implemented	Correctness gate + clipped log-speedup − instability penalty
JSON and Markdown reports	Implemented	One source record, full precision, reproducibility metadata
BF16, FP16 and FP32 policies	Implemented	Explicit repository tolerances
RMSNorm	Implemented	FP32 reduction, odd and production-like widths
SwiGLU	Implemented	Fused gate activation and multiplication
Row-wise softmax	Implemented	Stable FP32 reduction and tail masking
FP8 / MXFP4 candidates	Roadmap	No unverified support claim
Arbitrary-code security sandbox	Roadmap	Current runner is fault classification, not isolation
Multi-GPU collectives	Roadmap	No single-GPU extrapolation

Quick start: WSL2 + NVIDIA GPU

The project is designed to run in native Linux or WSL2 with a visible CUDA device. Keep the checkout inside the WSL filesystem for profiling work; /mnt/c/... is functional but can add filesystem noise to compilation caches and artifact generation.

git clone https://github.com/amitb-gpu/kernelproof.git
cd kernelproof
conda env create -f environment.yml
conda activate kernelproof
nvidia-smi
kernelproof list
kernelproof run --task all --dtype bfloat16

The default campaign executes every built-in shape using 10 warm-ups and 100 timing samples. Each sample contains 100 invocations and reports per-invocation latency, amortizing event and scheduling noise without hiding the distribution across samples.

Run more than one dtype:

kernelproof run \
--task rms_norm \
--dtype bfloat16 \
--dtype float16 \
--warmups 20 \
--repeats 100 \
--iterations-per-sample 100 \
--output results/rmsnorm-bf16-fp16.json

Exit codes are automation-friendly:

Code	Meaning
0	every requested case passed
2	at least one verification case failed
3	CUDA or the requested device was unavailable

Built-in workloads

RMSNorm

The candidate performs the square-and-mean reduction in FP32, applies reciprocal square root, and casts only when storing the requested output dtype. Cases include a masked 127-column tail, width 1024, the public gpt-oss residual width 2880, and widths 4096 and 8192.

SwiGLU

The candidate fuses SiLU activation and multiplication into one pass, avoiding an intermediate activation tensor. Cases deliberately include non-multiples of the Triton block size and larger throughput-oriented tensors.

Row-wise softmax

The candidate masks power-of-two padding with negative infinity, subtracts the row maximum, and uses FP32 exponentiation and reduction. Cases span tail handling through long-context-like row widths.

These kernels are compact enough to audit, but the harness—not a one-off kernel stunt—is the primary artifact.

Precision: what is and is not being claimed

FP32 is used as a numerical oracle for sensitive calculations. It is not presented as a realistic end-to-end serving format for a frontier model.

Format	Current role in KernelProof
FP32	Reference/control and strict candidate path
BF16	Primary transformer-style activation and output path
FP16	Secondary half-precision path
FP8	Planned after hardware/software-specific correctness policies are implemented
MXFP4	Planned for the public gpt-oss-20b MoE path

The default tolerance rule is elementwise:

abs(candidate - reference) <= atol + rtol * abs(reference)

Full policies and their limitations are in the methodology.

Reward semantics

KernelProof emits both a scalar and its explanation. Version 1 is:

if correctness failed:
reward = -1
else:
speed_score = clip(log2(reference_median / candidate_median), -2, 2)
instability = min(0.5, 2 * max(0, timing_cv - 0.05))
reward = speed_score - instability

That produces intuitive behavior:

• 2× faster: approximately +1 before any stability penalty;
• equal speed: 0;
• 2× slower: approximately -1;
• incorrect: exactly -1, with performance deliberately unmeasured.

The formula is identified as kernelproof.reward.v1; changing it requires a new identifier so stored training trajectories remain interpretable. See the reward specification.

Reports as training data and release evidence

Each run writes a full-precision JSON document and a derived Markdown audit report.

{
"schema_version": 1,
"config": {
"tasks": ["rms_norm"],
"dtypes": ["bfloat16"],
"warmups": 10,
"repeats": 100,
"iterations_per_sample": 100
},
"cases": [
{
"verdict": "pass",
"error": {
"max_absolute": "machine generated; never hand entered"
},
"speedup": "machine generated; never hand entered",
"reward": {
"specification": "kernelproof.reward.v1"
}
}
]
}

The real JSON uses numeric values; the strings above explicitly avoid presenting illustrative values as measurements.

For an RL system, retain candidate source and immutable task identifiers beside this report. The verdict, exception class, numerical diagnostics, timing distribution, and reward components provide a much denser learning signal than a single pass/fail bit.

For CI, treat a nonzero exit as a rejected optimization and upload the JSON report as an artifact.

RTX 5090 evidence

The committed campaign passed 26/26 cases across BF16 and FP16 on an RTX 5090 under WSL2. Each case used 20 warm-ups followed by 100 timing samples of 100 invocations. Candidate latency is reported per invocation.

Task	Cases	Candidate p50 range	Speedup range vs. included FP32 PyTorch oracle	Maximum absolute error
RMSNorm	10	9.55–20.41 µs	3.46–7.52×	1.953e-3
SwiGLU	8	8.66–16.55 µs	2.36–4.24×	9.766e-4
Softmax	8	8.88–9.80 µs	2.23–2.47×	3.052e-5

Evidence: human-readable report and full-precision JSON.

The measured-only Nsight capture provides a useful second view of the smallest RMSNorm case:

Nsight observation	Captured value
NVTX measured-candidate ranges	1
RMSNorm kernel instances	100
Kernel execution, average / median	0.741 / 0.736 µs
Kernel execution, min / max	0.704 / 0.800 µs
cuLaunchKernelEx host API median	4.791 µs

The difference between sub-microsecond kernel duration and effective callable latency is not a contradiction. For tiny shapes, launch and orchestration gaps dominate the end-to-end operator path. That distinction is precisely why the repository retains both CUDA-event measurements and an Nsight trace. See the curated Nsight output.

These are comparisons against the included reference callable, not claims against every vendor or framework implementation. Raw .nsys-rep and SQLite files remain ignored because they are bulky, stack-specific diagnostic artifacts. A beautiful README is not permission to invent a benchmark.

Nsight Systems: capture the measurement, not initialization

conda activate kernelproof
bash scripts/profile.sh

The script uses:

--capture-range=cudaProfilerApi
--capture-range-end=stop

KernelProof compiles the candidate and completes its warm-ups first. It then calls cudaProfilerStart(), submits measured candidate launches, synchronizes, and calls cudaProfilerStop(). The resulting trace therefore answers a narrow question: what happened during the candidate measurement region?

This avoids the common error of publishing an aggregate that quietly combines CUDA context creation, JIT compilation, an oracle implementation, warm-up kernels, and the code under evaluation.

Repository layout

kernelproof/
├── src/kernelproof/
│ ├── correctness.py # numerical and deterministic gates
│ ├── measurement.py # CUDA events and profiler bracketing
│ ├── reward.py # versioned RL reward
│ ├── verification.py # orchestration and failure taxonomy
│ ├── reporting.py # JSON + Markdown evidence
│ └── tasks/ # reference/candidate workload pairs
├── docs/
│ ├── ARCHITECTURE.md
│ ├── METHODOLOGY.md
│ └── REWARD_SPEC.md
├── scripts/profile.sh
├── tests/
└── .github/workflows/ci.yml

Design decisions

Why CUDA events instead of time.perf_counter()?

GPU work is asynchronous. Host wall time can stop when Python has merely submitted work. CUDA events measure elapsed time on the GPU stream and are synchronized before the samples are read.

Why median and p95?

A single minimum encourages benchmark gaming; a single mean is sensitive to outliers. Median captures the central launch and p95 exposes instability. Minimum, maximum, mean, sample count, and coefficient of variation remain in the evidence record.

Why exact deterministic replay if tolerances already exist?

Tolerance answers whether a candidate agrees with the oracle. Exact replay asks whether the candidate agrees with itself for identical inputs. They catch different failures.

Why not time failed candidates?

Because “fast but wrong” is not a point on the same optimization curve. Removing its performance signal prevents an optimizer from exploiting numerical or shape bugs for reward.

Why separate JSON and Markdown?

JSON is the source of truth for training and automation. Markdown is a review surface generated from the same object. Human formatting never reduces the precision of stored evidence.

Known limitations

• Built-in cases are deterministic and intentionally varied, but they are not exhaustive fuzzing.
• CUDA events measure stream execution time, not end-to-end request latency.
• The current candidate runner is not a security boundary for arbitrary model-generated code.
• Results on one RTX 5090 do not predict H100, B200, Trainium, TPU, or multi-node behavior.
• Allocation behavior is part of the included callable and may differ from a production memory pool.
• Reward v1 does not yet include compile time, peak memory, or energy.
• There is no claim that these demonstration kernels outperform every vendor or framework kernel.

Roadmap

1. Add randomized property-based shape generation and adversarial numeric distributions.
2. Add fused residual + RMSNorm and RoPE tasks.
3. Integrate gpt-oss-20b MXFP4 expert routing and grouped expert matmul.
4. Add FP8 policies with hardware-qualified reference paths.
5. Run candidates in disposable workers with compile and execution watchdogs.
6. Store raw timing samples and compare hardware-matched baselines in CI.
7. Add peak-memory and energy components under a new reward-specification version.
8. Add model adapters that return diagnostics to a coding agent for iterative repair.
9. Extend the task contract to multi-GPU collectives and communication/computation overlap.

Development

CPU-only policy and report tests run without importing Triton:

python -m pip install -e ".[dev]"
pytest
ruff check .
ruff format --check .

GPU verification is deliberately separate from hosted CI because a green CPU unit-test job is not evidence that a Triton kernel compiled or ran correctly on an NVIDIA GPU.

See CONTRIBUTING.md, the architecture, and execution safety before adding candidate-ingestion paths.

License

MIT