Martin Kleppmann (author of Designing Data-Intensive Applications) argues that AI will bring formal verification into the software engineering mainstream. His thesis: LLMs are getting good at writing proof scripts, which could dramatically reduce the cost of formal verification—historically prohibitive (the seL4 microkernel required 20 person-years and 200,000 lines of Isabelle for 8,700 lines of C).

Key formal verification languages include Lean, Coq/Rocq, Isabelle, Agda, F*, and Dafny. Currently, these are niche tools used primarily in academia and specialized industrial applications (cryptographic protocol stacks, verified compilers, microkernels).

This market tests whether AI-driven improvements will translate to widespread adoption within ~5 years.

Resolution Criteria:

Resolves YES if any programming language whose primary purpose is formal verification or proof assistance reaches the TIOBE Index Top 10 at any point before January 1, 2031.

Qualifying languages (non-exhaustive):

• Lean

• Coq/Rocq

• Isabelle

• Agda

• F*

• Dafny

• Idris (if used primarily for verification)

Resolves NO if no such language reaches Top 10 by January 1, 2031.

Edge cases:

• If TIOBE changes methodology significantly, I will use reasonable judgment to interpret the spirit of the criterion

• If a mainstream language (Python, Rust, etc.) adds formal verification as a feature, this does NOT count unless it becomes standard practice for that language

• I will use the official TIOBE monthly rankings as published on tiobe.com