PAX-Coder

The first GPU code generator that ships a machine-checked proof with every kernel.

Lean 4 · zero sorry NVIDIA sm_86 mma.sync · cp.async
Lean 4 Proof
PTX Kernel
Futhark Spec
-- Lean 4 proof will appear here
// PTX kernel will appear here
-- Futhark spec will appear here

PAX Certificate — Proof Obligations Satisfied

PO1PO2 PO3PO4 PO5PO6 PO7PO8