---
title: Formal Verification
category: concepts
created: 2026-12-21
updated: 2025-01-05
tags: [formal-verification, lean-proofs, verified-ai, mathematical-reasoning, axiom-math, proof-generation, type-checking, model-checking, smt-solvers, refinement-types, reinforcement-learning, hardware-verification, ai-for-science]
sources: [raw/feeds/2026-06-11--scaling-past-informal-ai-carina-hong-axiom-math.md]
confidence: high
---
# Formal Verification
Mathematical technique for proving the correctness of systems using rigorous logical methods. In AI contexts, particularly advocated by axiom-math as essential for achieving AGI through "Verified AI" approaches.
## Core Concepts
To a first approximation, formal verification means using type checkers (like for TypeScript, C++ or Rust, but more capable) to verify mathematical proofs meticulously specified in a language like **Lean**. Translating an "informal" proof into a Lean proof is hard — most theorems remain informal precisely because formalization is so labor-intensive.
## Broader landscape (beyond Lean type-checking)
Formal verification is broader than "type-checking a proof." It also includes:
- **Model checking**: TLA+, SPIN
- **SMT-based tools**: Dafny, F*, Why3
- **Refinement-type systems**: Liquid Haskell
Many of these don't look much like "type checking a proof" from the user's perspective even when there's a similar logical core underneath. Formal verification applies to **software and hardware correctness**, not only pure mathematics. carina-hong highlights **hardware verification as a killer app** (flight control, nuclear power plants, pacemakers) as the software/hardware running them grows more complex.
## Role in AI training and inference
Verification shows up in two places:
- **Training**: A Lean verifier provides a much stronger RL reward signal than statistical methods (GRPO, RLHF) — analogous to compile-and-test on coding RL. See [reinforcement-learning-verification](/concepts/reinforcement-learning-verification).
- **Inference**: Proofs can be checked for correctness cheaply even though they are expensive to generate. See [expensive-to-produce-cheap-to-verify](/concepts/expensive-to-produce-cheap-to-verify).
## Verification as the AI-for-science dividing line
Verification is the key difference between **AI for science** and **AI for computation**: in science you must physically test (verify) your hypothesis through experiment. alex-lupsasca notes that as models generate thousands of candidate proofs, humans become the verification bottleneck — making automated verification increasingly valuable. Lab-in-the-loop systems (Radical AI, Lila) are built around this premise.
## See also
- [verified-ai](/concepts/verified-ai)
- axiom-math
- [specification-problem](/concepts/specification-problem)
- [reinforcement-learning-verification](/concepts/reinforcement-learning-verification)
- [expensive-to-produce-cheap-to-verify](/concepts/expensive-to-produce-cheap-to-verify)
- [proofgen-benchmark](/concepts/proofgen-benchmark)