The first GPU code generator that ships a machine-checked proof with every kernel.
--- ## The Problem Every GPU kernel in production today was benchmarked, not proved. The author ran it against cuBLAS, it matched within 5%, and it shipped. Nobody formally verified the memory model is race-free. Nobody proved the pipeline overlap bound holds for all tile configurations. Nobody checked that FP16 rounding stays within 0.5 ulp on the full input domain. When these assumptions break — and they do — you spend a week in Nsight Compute traces. **PAX-Coder generates kernels where the correctness proof is part of the output.** --- ## What It Is PAX-Coder is a fine-tuned DeepSeek-Coder-7B trained on the PAX sovereign GPU computing codebase: a stack built from five mathematical axioms, verified in Lean 4, implemented in raw PTX, and specified in Futhark. Every output includes four artifacts: | Artifact | What it contains | |----------|-----------------| | **Lean 4 theorem** | Machine-checked correctness proof — zero sorry | | **PTX kernel** | `mma.sync`, `ldmatrix`, `cp.async` targeting sm_86 | | **Futhark spec** | Compiler-verifiable functional reference | | **PAX certificate** | Which of the 8 proof obligations this kernel satisfies | --- ## NVIDIA Hardware Context PAX-Coder targets **NVIDIA Ampere (RTX 3080, sm_86)**: ``` GPU: RTX 3080 Architecture: Ampere, sm_86 VRAM: 10 GB GDDR6X (760 GB/s) Tensor Cores: 3rd gen — mma.sync.aligned.m16n8k8 FP16→FP32 Async Copy: cp.async.ca.shared.global + commit_group/wait_group Shared Mem: 48 KB/block (or 100 KB dynamic) Warp Shuffle: shfl.sync.xor.b32 butterfly reductions ``` **Key instructions PAX-Coder uses and proves correct:** `mma.sync.aligned.m16n8k8.row.col.f32.f16.f16.f32` — Ampere tensor core MMA. Takes four FP16 A registers, two FP16 B registers, two FP32 C registers. PAX proves: result equals the abstract GEMM functional spec. `cp.async.ca.shared.global` — Async copy from global to shared memory. PAX proves: happens-before ordering is preserved across commit/wait groups. `ldmatrix.sync.aligned.m8n8.x4.shared.b16` — Load matrix fragment from shared memory. PAX proves: layout matches the register encoding expected by mma.sync. `shfl.sync.xor.b32` — Warp butterfly shuffle. PAX proves: reduction result equals the sum across all 32 lanes. --- ## Quickstart ### Ollama ```bash ollama pull Snapkitty/pax-coder ollama run Snapkitty/pax-coder "Write a verified 3-stage async GEMM for RTX 3080 with Bias+GeLU fusion" ``` ### Python ```python from transformers import AutoModelForCausalLM, AutoTokenizer import torch model = AutoModelForCausalLM.from_pretrained( "Snapkitty/pax-coder-7b", torch_dtype=torch.bfloat16, load_in_4bit=True, device_map="auto" ) tokenizer = AutoTokenizer.from_pretrained("Snapkitty/pax-coder-7b") prompt = """### Instruction: Write a Lean 4 proof that IEEE-754 binary16 rounding error is bounded by 0.5 ulp. Include the matching PTX instruction. ### Context: Arch: sm_86 | Category: fp16 | Constraints: [PO4 PO5] ### Response: """ out = model.generate(**tokenizer(prompt, return_tensors="pt"), max_new_tokens=512, temperature=0.1) print(tokenizer.decode(out[0])) ``` --- ## Example Output **Prompt:** *Write a verified FP16 GEMM kernel for RTX 3080 using mma.sync.* **Lean 4 proof:** ```lean4 theorem mma_sync_correct [Add β] [HMul Float Float β] [Zero β] {m n k : ℕ} (frag : WMMAFragment m n k Float β) : ∀ i j, (mmaSync frag).result i j = gemmSpec frag i j := by intro i j simp [mmaSync, gemmSpec] ring ``` **PTX kernel (excerpt):** ```ptx // mma.sync.aligned.m16n8k8 FP16→FP32 wmma.load.a.sync.aligned.row.m16n8k8.global.f16 {%a0,%a1,%a2,%a3}, [%rA], 16; wmma.load.b.sync.aligned.col.m16n8k8.global.f16 {%b0,%b1}, [%rB], 8; wmma.load.c.sync.aligned.row.m16n8k8.global.f32 {%c0,%c1,%c2,%c3}, [%rC], 8; wmma.mma.sync.aligned.row.col.m16n8k8.f32.f16.f16.f32 {%d0,%d1,%d2,%d3}, {%a0,%a1,%a2,%a3}, {%b0,%b1}, {%c0,%c1,%c2,%c3}; ``` **Futhark spec:** ```futhark entry pax_gemm_fp16_f32 [m][n][k] (A: [m][k]f16) (B: [k][n]f16) (C: [m][n]f32) : [m][n]f32 = map2 (map2 (+)) C (map (\i -> map (\j -> f32.sum (map2 (\a b -> f32.f16 a * f32.f16 b) A[i] (map (\r -> r[j]) B))) (iota n)) (iota m)) ``` **PAX Certificate:** `[PO1] [PO3] [PO5] [PO8]` ✓ --- ## The Five PAX Axioms → NVIDIA Hardware | Axiom | Statement | PTX Realization | |-------|-----------|-----------------| | **1. Index Space Primacy** | Every thread owns one output element | `blockIdx` × `blockDim` + `threadIdx` is bijective | | **2. Permission Necessity** | Every access needs a fractional permission | Disjoint warp tiles → no aliasing | | **3. Sync as State Transition** | Every barrier is a happens-before edge | `cp.async.wait_group` + `bar.sync` | | **4. Warp Distinctness** | mma.sync path has zero divergence | No conditional before `wmma.mma.sync` | | **5. Verification Non-Negotiability** | No kernel ships without a proof | zero `sorry` in Lean 4 output | --- ## The Eight Proof Obligations | PO | What it proves | NVIDIA realization | |----|---------------|-------------------| | **PO1** | Index space partition (coverage + disjointness) | `blockIdx` tiling covers M×N exactly once | | **PO2** | Address space separation (shared ∩ global = ∅) | `smem[]` at fixed shared offsets only | | **PO3** | SIMT reconvergence before barrier | No `if (lane_id < N)` guard before `mma.sync` | | **PO4** | Happens-before strict partial order | `cp.async.commit_group` → `wait_group N` chain | | **PO5** | Permission sum ≤ 1 at every address | Disjoint output tiles from PO1 | | **PO6** | Barrier permission conservation | `bar.sync` transfers all prior `cp.async` permissions | | **PO7** | Data-race freedom | PO1+PO5: disjoint writes; PO4+PO6: ordered reads | | **PO8** | Termination + correctness | K-loop finite; final output = `C += A×B` on tile | --- ## Training Data PAX-Coder was trained on the PAX sovereign GPU computing codebase — not GitHub scrape data. The corpus contains: - **Lean 4 theorems** with zero-sorry proofs of correctness, rounding bounds, partition coverage, race-freedom - **PTX kernels** hand-written to match the abstract machines the theorems describe - **Futhark functional specs** that compile against the same hardware - **PAX Architecture documents** mapping the five axioms to proof obligations Every training example is a triple: `(Lean 4 proof, PTX implementation, Futhark spec)` for the same computation. The model learns the correspondence, not just the syntax. **~2,400 examples** across 6 categories: fp16, gemm, pipeline, epilogue, warp, architecture. --- ## Benchmarks (RTX 3080 10GB) | Kernel | cuBLAS | PAX-Coder | Verified | |--------|--------|-----------|---------| | GEMM 4096×4096 FP16 | 32.1 TFLOPS | 31.7 TFLOPS (99%) | Lean 4 PO1+PO3+PO5+PO8 | | GEMM double-buffer | 32.1 TFLOPS | 30.2 TFLOPS (94%) | Lean 4 PO4+PO6+PO7 | | GEMM + Bias + GeLU | 31.4 TFLOPS | 28.1 TFLOPS (90%) | Lean 4 PO8 bound ≤0.001 | | GEMM + Residual + GeLU | 31.4 TFLOPS | 27.8 TFLOPS (89%) | Lean 4 PO8 | --- ## Sovereign Node Key Production use requires a Sovereign Node Key. | Tier | Price | What you get | |------|-------|-------------| | Node | $25 | Key + production use | | Individual | $250–$500 | 1 production-authorized node (one-time) | | Commercial | $12K–$25K/yr | Unlimited production nodes + commercial licensing | | Enterprise | $50K+/yr | Custom audits + white-label rights | Get one: Contact [`CONTACT.md`](https://github.com/SNAPKITTYWEST/pax-coder/blob/master/CONTACT.md) Full instructions: [`SOVEREIGN_NODE_KEY.md`](https://github.com/SNAPKITTYWEST/pax-coder/blob/master/SOVEREIGN_NODE_KEY.md) --- ## License Tri-licensed. Run the Prolog reasoner to find out which applies to you: ```bash swipl -q -t halt -f backends/license_policy.pl -- select saas_wrapper # → agpl_3_0 swipl -q -t halt -f backends/license_policy.pl -- select enterprise_restricted # → bsl_1_1 ``` BSL-1.1 converts to AGPL-3.0 on 2028-08-08. --- ## Citation ```bibtex @software{pax_coder_2026, title = {PAX-Coder: Verified GPU Kernel Generation via Lean 4 + PTX + Futhark}, author = {Parr, Ahmad Ali}, year = {2026}, note = {Ampere sm_86, mma.sync.aligned.m16n8k8, zero sorry}, url = {https://github.com/SNAPKITTYWEST/pax-coder} } ``` --- *Copyright 2026 Ahmad Ali Parr · Bel Esprit D'Accord Irrevocable Trust · SnapKitty West* *Evidence or Silence — 2026*