Verification

From Zero to QED
https://sdiehl.github.io/zero-to-qed/

Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
https://arxiv.org/abs/2609.15648v1

Formalization that keeps the mathematician in the loop
https://vida-nyu.github.io/Lea/

Open Gauss
https://github.com/math-inc/OpenGauss

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
https://github.com/google-deepmind/superhuman/tree/main/leap

The Foundation of Code Verification: The Lax Equivalence Theorem
https://bill-rider.com/2026/05/31/the-foundation-of-code-verification-the-lax-equivalence-theorem/

Formalizing Neural Networks in Lean
https://leandojo.org/torchlean.html

Goedel Code Prover
https://github.com/goedelcodeprover/Goedel-Code-Prover

Benchmarking LLMs on Real-World Software Verification in Lean 4
https://github.com/utopia-group/VeriSoftBench

Engineering Secure and Dependable Software Systems
https://sites.google.com/view/marktoberdorf2026/home

When AI Writes the World’s Software, Who Verifies It?
https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html

Lean 4 Skills for Claude
https://github.com/cameronfreer/lean4-skills

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
https://arxiv.org/abs/2602.02285

From Zero to QED
https://sdiehl.github.io/zero-to-qed/01_introduction.html

BEAVER: An Efficient Deterministic LLM Verifier
https://www.arxiv.org/abs/2512.05439

A Neurosymbolic Approach to Natural Language Formalization and Verification
https://arxiv.org/abs/2511.09008

An Introduction to Formal Verification Methods for Neural Networks
https://www.youtube.com/watch?v=kINfn-ZYiLY