Skip to main content
Stating the boundaries plainly is part of the product. When a kernel falls outside what the engine can prove, the result is UNKNOWN, never PASS.

​
Out of scope by design

​
What the engine proves today

Counterexamples (COUNTEREXAMPLE, UNSAFE, OVERFLOW, VACUOUS) are found for every kernel shape, including those the engine cannot prove. A bug is caught even when the correct version would only reach UNKNOWN.

​
Which nodes can be PROVED

A proof needs a closed form of the node’s Op Spec in the proof generator. In this release that covers: For any other node (attn.rope, attn.core, embed, lm_head, gdn.conv, gdn.core, Gemma 4’s mlp_residual with its layer scalar), a kernel with no counterexample ends UNKNOWN. So does a kernel with two output stores (a residual add fused with the next norm, which writes both the residual and the normalised row), and a value subgoal no lemma and no search entry closes (the norm computed as exp(−½ · log v)). Counterexample search, overflow and safety checks still run for these nodes.

​
Why attention is UNKNOWN today

The algorithm-level theorems already exist in the spec library and are kernel-checked:
  • flashAttn_eq: FlashAttention (online softmax, block skipping) equals the attention head of the spec;
  • chunkDeltaRule_eq: the chunked (WY-form) gated delta rule equals the recurrence, for every chunk size;
  • online_softmax_rescale and splitKV_lse_merge (built-in lemmas).
Wiring them into the proof generator, so that a kernel’s lifted loop is matched against them, is the next milestone. Until then those kernels stay UNKNOWN, and you can waive them with an owner and an expiry date.

​
CUTLASS

For CUTLASS and CuTe kernels, device-IR lifting is on the roadmap. Today the engine reports UNKNOWN. When Volta is available, it adds PTX-level evidence:
  • A Volta REJECT that is numerically confirmed is a genuine FAILED (COUNTEREXAMPLE, or UNSAFE for a data race).
  • A Volta ACCEPT is recorded as evidence in the result, never turned into a PASS: Volta itself does not claim soundness.

​
Model-scale limits of conformance

Model conformance runs the Lean oracle in float64. By default it uses a reduced-width configuration of the same architecture. The theorem reduced_same_architecture proves it has the same layer pattern, attention variants and norms as the checkpoint. A full-size run (--full) or the checkpoint cross-check (--pretrained) of a 30B model needs the model in float64 in memory: about 8 bytes per parameter, so roughly 250 GB.

​
Roadmap