Tenet 0.11.1

Full Changelog: v0.11.0...v0.11.1

Tenet 0.11.0

Full Changelog: v0.10.0...v0.11.0

Tenet 0.10.0

Full Changelog: v0.9.0...v0.10.0

Tenet 0.9.0

Two ways a file could have talked this kernel into accepting a proof of False, both closed.
Neither was reachable by the mutation harness; both came from reading what another checker had
already written down about itself.

If you are running 0.8.0 or earlier, upgrade. Both bugs are in every released version before
this one.

The two soundness fixes

A literal is not a proof of whatever the file calls Nat. A numeric literal was typed Nat by
assertion, without checking that the environment's Nat was the inductive the literal denotes. An
export declaring def Nat : Prop := False and then def boom : False := 3 was accepted, with an
empty axiom list, and tenet audit called it unconditional. That is a proof of False from a file
with no sorry and no axioms.

A primitive is checked before the shortcut named after it is taken. Computing Nat.add by
adding two machine integers, decided from the name alone, is safe for Lean because Lean ships its
prelude. It is not safe for a checker whose entire job is reading a file somebody else produced. An
export declaring Nat.add := fun a b => a made Tenet accept 2 + 2 = 4, which is false of the
declaration in front of it, and reject 2 + 2 = 2, which is true of it. All sixteen shortcuts are
now checked first: eight against their defining equations over free variables, the rest at sampled
values. A constant that fails is unfolded rather than rejected, so an unusual but honest prelude is
checked slowly instead of refused.

Also in this release

• .NET 8 support. Every package now carries net8.0 and net10.0, so a project that has not
  moved off .NET 8 can reference the libraries. .NET 10 is the faster of the two and the one the
  standalone binaries are built from.
• Agreement with a checker that carries a consistency proof. leanchecker is machine-checked
  never to accept a file declaring a theorem of type False. Across five Mathlib slices and 312,904
  distinct declarations, it and Tenet both accept in full, with counts matching exactly.
• docs/specification.md, the forty rules this kernel implements, each with its typing judgment,
  the method implementing it, and the corresponding function in Lean's C++ kernel. A test fails if a
  rule has no row or a row has no rule.
• docs/divergences.md, every place Tenet decides something differently from Lean, why, and how
  to switch it off. Anything not listed there is a bug worth reporting.
• Hostile tests, organized by what the checker takes on trust. Each asserts the attack is refused
  and that it succeeds with the defense off, so a test cannot pass by testing nothing.
• samples/Tenet.Explorer, a hundred lines that read Lean from C# with no Lean installed, built
  against the published packages so CI keeps checking that what is on nuget.org is usable.

The _nested namespace is now reserved, Nat.ble's equations no longer hold only on the newest
Lean, and the differential harness attributes the primitive divergence in both directions rather
than only the reassuring one.

Full detail in CHANGELOG.md. The
0.8.0 entry was missing and is written up there too.

dotnet tool install -g tenet

Tenet 0.8.0

Most of this release is about making the evidence say what it claims to say.

Finding things by name

axioms, why, statement, show and compare now take an export file, a single Module.olean, or a project directory. Given a directory every module is searched, so a declaration is found by its name rather than by the file it happens to live in: tenet why mathlib/.lake/build/lib/lean Finset.sum_comm answers in under three seconds across 8,275 modules.

New tenet names <target> [pattern]... lists the declarations a target defines. Every other command takes a name and until now nothing told you what the names are.

The kernel no longer takes the process down

Reduction can grow a term without bound on ill-typed input, and the unfolding limit bounds unfoldings rather than depth. A term could exhaust a 512 MB stack, and a .NET stack overflow cannot be caught: the process aborted, taking every other declaration being checked with it and leaving no report.

The kernel now probes the remaining stack as it recurses and rejects the one declaration with "expression too deep". Every recursion over a term or a universe level is guarded; the printers truncate instead of throwing, so an error message never replaces the error it was written to explain. Cost is under a percent, inside the noise.

Checks that could not fail

Three separate places reported success without measuring anything.

• The differential harness read a missing report as an empty failure list, so a checker that died was scored as accepting every declaration in the variant. A campaign where every variant was inconclusive printed zero disagreements and exited 0.
• crosscheck, the only test that can catch an .olean reader bug, could not see a binder-only difference or a let's nonDep flag. Its "binder names or implicitness" line was unreachable. Fixing it surfaced 18,499 binder differences on Init where the old comparison found 41, and 1,589 nonDep differences that were invisible. Substantive stayed at zero, now under a comparison strong enough for zero to mean something.
• tools/readercheck exists to check that: it damages an export one mutation kind at a time and asks whether crosscheck notices. It runs in CI.

Rule coverage

tenet check --rules counts each of the kernel's 40 typing and reduction rules by name, so a green run says what it exercised. All of Init reaches 36 of 40 in 52.5 million firings, and the tail is the point: Quot.ind reduced exactly once across 64,814 declarations.

The catalog is checked against Lean's type_checker.cpp and each entry states the judgment it implements. The edge-case corpus, which claimed to be dense in the rare rules, reached 25 of 40 and none of K-like reduction, Quot.ind, function eta or unit-like eta. It was rewritten against the measurement and now matches Init at 36 of 40.

A third opinion

difftest --oracle2 puts a Tenet-versus-Lean disagreement to con-leche, which is proved in Lean not to accept a proof of False. On its first real use it found that Tenet carries a level-normalization completeness gap of its own, narrower than Lean's and in the safe direction. A nightly job runs the three-way test.

Installing

dotnet tool install -g tenet

Published to nuget.org by Trusted Publishing, so no long-lived key exists. Packages now carry SourceLink and symbols, so you can step into the kernel from your own debugger.

Tenet 0.7.0

Checked against a checker with a consistency proof, and made to answer to programs as well as people.

Checked against con-leche

con-leche is an external Lean checker proven in Lean not to accept a proof of False. That is a stronger guarantee than anything Tenet offers, which is tested rather than proved, so running both on identical export files is worth more to Tenet than to con-leche.

Export	Tenet	con-leche	Agree
Init.Core	3,482	3,482	yes
Init	57,897	57,897	yes
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic	293,323	293,323	yes

293,323 distinct declarations, no disagreement. Count the largest run, not the sum: the corpora are nested.

The two reach those verdicts by visibly different routes. con-leche rewrites 62 projection functions of non-direct structure-likes to recursor form and hoists two declarations ahead of the pinned Nat operations they ground; Tenet does neither and agrees anyway.

On the same files with twelve jobs, Tenet ran Init in 5.5 s against 14.5 s and the Mathlib slice in 19.7 s against 63.1 s. con-leche's README says plainly that it is deliberately slow because the annotation work is what makes its proof tractable, so this measures the price of a proof, not a defect.

One difference in what each accepts: con-leche takes only Lean's three standard axioms and stops on anything else, so it cannot currently check FLT, which carries knownin1980s, Mazur_statement and Odlyzko_statement. Tenet checks such projects and reports which declarations rest on which assumption.

New

• --json on axioms, audit, compare, crosscheck, statement and why. Parsing prose was not an interface.
• --fail-on-axiom NAME on check: a CI gate that exits non-zero if anything rests on a named axiom. sorryAx is the obvious one.
• --sarif FILE: findings in SARIF, so a rejection or a stray sorry appears on the pull request diff rather than in a log.
• --timing: where the time went, and worker utilization. It measures the parallel contention rather than estimating it: the same Init check costs 24.2 s of kernel time on one job and 56.1 s summed across twelve.
• --names-out on crosscheck, so coverage across export slices can be unioned rather than summed.
• Native single-file binaries, a Homebrew formula, and shell completions for bash and zsh.
• A committed benchmark in tools/bench that exits non-zero on a regression.
• A verdict regression test over the edge-case corpus, pinning how structure eta, proof irrelevance, K-like reduction, quotient reduction and literal arithmetic are decided. The large runs all report zero failures and would keep doing so whichever answer were wrong.

Fixed

• The GC's adaptive heap sizing is pinned off. It costs this workload about 30% at twelve threads, and .NET 11 turns it on where .NET 10 left it off, so a runtime upgrade alone would have changed throughput by a third. With it pinned the two runtimes perform the same.
• AnalysisLevel is pinned rather than latest: with warnings as errors, a new SDK could add style rules and fail the build with no code change, which the .NET 11 RC did across 38 sites.
• compare compares the part that carries the meaning: a theorem by its type, a definition by type and value, a constructor field by field excluding the result type.

Verified on

Lean 4.35.0-rc1, 4.34.0, 4.33.1, 4.28.0, 4.24.0, 4.16.0 and 4.12.0; .NET 10 and .NET 11 RC1; Linux, macOS and Windows. Mathlib master on 4.35.0-rc1: 766,950 declarations, no failures. OpenAI's NavierStokesAndEuler, whole closure: 853,307 declarations, no failures, identical verdicts on both runtimes.

Packages

Tenet.Kernel, Tenet.Export, Tenet.Olean as libraries and tenet as a .NET tool, attached below. Dual-licensed MIT OR Apache-2.0.

Tenet 0.6.0

Two questions a kernel alone cannot answer: is my reader decoding what Lean actually stored, and are two projects stating the same theorem.

The check that agreeing with Lean can't do

Tenet reads Lean's compiled .olean files directly, which is what lets it check a project in place with no export step. It is also the riskiest thing it does, and comparing verdicts with Lean's kernel cannot test it. If the reader quietly drops a hypothesis, Tenet checks a weaker theorem than the one Lean stored, the proof still passes, and both kernels honestly say yes. The agreement carries no information.

tenet crosscheck compares every constant the reader decodes against the same constant as Lean's own exporter wrote it.

	Count
Constants compared, across all 648 modules of Init and a Mathlib slice	98,463
Identical in every field	98,375
Differing only in binder names or implicitness, which the kernel ignores	72
Same auxiliary declaration realized in a different module	16
Substantive differences	0

The 88 that differ are explained down to the last one, which matters more than the zero: an unexplained difference is where a bug hides.

Are two projects stating the same theorem?

tenet compare A.olean nameA B.olean nameB. A kernel checks that a proof proves the statement written down and never asks whether that statement is the intended one. The case a machine can settle is when somebody else has formalized the claim independently: then the question is whether the two agree.

It compares the part that carries the meaning, which depends on the kind of declaration. A theorem by its type alone, since two proofs of one statement are both proofs of it. A definition by type and value, because a signature says nothing. A constructor field by field, excluding the final result type: that names the structure itself, and two structures declared separately are distinct types in Lean however identically they are written.

Worked case. OpenAI's formalization.yaml names DeepMind's Formal Conjectures file as the independent statement of the Clay problem it adapted. Comparing across the two repositories is really comparing two Mathlib versions, so the reference was rebuilt inside the OpenAI project against its exact Mathlib, with only bookkeeping attributes stripped and two scoped notations inlined verbatim.

Every field that can differ in content is equal, including NavierStokesExistenceAndSmoothness, the one carrying the actual equations. The single difference in each derived structure is the inheritance reference to its parent, which cannot match by construction, and the parents compare equal on their own fields. The adaptation preserved the statement it started from. Whether that statement faithfully renders the Clay problem is still a question for people who read it; no kernel answers that one.

Also

• A kernel bug hunt, which found nothing, in either kernel. --kinds and --list-kinds focus a differential campaign, and eleven new mutations aim at one feature at a time: level normalization, literal arithmetic at the 2^31 / 2^63 / 2^64 / 2^128 boundaries, nested inductive metadata, recursor and constructor arity. Mutations whose result is equal to the original are marked, since a rejection there is a completeness gap and that is where both real kernel bugs were found. 122 variants, 10,548 agreed rejections, no disagreements.
• tools/edgecases, a Lean corpus dense in structure eta, proof irrelevance, K-like reduction, quotient reduction, nested and mutual inductives, literal boundaries and universe polymorphism. Both kernels accept all 58,236 declarations of its export; for several of those rules this is the only direct comparison against the reference the project has. --tail N aims mutation at it.
• Corrected what the README said about gonzalgo, per its author: it measures an axiom's reach and flags candidates, and does not prove a statement did not need the axiom.

Packages

Tenet.Kernel, Tenet.Export, Tenet.Olean as libraries and tenet as a .NET tool, attached below. Dual-licensed MIT OR Apache-2.0.

Tenet 0.5.0

Four questions a kernel can answer about a finished build, beyond "does it check".

A green Lean build tells you less than it looks. sorry is a real term of any type, so a formalization full of holes compiles perfectly, and a proof of a statement whose definitions were written that morning checks out exactly like one of a statement everybody agrees on. These commands answer the questions that remain, from the compiled .olean files, with no Lean installation needed.

New

• tenet axioms FILE NAME... prints the axioms a declaration depends on, transitively, matching Lean's #print axioms.
• tenet why FILE.olean NAME shows a shortest chain from a declaration to each assumption it rests on, naming the module at every step. An axiom list says what a theorem depends on; the chain says which lemma brought it in. gonzalgo did this first, covers Metamath as well as Lean, and goes further by asking whether the statement itself required the axiom.
• tenet audit <project dir> accounts for a whole project at once: how many declarations stand unconditionally, and every axiom beyond propext, Classical.choice and Quot.sound that the rest carry, with the declarations that introduce each hole.
• tenet statement FILE.olean NAME... lists the constants a theorem's statement is built from, split into those the project defined itself and those from established libraries. A wrong definition hides in the first group. It points; it does not judge.
• tenet show works on .olean files, and --report works in .olean mode.

Two runs

OpenAI's NavierStokesAndEuler (commit 8937a8f), whole import closure in one pass, nothing trusted in the middle:

$ tenet check NavierStokesAndEuler --all
OK: 850211 checked in 13068 modules, 0 failed, 679.5s, 12 jobs

Its four headline theorems rest on propext, Classical.choice and Quot.sound, and nothing else.

The FLT project (commit 81d8bee) gives the other answer, and it is the more interesting one:

$ tenet audit flt
flt: 9821 declarations defined by this project in 262 modules
  unconditional: 9630 (98.1%)
  resting on an assumption: 191 (1.9%)
    knownin1980s      106 declarations   (a named axiom this project introduces)
    sorryAx            90 declarations   (an unfinished proof)
    Mazur_statement     1
    Odlyzko_statement   1

The largest assumption is not sorry. An audit that grepped for it would report 99.1% and miss the bigger one; the first version of this command did exactly that. FLT documents all of this in its own source, and tenet why traces the main theorem straight through the project's own reduction chain to the two places the work stands.

Fixed

• A kernel path looked constants up with a lookup that returned null instead of the one that rejects, so an unknown constant could pass where the reference kernel rejects it.
• RecursorInfo.GetMajorInduct walked only pis where the reference walks lambdas too.
• The string-literal constant is read from the environment rather than hardcoded, since it changed with String's representation across Lean versions.
• Error messages print expressions with a bound; an unbounded printer could exhaust memory formatting a rejection.

Packages

Tenet.Kernel, Tenet.Export, Tenet.Olean as libraries and tenet as a .NET tool, attached below. Dual-licensed MIT OR Apache-2.0.

Tenet 0.4.0

Checked against several Lean toolchains, and used to re-check a published formalization.

Re-checking OpenAI's NavierStokesAndEuler

openai/NavierStokesAndEuler (commit 8937a8f) formalizes finite-time blowup for the three-dimensional Navier–Stokes and Euler equations in Lean 4. Tenet accepted 91,178 declarations across all 2,486 of the project's modules, with 0 failures, in 212 seconds. Its four headline theorems depend on nothing but the three standard axioms:

Theorem	Constants	Axioms
Euler.euler_breakdown_R3	89,915	propext, Classical.choice, Quot.sound
Euler.exists_compact_smooth_euler_singularity	94,404	the same three
NavierStokes.Comparator.navier_stokes_breakdown_R3	93,446	the same three
NavierStokes.Comparator.navier_stokes_breakdown_periodic	89,881	the same three

These lists agree with what Lean itself printed during the build. What the run establishes is narrow: a kernel written from the type theory rather than translated from Lean's code follows every step of those proofs and agrees, and no sorryAx appears. Whether the formal statements match the informal problem is a separate question no kernel can answer.

New

• tenet axioms FILE NAME... prints the axioms a declaration depends on, transitively, as Lean's #print axioms does. Works on exports and on compiled modules.
• tenet show FILE.olean NAME... prints declarations from a compiled module and its imports.
• A toolchain matrix in CI. Each job installs a Lean toolchain and checks its whole Init library in place: 4.34.0-rc2, 4.33.1 and 4.28.0 are clean.

Fixed

• The constant a string literal reduces to is version dependent (String.mk while String was a structure over List Char, String.ofList since the UTF-8 representation). Tenet had the current name hardcoded, as the reference kernel does, so rfl proofs such as String.length_empty were rejected on older toolchains. It now reads the name from the environment. Found by checking Lean 4.20.
• Helpers of Lean's old code generator (_cstage, _spec_, _elambda) are skipped and counted rather than failed: they reference constants the generator never stored, so no kernel can check them from module data.
• An unknown constant failure now says when no loaded module stores the constant.

Packages

Tenet.Kernel, Tenet.Export, Tenet.Olean as libraries and tenet as a .NET tool, attached below. Dual-licensed MIT OR Apache-2.0.

Tenet 0.3.1

Hardening and adoption.

Hardening

• The .olean reader cannot be crashed by a damaged file. Every raw read is bounds-checked and every stored pointer must lead to an earlier object (Lean's compactor writes children first, and later parts only point into earlier ones), so any walk over the object graph terminates and the only possible outcome is an OleanFormatException, which tenet check reports as a file error (exit 2). A corruption fuzzer over the checked-in Init.Coe module runs with the tests; its first run caught a BinderInfo check throwing the wrong exception type.
• The classic attacks as tests. Non-positive inductives (Curry), a constructor argument in a universe too large for its type (Girard), constructors that do not return their type, ill-typed indices, large elimination out of a proposition with several constructors, proofs of different propositions, Sort u : Sort u, and oversized literal arithmetic. Each test also checks the rejection reason.
• A declaration that hits the unfolding limit is reported once and not re-checked in the faithful mode.
• Tenet.DiffTest --timeout kills a checker run that does not finish; Lean's kernel has no unfolding limit and a mutation can send it into a very long reduction.

Adoption

• tenet check <project dir> checks every module a Lake project has built (its .lake/build/lib/lean).
• GitHub Action. uses: keithadler/tenet@main with project: . after lake build installs the released tool, checks the project, and writes a job summary with any failing declarations.
• tenet check FILE.olean --report out.json, as in export mode.
• Name.Parse (and --only) reads all-digit components as numeric, so private names round-trip.

Packages

Tenet.Kernel, Tenet.Export, Tenet.Olean as libraries and tenet as a .NET tool, attached below by the release workflow. Dual-licensed MIT OR Apache-2.0.