The Stack
Twelve worked examples. Same seven axes. Each artifact’s coordinate is the tuple of its measured values. Position predicts behavior — what produced the step, what oracle checked it, what cache it drew from, what it cost in joules.
c = ⟨ S, V, E, D, C, R, τ ⟩
KERNEL AUTOMATION · CPU
A goal in Presburger arithmetic — sums, differences, linear inequalities over integers — closes in a single tactic line. CPU-bound, sub-millisecond, no GPU. Most subgoals in real proofs look like this and never need anything more.
KERNEL AUTOMATION · PREMISE SEARCH
Best-first proof search bounded by depth, drawing premises from Mathlib. Discharges a wide class of routine algebraic and order-theoretic goals. The lemma-warm cache regime makes this the workhorse tier of any real proof effort.
DECISION PROCEDURE · SMT
A goal over bit-vectors of fixed width — typical in cryptographic and hardware verification — falls inside the decidable envelope. The SMT solver returns a proof certificate; the kernel re-checks. Polynomial-to-exponential CPU cost; no GPU.
BOUNDED MODEL CHECK · CBMC
A Rust function annotated with proof harnesses (preconditions, post-conditions) is checked by Kani via CBMC for bounded depth. Catches panics, overflow, and assertion violations within the bound. Not full functional correctness, but cheap and a real guarantee where it applies.
TYPE SYSTEM · COMPILE-TIME
Memory safety and data-race freedom for the whole program, proven at compile time by the type system. The "solver" is the type checker, the proof is the type derivation, the artifact is the compiled binary. Distilled into the language itself; no per-program search cost.
SMALL MODEL · CONSTRAINED DECODE
A 1–7B in-domain model proposes tactics under grammar constraints; the kernel applies and checks. Stochastic-bounded (pass@k > 1). The order-of-magnitude inflection over decision procedures starts here, but so does the energy bill.
OPEN-WEIGHT · TREE SEARCH
DeepSeek-Prover, Goedel-Prover, Kimina, Numina-Lean-Agent, Leanstral and similar open-weight provers, used as the search backend. Whole-proof draft with kernel-fed feedback. Indexed into a cross-project proof DB; verifiable, replicable across runs at fixed seed.
HYBRID · MCTS + LEAN
AlphaZero-style reinforcement learning with the Lean kernel as the reward oracle. Reported as several hundred TPU-days per Olympiad-class problem in 2024; cost has since fallen roughly an order of magnitude. The current upper bound on autonomous search energy.
INTERACTIVE PROOF · COQ
CompCert's correctness proof in Coq, library-integrated and re-checked on every release. The amortization is total: the proof was written once, the artifact ships with every certified compilation. Used in safety-critical avionics.
INTERACTIVE PROOF · ISABELLE/HOL
Functional correctness, security, and refinement proofs for a complete OS microkernel in Isabelle/HOL. Roughly twenty person-years for under ten thousand lines of C — the canonical example of why automation matters, and why the joules question is downstream of the proof-labor question.
INTERACTIVE PROOF · F⋆
Verified cryptographic primitives in F⋆, library-integrated into Firefox, the Linux kernel, and other production systems. The deepest demonstration that "the spec exists" is the binding constraint — for crypto it does, and the verified artifact ships.
LIBRARY INTEGRATION · MATHLIB
A useful lemma surfaced during one project's proof attempt, refactored and promoted into Mathlib. From that point forward every Lean user can call it via premise selection; the energy paid to produce it amortizes across every future cold proof in the ecosystem.
Two artifacts with nothing in common can sit at adjacent coordinates — a Z3 bit-vector discharge and a Kani Rust check share most of their tuple. Two with the same name (different solver tiers) sit twelve orders apart on E. The stack is what the difference looks like.
Continue