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

# Trust model

> What you have to trust for a PASS to mean what it says, and what you can check yourself.

The verification engine is closed source. You do not need to trust it, because every PASS ships with a Lean 4 proof that the standard Lean 4 toolchain checks on its own. This page lists exactly what a PASS depends on.

## What you do not need to trust

> [card] The engine
>
> It only *proposes* proofs. A PASS is declared after the Lean kernel accepts the certificate, and `#print axioms` lists only `propext`, `Classical.choice` and `Quot.sound`.

> [card] The Lemma Hub
>
> Every lemma is re-checked when it is admitted, when the engine packs it, and when you re-check a release. Its Lean source ships with the proofs.

> [card] Spec Hub's servers
>
> Packages are content-addressed and signed with Ed25519. The lock pins the digest, and a package whose digest differs from the lock is refused.

> [card] Us
>
> A release certificate, its proofs and its lemma closure can be re-checked offline with stock Lean and Mathlib. See [Re-check proofs](https://docs.theformalera.com/guides/recheck-proofs.md).

## What you do trust

Every release certificate lists its trusted base in the `trusted` field:

```json theme={"system"}
"trusted": ["Lean 4 kernel", "IR-to-Lean translation", "triton frontend", "ptxas",
            "trusted external library (embed)", "trusted external library (lm_head)"]
```

| Trusted | Why | Mitigation |
| - | - | - |
| The Lean 4 kernel and Mathlib | Every proof is checked by them | Small, widely audited kernel |
| The IR-to-Lean translation | The engine turns Triton IR into Lean definitions; the proof is about those definitions | Each definition carries its IR op and source line, so you can audit the translation; publishing the Lean semantics of Triton IR is on the roadmap |
| The Triton front end, LLVM, `ptxas` | Everything below the IR that runs on the GPU | Out of scope |
| Libraries you declare under `[trusted]` | Nodes you compute with cuBLAS, `torch.nn.Embedding`, … | Listed by name in the certificate |
| The spec itself | A proof shows "kernel = spec" | Spec conformance checks, below |

## Trusting the spec

If a spec is wrong, every proof against it is wrong in the same way. Each spec earns trust in four ways, and its Spec Hub page shows the status of each:

1. **Conformance to the official implementation.** The official Hugging Face implementation is run in float64 against the Lean oracle, layer by layer, on random weights. All eight models agree to within `4.1e-14` (relative). See [Results](https://docs.theformalera.com/conformance/results.md).
2. **Weight-level cross-check.** The oracle runs on the published checkpoint and real prompts, compared to the official implementation (`--pretrained`).
3. **Machine-checked properties.** The spec library proves 37 theorems about its own definitions: causality of every model, softmax shift-invariance, RoPE encodes relative positions, the chunked delta rule equals the recurrence, and the published configurations are well formed.
4. **Publisher signature and public audit.** Packages are signed; every public spec's Lean source is public.

> [!NOTE]
>
> A spec can only be as right as the reference it is checked against. If the official implementation has a bug, the conformance check makes the spec inherit it.

## Assumptions and guards

A proof holds only when its hypotheses do: the layouts you declared, the assumptions you wrote in `assume=`, and the model constants passed as arguments (for example, `eps == 1e-06`). `theformalera guards` generates a host-side check for each of them, so the deployed system can verify them at launch time. See [Layouts and assumptions](https://docs.theformalera.com/guides/layouts-and-assumptions.md).

The engine also checks that the assumptions are satisfiable. If they contradict each other, every kernel would be "proved". Such a run is reported as `FAILED · VACUOUS`.


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