07. Formal proofs in Lean

Evidence: 01.4 (Lean, Mathlib, CSLib, Aeneas and the AI provers in 2026). The binding facts:

• CSLib (leanprover/cslib, white paper arXiv:2602.04846, February 2026) is the Lean library for computer science. It treats time as an effect: TimeM returns a value and a count of ticks, and tick adds to the count. Its first worked example is merge sort, with correctness and an $O(n \log n)$ bound. Its roadmap puts many undergraduate algorithms and data structures in CSLib by the end of 2026.
• Aeneas, with Charon, translates safe Rust to a pure Lean model. It has verified 16.7 KLOC of production Rust (SymCrypt, arXiv:2609.15648, September 2026). Aeneas is tied to one Lean version at a time.
• AI provers (Aristotle, Aleph, DeepSeek-Prover and others, 01.4) now close many routine Lean goals. The kernel checks every proof, so the source of a proof does not matter for its truth.

7.1 Goals and limits

The Lean part proves three things about an algorithm:

1. Correctness. The executable model meets the spec of the problem, for every input.
2. Cost. The model's tick count meets each bound of the front matter, in its model.
3. Refinement (L4 only). One real implementation computes the same function as the model.

It does not prove that the Python, Java or C implementations are correct. They are linked to the model by testing against it (09.5). The site says this in plain words on each page ("The Lean proof is about the model. The code in other languages is tested against the model.").

7.2 The Algo package

lean/
  lakefile.toml            package Algo; requires mathlib and cslib
  lean-toolchain           leanprover/lean4:v4.35.0
  lake-manifest.json       mathlib v4.35.0, cslib at a pinned commit
  Algo.lean                imports every module (generated by algo lean index)
  Algo/
    Cost.lean              TimeM re-export, tick conventions, worst-case helpers (7.4)
    Model/                 the models of computation: Comparison, WordRAM, ExternalMemory, Query
    Prelude/               shared definitions: weighted digraphs, strings as List Char, …
    Sorting/
      SortingProblem.lean  the spec of the sorting problem
      MergeSort.lean
      Quicksort.lean
    Graphs/
      ShortestPaths/
        SSSP.lean          the spec of single-source shortest paths
        Dijkstra.lean
    DataStructures/
      PriorityQueue.lean   the abstract type and its laws (7.9)
      BinaryHeap.lean
      DisjointSets.lean
      UnionFind.lean
    Strings/
      ExactMatching.lean
      KMP.lean
  AlgoExtract/             the extractor (7.12)
  AlgoOracle/              the oracle executables (7.13)
  test/                    #guard and decide tests of the specs against the cases (rule L06)
lean-aeneas/               a separate Lake package for L4 (7.6)

Pins:

• Lean v4.35.0 and Mathlib v4.35.0, the same pins as math2. manifests/toolchains.yaml names them.
• CSLib at a commit that builds with that Mathlib. The bump (7.17) moves the three together.
• Batteries comes through Mathlib. Std.HashMap, Batteries.BinaryHeap and the core List.mergeSort lemmas may be used, and the module names each one it uses.

The module path mirrors the area of the node in CamelCase: nodes/graphs/shortest-paths/dijkstra/ ↔ Algo.Graphs.ShortestPaths.Dijkstra. Rule L09 checks the mirror. A problem's spec lives in its own module, because many algorithms import it.

7.3 The structure of a module

Each algorithm module has four parts, always in this order and with these names. algo new algorithm writes the skeleton.

Part	Name	What
spec	imported from the problem module, for example Algo.Sorting.IsSort	the relation between input and output
model	the lower-camel name of the algorithm, mergeSort	a total, computable function in TimeM, as close to the main pseudocode as Lean allows
correctness	<model>_correct or <model>_<spec>, for example mergeSort_isSort	∀ x, Spec x (model x).ret
cost	<model>_time_le, <model>_time_ge, <model>_<measure>_le	the bounds of 7.4

Conventions:

• The model is written to follow the pseudocode. Each tick has a comment with the pseudocode line id that it counts (-- L9), so a reader can match them.
• The model is total. Termination uses termination_by with the measure of the human proof. No partial def in a model (rule L07).
• The model is computable. No noncomputable, so the oracle can compile it (7.13, rule L07).
• Each public theorem has a docstring in simple English that says what it proves. The site shows it (7.16).
• Helper lemmas are private unless another module needs them. A lemma that two modules need moves to Prelude or upstream (7.15).

7.4 The cost model

Algo.Cost re-exports CSLib's TimeM and adds the conventions of this project. If CSLib changes its definition, Algo.Cost adapts and the modules do not change.

-- The shape, from CSLib: a value and a tick count.
-- structure TimeM (α : Type u) where
--   ret  : α
--   time : ℕ
-- bind adds the times; `tick c` adds c.

namespace Algo.Cost

/-- `f` runs in at most `g (size x)` ticks on every input `x`. -/
def TimeBound (f : α → TimeM β) (size : α → ℕ) (g : ℕ → ℕ) : Prop :=
  ∀ x, (f x).time ≤ g (size x)

/-- For each size `n`, some input of size `n` needs at least `g n` ticks. -/
def TimeLowerBound (f : α → TimeM β) (size : α → ℕ) (g : ℕ → ℕ) : Prop :=
  ∀ n, ∃ x, size x = n ∧ g n ≤ (f x).time

end Algo.Cost

Where the ticks go. A tick counts one unit of the model of the node (model in the front matter). The models fix what a unit is:

Model	One tick is	Example
comparison	one comparison of two keys	merge sort: a tick before x ≤ y
word-ram	one primitive operation on words, or one step of the dominant loop when a lemma bounds the rest by a constant (below)	binary search: one tick per probe
graph-ops	one edge relaxation, one vertex visit, and the priority-queue operations at their own cost	Dijkstra: relax costs 1, decreaseKey costs the cost of the queue
external-memory	one block transfer of B words	external merge sort
query	one oracle query	decision-tree lower bounds
cell-probe	one probe of a memory cell	the union–find lower bound
string-ops	one character comparison	KMP: at most 2n − m comparisons

Dominant operations. On the word RAM, counting each instruction makes the model unreadable. The convention is to tick the dominant operation and to prove, once for the module, a lemma steps_le_const_mul stating that each other operation of the pseudocode runs at most a fixed number of times per tick. The constant is explicit. The human proof (06.6) uses the same argument.

Bounds are explicit functions. A cost theorem states an explicit g, for example n * Nat.clog 2 n, not an asymptotic class. Then a second small lemma links g to the class of the front matter with Mathlib's Asymptotics.IsBigO on ℕ → ℝ, for example (fun n => (n * Nat.clog 2 n : ℝ)) =O[atTop] (fun n => n * Real.log n). Rule L05 checks that a node with L3 has both lemmas for each claim, and that the class matches the front matter string (with E01).

Θ needs both sides. A Θ claim needs TimeBound for the upper side and TimeLowerBound for the lower side. The lower side may use any family of inputs (reversed lists, for example).

Average and expected cost. An average-case claim needs a distribution on inputs of size n. An expected claim needs the random choices of the algorithm as an explicit argument (a list of coins, or a PMF from Mathlib). Until CSLib has a probabilistic cost model (planned for 2027), L3 covers worst-case and amortized claims only, as Q-19 (20) decides. Average and expected claims stay at H2 with the flag expected-not-formal, and rule L05 skips them. Randomized quicksort, hashing with chaining, treaps and skip lists are the first targets when the model exists.

Amortized cost. The model of a data structure returns the new state and the tick count. An amortized bound is a theorem about every sequence of operations: the total ticks are at most the sum of the amortized costs. The proof uses a potential function in Lean, the same Φ as the human proof.

Space. CSLib has no space monad as of November 2026. Until it does, Algo.Cost.SpaceM counts a high-water mark of allocated cells in models that need it, and L3 requires space claims only when the node sets lean.space: true. Document 20 records the choice of a space model as an open question. For M0 to M3, L3 means the time and count claims.

7.5 The axiom policy

A module that a node cites as proved (L2 or higher) uses only the standard axioms: propext, Classical.choice and Quot.sound. AlgoExtract (7.12) prints the axioms of each cited theorem, and rule L03 fails when it finds anything else, including:

• sorryAx, from sorry or admit;
• Lean.ofReduceBool and Lean.trustCompiler, from native_decide and decide +kernel options that trust compiled code;
• any axiom declared in the Algo package;
• implemented_by or extern on a definition that a cited theorem depends on.

A module may hold an unfinished proof with sorry while work goes on. The node then stays at the level below, and the page says "The Lean proof is in progress". The audit counts these.

decide is allowed. It is checked by the kernel.

7.6 Refinement of implementations

L4 says that one real implementation computes the function of the model. The first and only target in this version is the Rust implementation, through Charon and Aeneas.

The flow, in algo lean refine <slug>:

1. Charon reads impl/rust/ of the node in the generated Cargo tree (08.5) and writes LLBC.
2. Aeneas translates the LLBC to lean-aeneas/Extracted/<Area>/<Name>/Funs.lean and Types.lean.
3. A hand-written or agent-written file lean-aeneas/Refine/<Area>/<Name>.lean proves the refinement theorem:

/-- The Rust `merge_sort` returns the list of the Lean model, for every input
    whose length fits in a usize. -/
theorem merge_sort_refines (v : alloc.vec.Vec I64) (h : v.length ≤ Usize.max) :
    ∃ w, Extracted.merge_sort v = .ok w ∧
      w.toList.map I64.toInt = (Algo.Sorting.mergeSort (v.toList.map I64.toInt)).ret

The theorem says two things: the Rust function does not panic on any input that fits, and its output is the model's output after the integer conversion.

The exact form depends on the conversion between Rust machine integers and ℤ, and between Vec and List. Algo.Refine.Conv holds the standard conversions and their lemmas, written once.

Rules and limits:

• Version skew. Aeneas is tied to one Lean version, which may differ from the pin. lean-aeneas is a separate Lake package pinned to the Lean version of the pinned Aeneas release. It depends on Algo by path when the two versions agree. When they do not agree, L4 is not computed, the node keeps its last L4 with the flag refine-stale, and the bump report (7.17) says so. This is open question Q-05 (20).
• The Rust subset. Aeneas supports safe Rust with loops, enums, structs, traits and borrows, not unsafe or some trait objects. An implementation written for L4 stays inside the subset. The tier-1 Rust implementation of a core node is written in the subset where that keeps it idiomatic (08.3).
• Trust. L4 trusts Charon and Aeneas to translate MIR to Lean faithfully. The page says so.
• Other languages. No L4 for them in this version. Verus (Rust), Dafny and Why3 are possible later, and document 20 records the choice. For every language, the link to the model is the differential test of 09.5. A reader sees "tested against the proved model", not "proved".

7.7 Fidelity

A proof is only as good as its statement. Fidelity is the check that the Lean statements say what the page says. It has a machine part and a human part.

Machine checks (needed for L1).

1. The spec agrees with the cases. For each case of the contract (09.2), the Lean spec, made decidable or checked by a Lean checker, accepts the expected output. For a sample of mutated outputs (a swapped pair, a wrong distance, one element dropped), it rejects them. This runs in lean/test/ with #guard and decide (rule L06).
2. Not vacuous. The spec is satisfiable on every case (some output satisfies it), and its hypotheses are satisfiable (a spec that assumes False is caught). This follows math2's checks for degenerate statements.
3. Back-translation. An agent writes the Lean spec back into English, without seeing the page, and a second model compares it with the Definition section of the problem page. A disagreement opens an issue. This check advises; it never raises a level.

Human review (needed for L1 on the core, and always for L2 to count on the core). A reviewer who is not the author of the Lean spec records reviews/<tag>/lean-spec.yaml:

reviewer: alice                    # in registers/reviewers.reg
date: 2027-02-14
problem_text: blake3:6c1e…         # hash of the Definition section of the problem page
lean_spec: blake3:9a40…            # hash of the elaborated type of the spec, from AlgoExtract
human_proof: blake3:d2f7…          # hash of proofs/invariant.md, when the review covers it
verdict:
  spec_matches_text: yes
  proof_and_theorem_same_statement: yes      # or partial, with a note
notes: >-
  The Lean spec uses List.Perm; the text says "a permutation of the input". Same meaning.

The review counts only while all three hashes are current. Any change drops the node to the level below until a new review, as in math2. Reviews are signed commits, and rule L04 checks the hashes.

A reviewer checks in particular:

• the input domain (all lists, not only lists of distinct keys, unless the page says distinct);
• the output relation (a permutation and sorted, not only sorted);
• partiality (what the model returns on an input that the problem excludes);
• the cost measure (comparisons in the theorem, comparisons in the text);
• that the human proof and the Lean theorem state the same claim (06.5, point 5).

7.8 The formal ladder L0–L4

The ladder of 04.8, with the exact checks:

Level	Needs	Rules
L0	nothing
L1	the problem spec and the model exist and build; the model is total and computable; the machine fidelity checks pass; for the core, the spec review is current	L01, L06, L07, L04 (core)
L2	L1, and the correctness theorem is proved with the standard axioms only	L03
L3	L2, and each time and count claim of the front matter has an explicit bound theorem and its class lemma; space claims when lean.space is set	L05
L4	L3, and the refinement theorem for the Rust implementation is proved and fresh	L08

For a data structure, "correctness" is the set of law theorems of its abstract type plus the invariant preservation of each operation (7.9). For a theorem node (the sorting lower bound, max-flow min-cut), L2 means the theorem is proved, and L3 does not apply. For a problem node, L1 means the spec exists and is reviewed.

7.9 Abstract types and data structures

An abstract type is a Lean structure of operations plus a structure of laws, stated against a mathematical model of the state.

namespace Algo.DataStructures

/-- The priority queue as an abstract type over keys of a linear order.
    The model of a queue is the multiset of its keys. -/
structure PriorityQueue (α : Type) [LinearOrder α] (Q : Type) where
  empty      : Q
  insert     : Q → α → TimeM Q
  findMin    : Q → TimeM (Option α)
  deleteMin  : Q → TimeM (Option α × Q)
  model      : Q → Multiset α

structure PriorityQueue.Lawful {α Q} [LinearOrder α] (P : PriorityQueue α Q)
    (Inv : Q → Prop) : Prop where
  inv_empty   : Inv P.empty
  model_empty : P.model P.empty = 0
  inv_insert  : ∀ q a, Inv q → Inv (P.insert q a).ret
  model_insert : ∀ q a, Inv q → P.model (P.insert q a).ret = a ::ₘ P.model q
  findMin_spec : ∀ q, Inv q → (P.findMin q).ret = (P.model q).min?   -- the least key, or none
  deleteMin_spec : ∀ q, Inv q → …                                     -- removes one copy of the least key

A data structure gives an instance and proves Lawful with its invariant (IsHeap for a binary heap, the rank invariant for a disjoint-set forest). The cost theorems are per operation: insert_time_le : (insert q a).time ≤ Nat.log 2 (size q) + 1.

Algorithms that use an abstract type take it as a parameter with its laws. Dijkstra's model takes any lawful priority queue with decreaseKey, and its cost theorem takes the costs of the operations as parameters. The page then states the instance bounds: with a binary heap, with a Fibonacci heap.

Union–find is the hardest standard case: the inverse-Ackermann bound. CSLib and the literature (the Isabelle proof of Charguéraud and Pottier) show it can be done. It is a target of M3, not M1.

7.10 Worked example: merge sort

The spec, in the problem module:

namespace Algo.Sorting

/-- `out` is a sorted rearrangement of `xs`. This is the Definition of the
    sorting problem page: the output has the same elements, with the same
    multiplicities, in non-decreasing order. -/
def IsSort {α : Type} [LinearOrder α] (xs out : List α) : Prop :=
  out.Sorted (· ≤ ·) ∧ out.Perm xs

instance [LinearOrder α] [DecidableEq α] (xs out : List α) : Decidable (IsSort xs out) := …

The model, following the main pseudocode block of 06.4 (written on lists, which is how Lean is idiomatic; the page says so):

open Algo.Cost

/-- Merge two lists, one tick per comparison of keys (pseudocode L9). -/
def merge [LinearOrder α] : List α → List α → TimeM (List α)
  | [], ys => pure ys
  | xs, [] => pure xs
  | x :: xs, y :: ys => do
      tick                                   -- L9
      if x ≤ y then
        let r ← merge xs (y :: ys)
        pure (x :: r)                        -- L10
      else
        let r ← merge (x :: xs) ys
        pure (y :: r)                        -- L11
termination_by xs ys => xs.length + ys.length

/-- Merge sort (pseudocode L1–L5). -/
def mergeSort [LinearOrder α] (xs : List α) : TimeM (List α) :=
  if h : xs.length < 2 then pure xs          -- L1
  else do
    let half := xs.length / 2                -- L2
    let l ← mergeSort (xs.take half)         -- L3
    let r ← mergeSort (xs.drop half)         -- L4
    merge l r                                -- L5
termination_by xs.length
decreasing_by all_goals simp_wf; omega

The theorems:

/-- Merge sort sorts: its output is a sorted permutation of its input. -/
theorem mergeSort_isSort [LinearOrder α] (xs : List α) :
    IsSort xs (mergeSort xs).ret := by
  -- strong induction on xs.length, with merge_sorted and merge_perm;
  -- the same steps as proofs/induction.md

/-- Merge sort is stable. (property.stable) -/
theorem mergeSort_stable … : …

/-- At most n⌈lg n⌉ comparisons. (comparisons.worst, upper side) -/
theorem mergeSort_time_le [LinearOrder α] (xs : List α) :
    (mergeSort xs).time ≤ xs.length * Nat.clog 2 xs.length := by
  -- merge_time_le: (merge l r).time ≤ l.length + r.length,
  -- then the recurrence T(n) ≤ T(⌈n/2⌉) + T(⌊n/2⌋) + n, solved by induction

/-- The class lemma that links the bound to "Θ(n log n)" in the front matter. -/
theorem mergeSort_bound_isBigO :
    (fun n : ℕ => (n * Nat.clog 2 n : ℝ)) =O[Filter.atTop] (fun n => n * Real.log n) := …

/-- Reversed lists need at least ⌊n/2⌋⌊lg n⌋ comparisons. (the lower side of Θ) -/
theorem mergeSort_time_ge : TimeLowerBound mergeSort List.length (fun n => n / 2 * Nat.log 2 n) := …

The front matter binds these with lean.correct, lean.cost and, for the exact count of the front matter ($n\lceil\lg n\rceil - 2^{\lceil\lg n\rceil} + 1$), a separate theorem mergeSort_time_le_exact when it is proved. Until then the exact count is H2 only and the page says which bound Lean proves.

When CSLib has the same model, the module proves mergeSort_eq_cslib : mergeSort xs = Cslib.Algorithms.MergeSort.mergeSort xs and reuses its theorems. The front matter names it in lean.cslib.

The spec proofs in this document are outlines. The real module has the full proofs.

7.11 Sketch: Dijkstra's algorithm

• Prelude. Algo.Prelude.WDigraph: a finite vertex type Fin n, an adjacency function to lists of (Fin n × ℕ). Weights are natural numbers, so the non-negative hypothesis is part of the type. A path is a list of edges, pathWeight, and the distance dist G s v : WithTop ℕ is the infimum over paths (Mathlib's WithTop, with ⊤ for unreachable).
• Spec. IsSSSP G s d : Prop := ∀ v, d v = dist G s v, in Algo.Graphs.ShortestPaths.SSSP.
• Model. dijkstra (P : PriorityQueue …) (G) (s) : TimeM (Fin n → WithTop ℕ), a loop over at most n extractions, written with well-founded recursion on the number of unsettled vertices. Ticks: one per relaxation (pseudocode L8), plus the ticks of each queue operation.
• Correctness. The invariant of 06.5 as a Lean predicate Inv S d, proved to hold initially, to be kept by each extraction (the step that uses ℕ weights), and to give IsSSSP when S is all vertices.
• Cost. time ≤ n * cExtract + m * (1 + cDecrease) + n * cInsert, with the costs as parameters, then the binary-heap instance gives $O((n + m)\log n)$.
• Plan. M2: correctness with a simple list-based queue (O(n²) model). M3: the generic queue and the binary-heap bound.

7.12 AlgoExtract

AlgoExtract is a small Lean program, like math2's M2Extract. algo lean extract runs it after lake build. For each declaration that a node names, it writes one JSON line to build/lean/decls.jsonl:

Field	Meaning
decl	the full name
kind	def, theorem, structure, instance
type	the pretty-printed type
type_hash	BLAKE3 of the elaborated type (the hash that reviews bind to)
axioms	the axioms the declaration depends on (rule L03)
deps	the Algo and CSLib declarations it uses (for the graph of formal dependencies)
sorry	true if any dependency uses sorryAx
computable	true if the compiler can run it (rule L07)
doc	the docstring
pos	the file and the line range (for links and rendering)
deprecated	the Mathlib or CSLib deprecation, if any

The status package reads this file to compute L. Rule L01 checks that each name of the front matter is in it with the expected kind. Rule L02 checks that the type of lean.correct mentions the spec of lean.spec and the model of lean.model, so that a theorem about something else cannot be bound by mistake.

7.13 Executable models and the oracle

Each problem names one oracle in contract.yaml (09.5): a model of an L2 algorithm that solves it, for example Algo.Sorting.mergeSort for sorting. algo lean oracle builds AlgoOracle, one Lean executable named algo-oracle (08.10) with a main that reads JSON cases for a problem on stdin and writes the model's output, using Lean.Json. The JSON types follow the type map of the contract (09.1). The decoding and encoding code is generated by algo gen oracle, so a model needs no hand-written IO.

Because the model is proved correct, a disagreement between an implementation and the oracle means the implementation is wrong, the contract's type map is wrong, or the compiler is wrong. The last is very rare, and the differential runner then re-checks with the checker of 09.3, which does not use the oracle.

The oracle is compiled code. It is trusted for testing, not for proofs, which is why native_decide stays banned (7.5).

7.14 Who writes the proofs

Anyone: a person, an agent of document 12, or an outside AI prover. The kernel is the judge. The rules:

• The prover role (12.2) runs in a sandbox with the pinned toolchain and a Lean REPL. It may call external provers whose terms are recorded in the run record.
• A proof is accepted if it builds, passes L03, and is not slower than 60 seconds per module on the CI runner (rule L10, to keep the build fast). A slow proof is refactored before merge.
• A proof that an agent wrote is labelled in the provenance log (04.7), like any other file. Proofs are not reviewed for truth, since the kernel checks them. Statements are reviewed (7.7).
• Style follows Mathlib's: short tactic blocks, named have steps that match the human proof, no set_option maxHeartbeats above 400000 without a comment.

7.15 Upstreaming

The aim is that the general parts of Algo end up in CSLib and Mathlib, as math2 does with Mathlib.

• A spec, a model or a lemma with no project-specific choice is a candidate. algo lean upstream lists them: declarations that 3 or more modules use, and whole modules for core algorithms that CSLib lacks.
• An upstreamed declaration becomes a thin alias in Algo, with lean.cslib in the front matter, and the module proves equality with the upstream model (7.10).
• Licences match: Algo is Apache-2.0, as are Mathlib and CSLib (17.1).
• The project follows CSLib's review process and naming. A pull request to CSLib carries no AI-written code that its authors have not read, in line with CSLib's and Mathlib's policies on AI contributions (01.4).

7.16 Rendering on the site

• The Formal proof section of a page (06.3) shows, for each bound declaration: the docstring, the statement as rendered Lean with syntax colours, the level, the axioms, and a link to the source line on GitHub.
• The module page /<slug>/lean/ shows the whole module with hover information (types and docstrings of each name), rendered at build time. The default renderer is Verso's highlighted Lean output, which Lean's own documentation uses. A fallback renders plain highlighted source from AlgoExtract positions. Document 20 records the choice.
• Each tick comment with a line id links to the pseudocode line, and the pseudocode line shows a small "Lean" mark when a tick points at it.
• The page never shows a Lean proof as a replacement for the human one. The human proof comes first.

7.17 The monthly bump

Like math2, a weekly job algo bump tries the newest Mathlib release and a matching CSLib commit, and opens a pull request with the report in reports/bump/ when the build passes. The monthly release takes the last green bump. The report lists:

• modules that broke, and the fixing commits;
• declarations that changed type_hash, which voids their fidelity reviews (7.7) and lists the nodes to re-review;
• new CSLib declarations that match Algo declarations (upstreaming done, 7.15);
• the Aeneas version skew for lean-aeneas (7.6).

7.18 Rules this document adds

Listed in 13.3 with their severities.

Rule	Checks
L01	each Lean name in the front matter exists in build/lean/decls.jsonl with the expected kind
L02	the correctness theorem mentions the bound spec and model
L03	cited theorems use only propext, Classical.choice, Quot.sound; no sorryAx, ofReduceBool, package axioms or implemented_by
L04	the fidelity review of a core node is current for all its hashes
L05	at L3, each time and count claim has an explicit bound and a class lemma matching the front matter
L06	the spec accepts the expected outputs of the cases and rejects the mutated ones; it is not vacuous
L07	the model is total (no partial) and computable (no noncomputable)
L08	at L4, the refinement theorem is proved against a fresh extraction of the current Rust file
L09	the module path mirrors the node path
L10	each module builds in at most 60 seconds on the CI runner

Source of this page