Formal verification

Agenda paper that defines verified AI from the perspective of formal methods, mathematical techniques for specifying and verifying systems. It sets out five challenges and five corresponding principles.

Defines guaranteed safe AI as a family of approaches that combine a world model, a safety specification and a verifier. The world model describes mathematically how the AI system affects the outside world. The verifier provides an auditable proof certificate that the system meets the specification relative to the world model.

Position paper arguing that artificial general intelligence should be built to provably satisfy human-specified requirements. The authors propose using advanced AI for formal verification and for mechanistic interpretability, the study of a model's internal mechanisms.

Simplex-based SMT technique for neural networks with ReLU activations. It either proves that a network has a given property or finds a counterexample. It was evaluated on networks from a prototype airborne collision-avoidance system (ACAS Xu).

GPU-accelerated neural-network verifier based on linear bound propagation and branch and bound. Its README lists it as the winner of every annual neural-network verification competition (VNN-COMP) from 2021 to 2026.

Report on the 2025 edition of the annual competition that compares neural-network verifiers on shared ONNX and VNN-LIB benchmarks. Eight teams took part.

Open-source programming language and proof assistant, software that checks every step of a proof. It is used for formally verified code and machine-checked mathematics, and is a common target for AI-generated proofs.

Verification-aware programming language whose static verifier checks code against its specifications before it runs. Dafny programs compile to languages such as C#, Java, JavaScript, Go and Python.

Tool for verifying Rust code in which developers write specifications and proofs that automated solvers check for all possible executions.

Benchmark of over 750 Dafny programs that tests whether language models can generate the hints the Dafny verifier needs. At release, the best model and prompt succeeded on 68 percent of them.

Benchmark of 12,504 formal specifications in Dafny, Verus/Rust and Lean for generating formally verified code. Off-the-shelf models succeeded 82, 44 and 27 percent of the time in those three languages, respectively.

Repository-scale benchmark of 43 multi-module Lean 4 tasks, in which an agent must write both the implementation and its proof. Agents may also prove that a specification cannot be satisfied. The strongest agent fully solved 27 tasks.

Program of the UK's Advanced Research and Invention Agency (ARIA), backed by £59m. It is building an open-source toolkit with which AI agents produce formally verified artifacts, and is applying it mainly to cybersecurity.

Describes AlphaProof, an AlphaZero-inspired agent that learns to find formal proofs in Lean through reinforcement learning. It trains on millions of problems that were automatically translated into Lean. At the 2024 International Mathematical Olympiad, it solved three of the five non-geometry problems. Together with AlphaGeometry 2, it reached a silver-medal-equivalent score.

Harmonic's theorem-proving system, which produced formal solutions to five of the six problems of the 2025 International Mathematical Olympiad. It searches over Lean tactics, the commands that build a proof, with Monte Carlo graph search. Its informal reasoning system drafts and formalizes lemmas, and a separate solver handles geometry.

Open-source Lean 4 theorem-proving model. Its cold-start data, used in the first training stage, come from a pipeline in which DeepSeek-V3 decomposes problems into subgoals. Reinforcement learning follows. The 671B-parameter model reaches an 88.9% pass ratio on MiniF2F-test and solves 47 of 658 PutnamBench problems.

Lean theorem-proving model that refines whole proofs using Lean feedback, proved lemmas and self-summarization. It works with the Seed-Geometry engine. The authors report fully proving five of the six 2025 International Mathematical Olympiad problems, one of them after the submission deadline. They also report proving 78.1% of formalized past IMO problems.

Proves a tight ℓ2-norm robustness guarantee for classifiers smoothed with Gaussian noise, which predict by majority vote over noisy copies of an input. For example, it certifies 49% top-1 accuracy on ImageNet under perturbations of ℓ2 norm below 0.5. Because the guarantee is computed by Monte Carlo sampling, it holds only with high probability.

System description of version 2.0 of Marabou, an open-source verifier that checks properties of neural networks. It solves linear and non-linear constraints with an SMT-based procedure. The new version can produce proof certificates for queries that have no solution. It also handles more activation functions and accepts queries through a richer Python API.

AWS announcement that Automated Reasoning checks in Amazon Bedrock Guardrails are generally available. The safeguard uses formal verification techniques to check generative AI outputs against an Automated Reasoning policy. The policy's rules are extracted from a customer's own documents.

Interactive theorem prover and dependently typed programming language, formerly the Coq Proof Assistant. It is used to write formal specifications and machine-checked proofs that programs meet them. It can also extract executable OCaml or Haskell code from specifications.

Generic proof assistant, used mainly as Isabelle/HOL for higher-order logic. It checks formal proofs about mathematics and about the correctness of hardware, software and protocols. Through Sledgehammer, it can call external automated provers. It comes with the Archive of Formal Proofs, a collection of proofs checked in Isabelle.

Book on writing definitions and machine-checked proofs in Lean 4, written with contributions from the Lean community. It covers dependent type theory, propositions and proofs, tactics, inductive types, structures and type classes.