References

The literature anchoring the stack.

Every axis-value, every constant, every cell on the table traces to a published source. Grouped by domain. Open-standards and scholarly literature only.

I · Logic & foundations

The deductive substrate every prover ultimately re-enacts.

  1. Frege, G. (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle.
  2. Russell, B., & Whitehead, A. N. (1910–1913). Principia Mathematica. Cambridge University Press.
  3. Hilbert, D., & Ackermann, W. (1928). Grundzüge der theoretischen Logik. Springer.
  4. Gödel, K. (1929). Über die Vollständigkeit des Logikkalküls. Doctoral thesis, Vienna.
  5. Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik 38.
  6. Church, A. (1936). An unsolvable problem of elementary number theory. American Journal of Mathematics 58.
  7. Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the LMS s2-42.
  8. Curry, H. B., & Feys, R. (1958). Combinatory Logic. North-Holland.
  9. de Bruijn, N. G. (1968). AUTOMATH, a language for mathematics. Technological University of Eindhoven.
  10. Howard, W. A. (1980). The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.

II · Program logic & verification methodology

The bridge from mathematical proof to software correctness.

  1. Floyd, R. W. (1967). Assigning meanings to programs. Proceedings of the AMS Symposium in Applied Mathematics 19.
  2. Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM 12, 576–580.
  3. Dijkstra, E. W. (1976). A Discipline of Programming. Prentice-Hall.
  4. Owicki, S., & Gries, D. (1976). Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM 19.
  5. Lamport, L. (1977). Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering SE-3.
  6. Reynolds, J. C. (2002). Separation logic: a logic for shared mutable data structures. LICS.
  7. O'Hearn, P. W. (2019). Incorrectness logic. POPL.

III · Interactive theorem provers

The systems on which the next four decades of formal verification ran.

  1. Milner, R. (1972). Logic for computable functions: description of a machine implementation. Stanford AIM-169.
  2. Boyer, R. S., & Moore, J S. (1973–1979). A Computational Logic. Academic Press, 1979.
  3. Trybulec, A. (1973). The Mizar system. Studies in Logic, Grammar and Rhetoric.
  4. Gordon, M. J. C., Milner, R., & Wadsworth, C. P. (1979). Edinburgh LCF: A Mechanised Logic of Computation. LNCS 78. Springer.
  5. Coquand, T., & Huet, G. (1988). The Calculus of Constructions. Information and Computation 76.
  6. Paulson, L. C. (1989). The foundation of a generic theorem prover. Journal of Automated Reasoning 5.
  7. Harrison, J. (1996). HOL Light: A tutorial introduction. FMCAD.
  8. Norell, U. (2007). Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers.
  9. de Moura, L., & Ullrich, S. (2021). The Lean 4 theorem prover and programming language. CADE 28.
  10. Mathlib Community (2020). The Lean Mathematical Library. CPP 2020.

IV · SMT & decision procedures

The deterministic oracles every higher tier calls into.

  1. Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. JACM 7.
  2. Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. JACM 12.
  3. Nelson, G., & Oppen, D. C. (1979). Simplification by cooperating decision procedures. ACM TOPLAS 1.
  4. de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. TACAS.
  5. Barbosa, H. et al. (2022). cvc5: A versatile and industrial-strength SMT solver. TACAS.
  6. Kovács, L., & Voronkov, A. (2013). First-order theorem proving and Vampire. CAV.
  7. Barrett, C., & Tinelli, C. (2018). Satisfiability modulo theories. In Handbook of Model Checking. Springer.

V · Verified systems shipped

The existence proofs that specification-level functional correctness is real, even at substantial proof cost.

  1. Leroy, X. (2009). Formal verification of a realistic compiler. Communications of the ACM 52.
  2. Klein, G. et al. (2009). seL4: formal verification of an OS kernel. SOSP.
  3. Appel, A. W. (2011). Verified Software Toolchain. ESOP.
  4. Hales, T. et al. (2017). A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5.
  5. Zinzindohoué, J.-K., Bhargavan, K., Protzenko, J., & Beurdouche, B. (2017). HACL*: a verified modern cryptographic library. CCS.
  6. Erbsen, A., Philipoom, J., Gross, J., Sloan, R., & Chlipala, A. (2019). Simple high-level code for cryptographic arithmetic — with proofs, without compromises. IEEE S&P.
  7. Protzenko, J. et al. (2020). EverCrypt: A fast, verified, cross-platform cryptographic provider. IEEE S&P.

VI · Verification-aware languages & checkers

Languages and tools that make formal properties first-class.

  1. Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.
  2. Leino, K. R. M. (2010). Dafny: An automatic program verifier for functional correctness. LPAR-16.
  3. Swamy, N. et al. (2016). Dependent types and multi-monadic effects in F⋆. POPL.
  4. Jung, R., Jourdan, J.-H., Krebbers, R., & Dreyer, D. (2018). RustBelt: securing the foundations of the Rust programming language. POPL.
  5. Astrauskas, V., Müller, P., Poli, F., & Summers, A. J. (2019). Leveraging Rust types for modular specification and verification. OOPSLA.
  6. Lattuada, A. et al. (2023). Verus: Verifying Rust programs using linear ghost types. OOPSLA.
  7. Vanhattum, A. et al. (2023). Kani: A bit-precise model checker for Rust. ASPLOS demo.
  8. Clarke, E., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs (CBMC). TACAS.

VII · AI for theorem proving — open-weight wave

The recipe — LLM + Lean + verifier-as-reward + autoformalized data + search — as it became commodity at the open-weight layer.

  1. Polu, S., & Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv 2009.03393.
  2. Han, J. M., Rute, J., Wu, Y., Ayers, E. W., & Polu, S. (2022). Proof artifact co-training for theorem proving with language models. ICLR.
  3. Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., & Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv 2202.01344.
  4. Zheng, K., Han, J. M., & Polu, S. (2022). MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR.
  5. Yang, K. et al. (2023). LeanDojo: theorem proving with retrieval-augmented language models. NeurIPS D&B.
  6. Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations (AlphaGeometry). Nature 625.
  7. DeepMind AlphaProof Team (2025). AI achieves silver-medal standard solving International Mathematical Olympiad problems. Nature.
  8. Tsoukalas, G. et al. (2024). PutnamBench: evaluating neural theorem-provers on the Putnam mathematical competition. NeurIPS D&B.
  9. DeepSeek-AI (2024–2025). DeepSeek-Prover-V1, V1.5, V2 technical reports. arXiv preprints.
  10. Lin, X. et al. (2025). Goedel-Prover-V2: scaling formal theorem proving with self-correction. arXiv.
  11. Moonshot AI (2025). Kimina-Prover technical report.
  12. ByteDance Seed (2025). Seed-Prover and BFS-Prover technical reports.
  13. Project Numina (2025). Numina-Lean-Agent — open-source autonomous Lean prover.
  14. Mistral AI (2025). Leanstral: an open-weight Lean prover release.
  15. Glazer, E. et al. (2024). FrontierMath: a benchmark for evaluating advanced mathematical reasoning. arXiv 2411.04872.

VIII · Energy of inference and verification

Empirical measurement of the joules the previous sections actually cost.

  1. Patterson, D. et al. (2021). Carbon emissions and large neural network training. arXiv 2104.10350.
  2. Henderson, P., Hu, J., Romoff, J., Brunskill, E., Jurafsky, D., & Pineau, J. (2020). Towards the systematic reporting of the energy and carbon footprints of machine learning. JMLR 21.
  3. Strubell, E., Ganesh, A., & McCallum, A. (2019). Energy and policy considerations for deep learning in NLP. ACL.
  4. Niu, X. et al. (2026). TokenPowerBench: measuring per-token power consumption across modern LLM serving stacks. AAAI.
  5. NVIDIA. NVIDIA Management Library (NVML) — GPU power telemetry interface.
  6. Intel. Running Average Power Limit (RAPL) — CPU package and core power telemetry.