Triton kernel
act_fast.pysig = 0.5 * (
1.0 + libdevice.tanh(0.5 * g))
tl.store(Y + row * I + cols,
g * sig * u, mask=m)Formal verification for inference teams
Formal verification.
Less time. Less cost.
The Formal Era verifies inference operators against precise model specifications. Our extensive Lemma Hub supplies already proven results, reducing repeated proof search so verification takes less time, compute and manual work.
A verification result you can independently check with Lean 4.
Model spec
Qwen3.8 27B · mlp.act
y[t,i] = silu(gate_up[t,i]) · gate_up[t,17408+i]
Reusable lemma
Lean 4theorem exp_two_mul_half (x : ℝ) :
Real.exp (2 * (x * (1 / 2))) =
Real.exp x := by ring_nfReuses a proven identity in the SiLU proof.
01 / The advantage
Faster verification.
Less repeated work.
The expensive part of verification is repeatedly discovering how to prove familiar mathematics. Our extensive Lemma Hub gives the verifier already proven results to reuse, reducing search effort, compute and manual work.
A foundation you can reuseThe Lemma Hub
General lemmas
Mathematical identities that travel across operators.
Operator lemmas
Proof steps shared by models using the same operator.
Model lemmas
Reuse across implementations of the same model.
Shorten the verification process
When a proof obligation matches an existing lemma, the verifier cites it directly. Less repeated search means a faster path to a verification result.
Spend less on repeated proving
Reusing checked results reduces solver work and the manual effort needed to construct proofs. A matching lemma can carry that saving across configurations and models.
Keep the benefit as code changes
New implementations can build on the same mathematical results. Further checked proof steps can enrich the library for later verification runs.
Knowledge that compounds
More proven knowledge.
Less verification work.
The result is verification. The advantage is the proof library
behind it.
Reuse what is already proved to spend less on what
comes next.
02 / The platform
One verification system.
Three connected strengths.
The Spec Hub defines what your operator should compute. The Formal Verifier checks the implementation. The Lemma Hub accelerates that verification with proven results, while Lean 4 checks the final proof.
Spec Hub
Versioned model specifications establish the mathematical contract.
Explore specificationsFormal Verifier
Check your implementation against that contract and produce a verification report.
Proof · Counterexample · UNKNOWN Read verifier docs
03 / Accelerate
Lemma Hub
Reuse already proven results to reduce verification time and proving cost.
Browse lemmasPut verification into your workflow
Follow the quickstart
kernels/norm.pyTriton
import theformalera as tfe
@tfe.implements(
["Qwen/Qwen3.8-27B@1.0:layers[*].input_norm",
"Qwen/Qwen3.8-27B@1.0:layers[*].post_attn_norm"], # one kernel, two nodes
grid=("T",), # one program per row
bind={"X": "x", "W": "w", "Y": "y", "eps": "eps"},
)
@triton.jit
def rmsnorm_kernel(X, W, Y, stride_x, stride_y, eps,
H: tl.constexpr, BLOCK: tl.constexpr):
row = tl.program_id(0)
...
The spec key names the model, its version and the node in its
compute graph.
theformalera annotate --suggest
drafts it for you.
.github/workflows/theformalera.ymlGitHub Actions · also GitLab, Buildkite, local hooks
jobs:
verify:
runs-on: ubuntu-latest # no GPU needed
steps:
- uses: actions/checkout@v4
- uses: theformalera/verify-action@v1
with:
token: ${{ secrets.THEFORMALERA_TOKEN }}
level: proof
sarif: true # line annotations
comment: true # PR summarytheformalera.lockTOML
# theformalera.lock: commit it, so CI and laptops check the same spec
[[spec]]
key = "Qwen/Qwen3.8-27B"
digest = "sha256:313a42af237f0db7ec729fd0d5d9230d932d829d…"
verdictsexit status 0 only if the policy passes
PASS · PROVEDEqual to the spec for the whole shape domain, with a Lean 4
proof that the stock Lean toolchain checks again.
FAILEDA counterexample, out of bounds access, data race or
overflow. With the minimal witness, the exact region where
the kernel is correct, the suspect line and a GPU repro
script.
UNKNOWNTimeout or a construct we cannot prove yet. Never reported
as PASS: waive it with an owner and an expiry, or fail the
build.
The contract, for every input in the declared domain: output equals the spec element by element over the reals, every intermediate fits its data type, and there is no out of bounds access, race or uninitialized read.
03 / Measured proof reuse
Less search.
The same standard of proof.
In this recorded experiment, a deposited SiLU lemma closed later goals across configurations, a different implementation and another model.
762 ms
First successful solve, then deposited.
207–259 ms
Later configurations and a different implementation, using the deposited lemma.
Value subgoal timings only. These are not total verification times or a promise for every operator.
Each row is a new verification
Lower is faster
Searched and depositedReused a lemmaHub disabled
View the full experiment data
Recorded October 31, 2026 · CPU verification · No result cache
hitsView source data
Reuse across models. The SiLU lemma also closed a goal on Qwen3 0.6B. A separate RMSNorm lemma transferred from Qwen3.8 27B to Muse Glimmer 30B.
A wrong kernel still fails. The negative control used the wrong RMSNorm weight rule. The verifier returned a counterexample, with no lemma applied.
04 / Correctness you can inspect
Catch the boundary
your tests never tried.
The recorded GPU test passed four sequence lengths, all multiples of 16. The verifier found that a paged attention kernel skipped every partial final page. Explore the bug below.
token read
token skipped
past seq_len
–tokens read
–pages visited
Every length the test suite tried is a multiple of 16, the page
size. Slide to any other length: the last partial page is never
read. Nobody told the verifier which lengths to try; it reports
exactly where the kernel is correct,
seq_len % 16 == 0.
05 / Independently checkable
Reuse the proof.
Keep the scrutiny.
A matching lemma saves search. Lean 4 still checks the final proof. Each proof package includes the source of the lemmas it uses, so you can check it without access to the Hub.
Read the trust model
Independent replay summaryRecorded release
$ ./recheck.sh
Lemma dependency closure compiled
RMSNorm proof checked
SiLU proof checked
9 Lean source files
0 unfinished proofs
3 standard Lean axioms
Completed in 7.989 sStock Lean 4 toolchain. No verifier code or live Hub connection needed for the replay.
See the workflow
From kernel to verdict.
Watch a real CLI session: verify, inspect a counterexample, fix the kernel, reuse a lemma and independently check a release proof.
3 minutes, 43 seconds
The video could not load. Download the demo or contact contact@theformalera.com.
The foundation
A shared definition
of correct.
Versioned Lean 4 specifications separate a model’s mathematics from its implementation. Bind your operators to spec nodes and lock the version used in verification.
Model specifications
A few useful answers
Before your first proof.
What does The Formal Era deliver?
We deliver formal verification of your inference operators against model specifications, with a report and a Lean proof for a PROVED result. The Lemma Hub supplies already proven results that accelerate the verification process.
Why is verification faster and less expensive?
The verifier reuses matching lemmas from our accumulated library instead of rediscovering those proof steps. This reduces solver search, compute and manual proving effort. The saving depends on your implementation and the lemmas that apply.
Can one lemma work across models?
Yes, when the theorem’s assumptions match. General lemmas apply broadly. Operator lemmas can parameterize model dimensions. Model lemmas apply to other implementations of the same specification.
What happens when no lemma matches?
The verifier falls back to proof search. If it cannot close the goal within its supported paths and budget, it reports UNKNOWN. A match never replaces the final Lean check.
Does verification cover floating point rounding?
Mathematical equivalence is defined over the reals. Floating point rounding, associativity and changes in accumulation precision are outside this equivalence contract.
Are our proof contributions public?
The product supports public, organization and local libraries, with contribution controls. Lemmas referencing a private specification belong in the organization library. Discuss the right configuration in your demo.
Which operators can be proved today?
The recorded examples prove SiLU, RMSNorm and residual addition. Some attention and recurrent proof paths still return UNKNOWN. We will review your operator and its supported proof path in the demo.
How do we evaluate it with our team?
Start with one representative operator and its model. Browse the public specifications and lemma library, then follow the quickstart before you book a demo.
Start with one operator
Verify more.
Repeat less proof work.
Bring an operator and its model. See how our specifications, verifier and accumulated lemmas work together to reduce verification time and proving cost.
Explore the public Hub and documentation before committing.