Bit-exact GPU kernel generation from Prolog. Every operation verified to 0 ULP against PyTorch.
LlamaTov is a compiler toolchain that generates GPU compute kernels from a declarative Prolog specification. Each kernel is verified bit-exact (0 ULP) against PyTorch's reference implementation on real GPU hardware (NVIDIA Tesla P4).
The system lifts neural network operations from source code into a backend-neutral intermediate representation (op_expr), then lowers them to multiple backends: LLVM IR (CPU and NVPTX), CUDA C, MLIR, PyTorch, and Rust. The generated code produces identical floating-point results to the reference — not approximately equal, not within tolerance, but bit-for-bit identical.
The entire toolchain — the lifters, the IR, the lowering, the emitters, the verification infrastructure — is written in Prolog and Logtalk by the Ruach Tov Collective, a collaboration between a human (Heath) and five AI agents.
11 elementwise operations × 6 backends. Watch cells turn green as each (op, backend) pair achieves 0-ULP verification. Every green cell carries provenance — the specific commit and deployment that produced it.
How much of the llama model has been lifted from C source into our intermediate representation. Tracks the progress of the source → IR pipeline.
Chronological record of verification milestones. Each bar represents a batch of operations reaching bit-exact status.
Per-operation match status between our generated LLVM IR and the reference. The census of what matches, what diverges, and why.
The first 11 verified kernels are elementwise activation functions — the building blocks of neural network inference:
Each operation is specified as a Prolog fact (op_expr/2), lowered to backend-specific code by pattern-matching rules (lower_llvm/3, lower_cuda/3, etc.), and verified by comparing the GPU output against PyTorch on the same input tensor. The verification is automated and continuous.
The toolchain follows a three-layer architecture:
The emitters are Logtalk objects implementing a common protocol (backend_protocol). Adding a new backend means adding one object — no changes to the dispatcher, the verifier, or the dashboard.
Our research papers on sorting networks, FPGA verification, and the mathematical foundations of the project:
Overview of the sorting network verification methodology.
How we verified a 32-element sorting network — the largest proven optimal by our methods.
Book-length treatment of the lattice theory underlying sorting network verification.
Full index of papers by all Collective members.
github.com/Ruach-Tov/LlamaTov — the public repository. Includes reproduction instructions, census data, and the emitter substrate.
Ruach Tov (רוח טוב, "good spirit") is a collaboration between Heath Hunnicutt and five AI agents — Mavchin, Iyun, Mavhir, Mavdil, and Medayek — working continuously since February 2026. We build tools, write papers, and verify theorems together.
