Skip to main content
No. Lowering, counterexample search, overflow and safety checks, proof generation and the Lean check all run on a CPU. You only need a GPU to run a generated repro script.
No. You write annotations and read reports. Lean is what checks the proofs; you can read the specs as rendered formulas with theformalera spec show.
Verification answers one question: is this the same mathematical function? Tiling, reordered sums and different accumulation orders all change the rounding without changing the function. Proving rounding bounds is a different, much harder problem. Overflow, NaN and infinities are checked: values in proofs are reals plus ±∞ and NaN.
A test samples inputs and compares within a tolerance. A proof covers every input in the shape domain, with no tolerance. The tail-page bug passes four differential tests and is wrong for 60 of 64 sequence lengths. The reward-hacking rollouts pass allclose and compute different functions.
You do not have to trust the engine: every PASS comes with a Lean 4 proof that stock Lean re-checks. See Trust model for what is trusted: the Lean kernel, the IR-to-Lean translation and the compiler stack below the IR.
Then the proofs against it are wrong in the same way. Every spec is checked against the official Hugging Face implementation, layer by layer, in float64, and its hyperparameters against config.json. A spec bug found later gets a security advisory, which pull reports.
With runner = "local", no. With cloud, only the lowered Triton IR and the annotations are uploaded, never the repository. Lemma retrieval sends only Spec Keys and op names. Deposited lemmas contain only equations over the reals, never kernel names, file paths or annotation contents, and [lemmas] contribute = "off" disables deposits.
No. Lemmas are Lean theorems, re-checked at admission, before use and when you re-check a release. Every final proof is checked by the Lean kernel. Lemmas can only make a correct kernel’s proof faster to find.
Row kernels (RMSNorm variants), element-wise kernels (SwiGLU, GeGLU, residuals, gates), tiled reductions and GEMMs with a K loop. Attention, Gated DeltaNet and CUTLASS kernels get counterexamples and safety checks, but a correct one is UNKNOWN for now. See Limitations.
Yes, with model conformance: theformalera-conformance verify <model> <impl.py> checks a PyTorch implementation against the Model Spec, layer by layer, and reports the first layer that disagrees.
See Write and check a spec. theformalera spec new --from-export drafts a spec from a torch.export graph. Adding a checkpoint of an existing family takes one Lean record. Private specs for unreleased models stay in your organisation’s namespace or on a self-hosted Hub.