Skip to main content
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

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.

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.

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.

Us

A release certificate, its proofs and its lemma closure can be re-checked offline with stock Lean and Mathlib. See Re-check proofs.

​
What you do trust

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

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