About PAX-Coder

What PAX-Coder Does

PAX-Coder is a fine-tuned AI model (based on DeepSeek-Coder-7B) that generates GPU kernels paired with formal proofs. You ask it to write a kernel, and it gives you:

Lean 4 proof — A mathematical proof that your kernel is correct
PTX assembly — The actual GPU code that runs on NVIDIA sm_86 hardware (RTX 3080, RTX 4090)
Futhark reference — A high-level functional specification to verify against
PAX certificate — Which safety guarantees this kernel provides

For Whom

GPU engineers who want to ship kernels with formal guarantees
CUDA developers who want to skip manual proof-writing
Research labs building verified AI infrastructure
Companies shipping safety-critical ML models where "trust me bro" is not acceptable

What Makes It Different

Most GPU kernel generators output code you hope is correct. PAX-Coder outputs code + a machine-checked proof that it IS correct. The proof can be read by any Lean 4 compiler and verified independently—no human judgment required.

Key Topics

🎯 Getting Started

No prerequisites needed — Read User Guide in the README
30 seconds: Run via Ollama (pre-installed model)
3 minutes: Run via Python (HuggingFace transformers)
30 minutes: Train your own version locally

🔧 What You Can Ask For

IEEE-754 floating-point proofs (rounding error bounds)
GEMM kernels (matrix multiply)
Async copy pipelines (3-stage, double-buffer)
Epilogue fusion (Bias+GeLU, Residual+GeLU)
Warp reductions (shfl.sync)
Architecture mappings (axioms → proof obligations)

📋 What You Get

Every output includes:

Lean 4: Machine-checked theorem (zero sorry placeholders)
PTX: sm_86 assembly for RTX 3080 / RTX 4090
Futhark: Functional spec (compiler-verified semantics)
Certificate: Which of 8 proof obligations this satisfies

🏗️ The Five Axioms (Math Foundation)

Index Space Primacy — Each thread owns one element; proven partition
Permission Necessity — Every memory access has a fractional permission; sum ≤ 1
Synchronization as State — Barriers are happens-before edges
Warp Distinctness — SIMT reconvergence proven before barriers
Verification Non-Negotiability — No kernel ships without proof

These map to 8 proof obligations (PO1–PO8) that codify GPU safety.

🎓 Training

You can train your own version:

python3 export_training_data.py   # Extract proofs + code
./run_training.sh                  # QLoRA fine-tune (4-6h on RTX 3080)
ollama create pax-coder -f Modelfile

📜 License

Tri-licensed (BSL-1.1, AGPL-3.0, MPL-2.0). Use the Prolog reasoner to determine which license applies to your use case.

🔑 Sovereign Node Key

Production use requires a Sovereign Node Key — proof you've contributed to the stack. Not DRM; community membership. See SOVEREIGN_NODE_KEY.md.

The Repository

Folder	Purpose
`PAX/`	Lean 4 formal proofs (ConstraintDAG, PipelineDAG, Float16_Rounding, WMMA, IR_DAG)
`src/`	GPU kernel templates (PTX + Futhark specs)
`backends/`	License policy reasoner (Prolog)
`docs/`	Documentation (architecture, user guide, GTM)
`demo/`	Interactive examples

Key Files

README.md — This document + quickstart + user guide
USER_GUIDE.md — Step-by-step usage examples
PAX_ARCHITECTURE.md — 5 axioms → 8 proof obligations
PAX_CODER_README.md — Commercial integration (GGUF, CUDA, PTX, GEMM bridge)
SOVEREIGN_NODE_KEY.md — How to get a node key
LICENSE.tri — Full tri-license text

Hardware Support

GPU	Architecture	Status
RTX 3080	Ampere (sm_86)	Primary target ✅
RTX 4090	Ada (sm_90)	Secondary (TMA support planned)

Quick Links

Use it now: User Guide in README
Examples: demo/ folder
Architecture details: PAX_ARCHITECTURE.md
Commercial integration: PAX_CODER_README.md
Contribute: CONTRIBUTING.md

TL;DR: Write English prose asking for a GPU kernel. PAX-Coder generates proof + code. Ship with confidence.