Overview
VeriTile embeds a typed Triton-style kernel language in Lean 4. It connects kernel implementations to mathematical specifications, with proofs that Lean can check and readers can inspect in the repository.
Two questions a proof can answer
Section titled “Two questions a proof can answer”- Correctness: does this kernel implement its mathematical contract? The vector addition example proves a pointwise sum, termination, and preservation of memory outside the output window under its stated preconditions.
- Equivalence: do two implementations agree on observable outputs? Stable softmax and fused SwiGLU demonstrate this under their explicit rounding models and memory contracts.
The showcase contracts use KernelIO notation: io ⊨ spec for an
implementation contract, and io₁ ≡[R] io₂ for equivalence under a rounding
model. Lower-level ComputeCorrect and ComputeRefine surfaces remain
available. The source of each theorem records its full assumptions.
From code to proof
Section titled “From code to proof”Follow the Python-to-contract walkthrough for an executable vector-add example, its assumptions, and a rejected mutation.
- Describe a supported kernel using the typed
triton { ... }DSL. - State its input/output contract or its relationship to another kernel.
- Prove the contract against VeriTile’s operational semantics in Lean 4.
- Check the proof and its dependencies with the repository’s build and trust audits.
The DSL supports tile operations, loads and stores, masks, reductions, and control flow within the documented Triton subset. The translation cookbook explains how to work with it.
Proof automation
Section titled “Proof automation”The lemma library
provides reusable facts for loops, mathematical operators, and memory.
The proving wrapper
runs an agent proof loop with a cycle limit and saved logs. The official
comparator judges the theorems selected with --theorem against a snapshot of
the original task and dependencies, checks permitted axioms, and replays the
proofs in Lean’s kernel. See the
setup and usage guide.
Artifact and bench audits also require official comparator proof replay, using
a frozen snapshot of the current repository sources. The trust gates retain
their additional checks of theorem statements and circular specifications.
What the proof covers
Section titled “What the proof covers”Algorithm-level proofs use mathematical semantics. Abstract rounding models support additional contracts, but do not establish full IEEE-754 behavior. PTX code generation, TMA, detailed hardware concurrency, and Python wrapper execution have separate boundaries. Read the semantic scope and each theorem’s assumptions before interpreting a result.