Skip to main content
Code and specs meet in one place: the verification engine. Your repository supplies kernels and annotations. Spec Hub supplies the Lean 4 definition of each model node. The engine either finds an input on which the kernel is wrong, or writes a Lean 4 proof that it is right for every allowed input, which the Lean kernel then checks.

​
The verification contract

For every input inside the node’s declared shape domain and value domain, a PROVED kernel satisfies all three of:
  1. Semantic equivalence. Every output element equals the spec’s value, with numbers treated as real numbers.
  2. No overflow. Integer index arithmetic never wraps, and float intermediates stay finite.
  3. Execution safety. No out-of-bounds access, no two programs writing the same address, and every output element is written.
In Lean this is the predicate TheFormalEra.Engine.Implements (specs/TheFormalEra/Engine/Basic.lean). For every lane of every program that executes a store:
  • two lanes never write the same address;
  • every write lands inside the output tensor and stores the spec’s value as a finite float;
  • every element of the output is written.
Numbers are real numbers. Floating-point rounding and associativity are out of scope by design. Re-ordering or re-associating a sum, a different tile size, or a different accumulation order are all the same function. The question verification answers is: is this the same mathematical function?

​
The pipeline, one kernel at a time

Each annotated kernel goes through these stages, once per constexpr configuration (every @triton.autotune config is a separate program): A PASS is declared only after the Lean kernel accepts the certificate, and #print axioms of its main theorem lists only propext, Classical.choice and Quot.sound.

​
What a certificate looks like

A certificate is an ordinary Lean 4 file in .theformalera/proofs/. It starts with the lifted kernel semantics:
It continues with the binding hypotheses (layouts of the caller’s tensors, scalar arguments, non-overlapping outputs) and ends with the theorem implements: the lifted kernel satisfies Implements for the Op Spec of its node. Values are FVal: real numbers plus ±∞ and NaN, with exact real arithmetic on finite values.

​
Value subgoals and the Lemma Hub

Most of a proof is index reasoning: the tiles cover the iteration space exactly once, every reduction term is added once. Once that is done, what remains for each output element is an algebraic subgoal: “this expression over loaded values equals the Op Spec’s expression”. The tactic tfe_close closes those subgoals:
  1. Try ring_nf. If it closes the goal, the goal is trivial and is never stored as a lemma.
  2. Otherwise, replace every non-arithmetic subterm (tensor reads, reductions) with a variable and normalise. The same algebra then gives the same statement, whatever the tile sizes, layout or operation order.
  3. Look the canonical statement up among the retrieved lemmas: a hit.
  4. On a miss, run a portfolio of closing tactics under a time budget: a search. If it succeeds, the result becomes a new lemma.
See Lemma Hub.

​
Where the engine runs

The engine is the same in all three run modes; only its location changes: See Run modes.