> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# How it works

> What happens between `theformalera verify` and a verdict, and what a PASS actually proves.

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.

```mermaid theme={"system"}
flowchart LR
  repo["Your repository<br/>kernels + @tfe.implements<br/>theformalera.toml / .lock"]
  hub["Spec Hub<br/>Lean 4 Model Specs<br/>Op Specs, shape domains"]
  lemma["Lemma Hub<br/>machine-checked lemmas"]
  engine["Verification engine<br/>lower → lift → bind → check → prove"]
  out["Verdicts<br/>Lean 4 proofs · counterexamples<br/>reports · certificate"]
  repo --> engine
  hub --> engine
  lemma <--> engine
  engine --> out
```

## 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.

> [!NOTE]
>
> **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):

| Stage | What happens | Can produce |
| - | - | - |
| 1. Discover | Read `@tfe.implements` from the Python AST (or `// @theformalera` comments in C++), with autotune configs. Nothing is imported or run. | annotation errors |
| 2. Resolve | Look the Spec Key up in the locked spec package; the model's constants (hidden size, ε, head counts) become fixed numbers, the runtime dimensions (`T`, `B`, `S`) stay symbolic. | `FAILED` for a key that names no node |
| 3. Lower | Compile the kernel to Triton IR (TTIR) with the official Triton front end, on the CPU. | `UNKNOWN` if lowering fails |
| 4. Lift | Translate the IR into Lean 4 definitions, one per IR value, each documented with the IR line and source location. | `UNKNOWN` at the first construct outside the model |
| 5. Bind | Match kernel parameters to the spec's tensors, scalars and dimensions; infer strides and layouts. | binding errors |
| 6. Vacuity | Check that the assumptions leave a non-empty shape domain. | `FAILED · VACUOUS` |
| 7. Overflow | int32 index arithmetic over the whole shape domain (SMT), float intermediates over the value domain (interval analysis). | `FAILED · OVERFLOW` |
| 8. Counterexample search | Run an instrumented interpreter on enumerated shapes against the spec's float64 reference interpreter; check bounds and write conflicts. | `FAILED · COUNTEREXAMPLE` or `UNSAFE`, with witnesses |
| 9. Proof | Generate a Lean 4 certificate of the contract for the whole shape domain and check it with the Lean kernel. | `PASS · PROVED` |
| 10. Bounded fallback | If the general proof fails, prove each enumerated shape separately. | `PASS · BOUNDED` |
| 11. Otherwise | Point at the IR construct the proof generator could not handle. | `UNKNOWN · UNSUPPORTED` / `TIMEOUT` |
| 12. Deposit | Return the reusable sub-proofs as new lemmas, and the subgoals it could not close as open goals. | Lemma Hub entries |

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:

```lean theme={"system"}
/-- `%row = tt.get_program_id x : i32 loc(#loc30)` (norm.py:16) -/
@[tfe_idx] def v10 (a : Args) (p0 p1 p2 : ℤ) : ℤ :=
  p0

/-- `%ms = arith.constant 5.120000e+03 : f32 loc(#loc28)` (norm.py:20) -/
noncomputable def v8 (a : Args) (p0 p1 p2 : ℤ) : FVal :=
  FVal.fin (5120 : ℝ)
```

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](https://docs.theformalera.com/concepts/lemma-hub.md).

## Where the engine runs

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

| `runner` | Who solves | What leaves the machine |
| - | - | - |
| `local` | The engine on your CI runner (`theformalera[engine]`) | Nothing but spec and lemma downloads |
| `cloud` | Solve workers behind Spec Hub | Lowered IR and annotations, never the repository |
| `on-prem` | The enterprise engine in your data center | Nothing leaves your network |

See [Run modes](https://docs.theformalera.com/guides/run-modes.md).


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.