LeanExe uses five tools for source-driven proof, exact-artifact proof, empirical semantic comparison, and release evidence. The source artifact tool compiles one registered Lean entry and generates the Talos model of its current WASM output, while the source proof tool repeats that generation before checking the handwritten specification. The exact-artifact tool starts from a frozen binary package, the conformance tool runs a pinned official WebAssembly corpus slice through Talos and Wasmtime, and the release tool binds their results to one repository identity.
The compiler remains outside both proofs' trusted base. The source-driven gate checks the Talos model decoded from generated WAT, while the exact-artifact theorem checks the Talos translation of a validated module decoded from embedded binary bytes. A distributed binary receives the artifact theorem only when its complete byte sequence equals the frozen package and Lean's embedded value.
| Stage | Explicit inputs | Other inputs used by the stage | Outputs | Human work |
|---|---|---|---|---|
| Write and test the program | A Lean source module and exported entry definition. | The accepted source subset, public ABI, compiler semantics, and ordinary test infrastructure. | Tracked Lean source and tests; checked declarations under the ignored root .lake tree. |
Choose the computation, types, error behavior, and test cases. |
talos-artifact.js prepare |
A case name and its entry in proofs/talos/cases.json. |
The root compiler's pinned Lean version, the proof workspace's separately pinned Lean version, lean-wasm, wasm-tools 1.251.0, the pinned Talos revision, and either the standard systemd resource policy or explicitly authorized local runner mode. |
Ignored WASM and WAT under proofs/talos/.generated/<case>/; a tracked lean/Project/<Case>/Program.lean proof cache. |
Inspect any changed instruction stream and decide what property warrants proof. |
| Develop the specification | The source meaning, generated Program.lean, generated WAT, and the intended claim. |
Talos semantics, the shared runtime theorems, representation predicates, arithmetic lemmas, and examples from completed cases. | Tracked Spec.lean and any tracked helper proof modules under lean/Project/<Case>/. |
State adequate preconditions and postconditions, then construct the proof. |
talos-proof.js check |
A case name or --all, the registry, current source, and handwritten proof modules. |
Every artifact-stage dependency, the proof Lake project, its pinned manifest, runtime pins, and aggregate imports. | Ignored generated files and Lake outputs; a zero exit status only after the selected theorem builds. | Interpret a failure and change source, specification, or proof according to its cause. |
artifact-proof.js check |
An exact program.wasm path and registered artifact proof target. |
The content-addressed package, strict manifest and registry, embedded bytes, binary verifier, Talos semantics, and behavioral proof modules. | Lake outputs; a zero exit status only after identity, formal artifact, behavior, and manifest-declaration checks pass. | Review the manifest, trusted revisions, host assumptions, and behavioral statement. |
artifact-conformance.js check |
The pinned conformance configuration and exact official .wast files and command lines. |
Pinned CodeLib and testsuite revisions, wasm-tools 1.251.0, Talos, and Wasmtime 44.0.0 with the recorded feature settings. |
Exact decoder or validator classifications, per-file Talos counts, and Wasmtime outcomes; a zero exit status only when every configured result matches. | Review invalid-module classifications, coverage labels, skipped command kinds, and every semantic discrepancy. |
The source artifact stage creates a fresh uniquely named tmp/leanexe-talos-* directory and places Talos's required rust/<case>/Cargo.toml and rust/build/<case>/ layout below it. It removes only that same task-owned staging directory after Talos emits Program.lean; pre-existing tmp/ entries are not cleanup targets, and a failure to remove the new staging directory makes the command fail. The requested ignored WASM and WAT outputs and the tracked Lean model remain persistent proof inputs after a successful prepare operation.
The persistent source-driven case consists of the source program, its tests, one registry entry, runtime pins, an aggregate import after completion, the generated Program.lean cache, and handwritten proof modules. A case may divide its proof among many files, with Spec.lean importing the final theorem. Either source-driven tool can regenerate the cache, and a byte change marks a changed proof subject that must pass its source-driven behavioral gate and, when the case is also registered as a frozen package, the exact-artifact equality and behavioral gates. The source registry has thirty-nine complete cases, and the proof tree tracks thirty-nine corresponding Program.lean caches; thirty-four currently have registered exact-artifact packages. The sixth restricted binary64 registration is the completed fixed Euler step. Project.EulerRusanovStep.Spec registers exact execution as sodQuarterStepCheckedBits_exact and the decoded-real certificate as sodQuarterStepCheckedBits_wat_real: all six numeric payload words are finite; the exact decoded left and right cells are [207/256, 9/80 - ε/20, 257/128] and [81/256, 9/80 + 3ε/40, 95/128] for ε = 2^-52; both are admissible; their signed errors are [0, -3ε/64, -7ε/512] and [0, 5ε/64, -25ε/512]; and the physical balance residual is [0, ε/32, -ε/16], not zero. This remains a fixed-case theorem rather than an input-generic solver theorem, and its separate exact-byte theorem and verified-data package are complete.
All four tools call tools/leanrun for every Lake, Lean, lean-wasm, and Talos verifier process. In standard mode each child receives MemoryHigh=4G, MemoryMax=6G, MemorySwapMax=1G, CPUQuota=100%, nice -n 10, ionice -c 3, LEAN_NUM_THREADS=1, and a stage-specific timeout. The runner shares the same-user ../vq lock, and the tools stop when they cannot acquire that lock or create the required user scope.
In a container without a systemd user scope, an explicit user-authorized
LEANRUN_LOCAL=1 on one of these tools keeps every child local and retains the
pinned toolchain, shared lock, stage timeout, LEAN_NUM_THREADS=1, nice, and
ionice. The runner warns that the cgroup CPU, memory, and swap limits are
not enforced. The mode is never an automatic fallback. Invoke the tool
directly with the variable; do not wrap a runner-calling tool in
tools/leanrun, because its child runners must acquire the lock themselves.
Do not wrap these commands in a second resource scope. The tools create a separate limited scope for each expensive child, and the shared lock queues behind any participating Lean or Lake process. The Node drivers use signal-aware process groups, so SIGINT or SIGTERM reaches the active runner, timeout process, Lake process, and Lean child before the driver exits.
Register the source module and entry in proofs/talos/cases.json. The registry requires a snake-case case name, the checked Lean module, the fully qualified entry, the Pascal-case proof module, the final specification target, and a completion flag. Set complete to false until the case has its intended theorem and belongs in the aggregate proof library.
The optional sourceWorkspace field selects compiler (the default) or
proof. The latter builds the source in proofs/talos/lean and invokes
the root compiler through that workspace's lake env, so extraction can
load its checked declarations and pinned dependencies. The compiler and
source builds run in sequence through tools/leanrun.
{
"name": "fold_sum",
"module": "LeanExe.Examples.ByteArrayPrograms",
"entry": "LeanExe.Examples.ByteArrayPrograms.foldSum",
"leanModule": "FoldSum",
"specTarget": "Project.FoldSum.Spec",
"complete": true
}Generate one case from the repository root. The tool validates the wasm-tools version, builds the compiler and source module, compiles the entry, renders WAT, invokes Talos through temporary Cargo-shaped input, and replaces local outputs only after every stage succeeds. Content-identical outputs retain their timestamps, which prevents needless proof rebuilds.
tools/talos-artifact.js prepare fold_sumThe generated files support inspection and proof development. Read proofs/talos/.generated/fold_sum/program.wat when function indices, control flow, or instruction boundaries require examination, and import Project.FoldSum.Program from handwritten proof modules. Regenerate these files after changing the source, compiler, Talos pin, or wasm-tools pin.
A registration with "annotations": true also generates
program.annotations.json, proof-recipes.json, and the tracked
AnnotationMatches.lean module. Preparation checks the compiler
sidecar against the generated model before producing the Lean
equalities. The proof gate compares both tracked generated modules
with fresh output. The Riemann registration enables this support.
Add the generated module import and four runtime equalities to Project/Runtime/Checks.lean. The runtime function indices follow the user functions in the generated module, and release takes its own index because its body calls itself recursively. A failed rfl identifies a generated runtime change that the shared runtime library must address.
example : Project.FoldSum.func1Def = allocFuncDef := rfl
example : Project.FoldSum.func2Def = resetFuncDef := rfl
example : Project.FoldSum.func3Def = retainFuncDef := rfl
example : Project.FoldSum.func4Def = releaseFuncDef 4 := rflState the primary theorem over meaningful inputs and relate the WASM result to the source computation. Include memory layout, address and page bounds, ownership, allocator state, counters, and frame conditions wherever the generated program depends on them. A fixed example can test the proof machinery but does not establish an input-generic program theorem.
The proof normally enters through TerminatesWith.of_wp_entry_for, changes to a wp goal over the generated function body, and composes bounded instruction regions. Project/Common.lean supplies address and read-over-write tools, while Project/Runtime supplies generic allocator, retain, release, free-list, and recursive teardown results. Artifact Proving explains the shared ProofKit, annotation, LTG, journal, and independent-checking boundaries, while Artifact-Proof Strategies records general construction guidance.
Divide a generated function at calls, loops, branches, allocations, copy loops, final stores, and result construction. Give each region an explicit instruction list or a small definitionally equal extraction, and state its semantic postcondition before proving the generated adapter. A target that reaches its timeout without a diagnostic requires a smaller theorem or a reusable semantic lemma before another build.
The focused gate regenerates the artifact and model before building the registered specification target. It reports Lean warnings but fails on compilation, model generation, runtime-pin, or proof errors. An incomplete case can use the same command, although its successful build does not count it among the completed proofs.
tools/talos-proof.js check fold_sumAfter the theorem is complete, set complete to true and import Project.<Case>.Spec from Project.lean. The aggregate gate verifies that completed registry entries match the specification imports and that every registered case appears in the runtime checks. It then regenerates all registered cases serially and builds the complete Project target; the 2026-08-26 run passed all twenty cases.
Those older aggregate results are historical: twenty cases passed on 2026-08-26 and twenty-six on 2026-09-04. The current gate regenerates thirty-nine cases and builds the thirty-nine completed specifications. On 2026-09-07 the then-current 29 models regenerated successfully, but the build reached its 20-minute limit while compiling existing CLOB dependencies without a theorem diagnostic; smaller missing targets must complete before a retry.
tools/talos-proof.js check --allThe final gate can fail because the source no longer compiles, wasm-tools has the wrong version, Talos rejects the WAT, the generated model differs from the tracked cache, the cached model does not compile, a runtime definition changed, a handwritten theorem no longer matches the current instruction stream, or the registry and aggregate imports disagree. It also fails when a child exceeds its timeout, the standard-mode cgroup manager rejects a required limit, a generated ignored output cannot be replaced, or a temporary directory cannot be removed. These failures preserve the stage name and child status so the next investigation starts at the first failed boundary.
An exact-artifact package has the path proofs/artifacts/<case>/<sha256>/ and contains program.wasm and manifest.json. The separate artifact registry maps its case, digest, manifest, and proof target, while Project.<Case>.ArtifactBytes embeds the complete byte sequence in Lean. Schema three names the embedded bytes, decoded raw module, cached execution module, closed module-equality theorem, and concrete source behavioral theorems, while recording both Lean pins, the Talos revision, the normative verifier-source digest, and host assumptions.
Check an external binary by passing its path and the registered artifact target. The command rejects an unregistered target, a manifest mismatch, a changed digest or length, any byte difference from the immutable package, or any difference from Lean's embedded byte value. It then builds the exact artifact theorem and behavioral specification, checks the expected theorem types, and rejects sorryAx or an axiom outside the standard logical axioms and generated decision-certificate families recorded by the artifact format.
tools/artifact-proof.js check \
proofs/artifacts/fold_sum/b599860eb8fe3937148455c27c8cfca5473f967001e563530b4790c43017e3b5/program.wasm \
Project.FoldSum.ArtifactTranslationcheck-artifacts performs the identity, embedded-byte, and exact-artifact theorem stages for all thirty-four packages. check-all adds every behavioral specification and the aggregate manifest-declaration check. Neither aggregate mode invokes LeanExe, reads a source program, or invokes wasm-tools. The 2026-09-04 twenty-one-package receipt belongs to its recorded earlier input; the retained 21-package release draft records digest dfad5b82317c9ca0a67e6692ecb872457e6d6406cd9d6bad90e1333a29c1ec11 and its aggregate receipt is pending. The accepted 2026-08-26 receipt covers the twenty packages registered at that time.
The conformance configuration pins the CodeLib and official WebAssembly testsuite revisions, Wasmtime version and feature options, twenty-five exact execution files with coverage labels, and fifteen invalid-module commands identified by file, assertion kind, and source line. The command verifies those revisions and executable versions, builds the pinned Talos testsuite executable and the artifact classifier, and runs each operation serially. A temporary one-file corpus selects each execution filename exactly, avoiding the Talos harness's substring matching.
tools/artifact-conformance.js checkThe invalid-module stage extracts each configured official module and requires the exact decoder or validator error constructor recorded in the configuration. wasm-tools adds custom name sections when encoding text-origin assert_invalid modules, so the command strips custom sections from those cases before classification. It preserves raw assert_malformed binary modules byte-for-byte, and the 2026-08-26 run matched all fifteen classifications, including truncation, version, section, integer-width, alignment, stack, and memory-limit failures.
Talos executes supported assertions and reports unsupported command kinds as skips, so the invalid-module stage supplies separate evidence for the artifact decoder and validator. The 2026-08-26 execution run produced 3,853 passes, six known assertion failures, 627 skips, and no cascades, decoder errors, interpreter errors, or fuel exhaustion in Talos, while Wasmtime passed all twenty-five files with function-references=y. The command warns only when the failures exactly match the six imported-memory rows recorded for memory_grow.wast; an upstream repair removes the warning, while any changed or additional failure stops the gate.
The release file binds the artifact registry hash, every package-manifest hash, exact theorem names, verifier and release-input digests, tool pins, and machine-produced gate receipts. The release-input digest includes every project proof source, tracked Talos execution cache, recursive local LeanExe import, Lake definition, selected binary, manifest, pin, and verification driver used by the two gates. Its status follows the immutable source revision, accepted kernel disposition, matching aggregate and conformance receipts, and a successful cold-checkout receipt; removing a blocker string without satisfying its corresponding field makes validation fail.
tools/artifact-release.js inspect
tools/artifact-release.js refresh
tools/artifact-release.js check-ready
tools/artifact-release.js check-cold <revision>inspect validates the draft without claiming release readiness, while refresh reconstructs package records and consumes matching receipts from build/evidence. check-ready returns a failure until every derived condition holds. check-cold compares the current and cloned release inputs before setup, checks the exact Lean and dependency revisions, rejects tracked mutations after setup or either gate, reruns both gates, and writes the cold receipt before removing its temporary checkout. The current draft binds twenty-one packages under Lean 4.34.0-rc2 and Talos 87e3aa5e8f6e6f3b3eb5e7e4c5aba43071002d47; matching aggregate-artifact, semantic-conformance, source-revision, and cold-checkout evidence are pending. The accepted 2026-08-26 receipts bind only their earlier twenty-package input digest.
Commit the source module, tests, cases.json, runtime pins, Project.lean import after completion, generated Program.lean proof cache, Spec.lean, and every handwritten helper it imports. An exact-artifact migration also commits the content-addressed binary and manifest, artifact registry entry, embedded bytes, decoded caches, and exact translation theorem modules. A conformance change commits proofs/talos/conformance.json, the driver or parser tests it changes, and documentation of the pinned revisions and observed result. Every proof change also records the theorem's scope, host assumptions, and new reusable results.
Never edit Program.lean by hand, and never recreate a persistent proofs/talos/rust tree. Run the artifact tool when the model needs to change, review the tracked cache diff, then repair the handwritten theorem against the new instruction stream. Record focused and aggregate gate results in devnotes.md without treating an old object file as current evidence.