Prediction: Theorem Provers Will Completely Dominate Programming (And Soon)

Is it time to say goodbye to standard programming languages?

At Scidonia, we recently made a bold prediction: Theorem provers are going to completely dominate the programming language space, and it’s going to happen very quickly.

If you think of theorem provers like Rocq (formerly Coq) or Lean as esoteric, academic tools meant only for mathematical proofs, it's time to update your mental model. The shift is already happening, driven by two undeniable forces: Correctness and Speed.

Here is why conventional languages are on borrowed time, and why the future belongs to Formal Verification and a paradigm we call Vericoding.

1. Correctness: Achieving Perfect Security (Without the Crippling Cost)

Historically, formal verification was too expensive, slow, and niche for everyday software. It took two person-years to write the seL4 operating system kernel, but twenty person-years to formally verify it.

But as it turns out empirically, a theorem prover like Rocq or Lean provides a functional programming language that is nearly as convenient for frontier AI models (LLMs) to use as anything else. LLMs are changing the math on formal verification. You don’t have to write elaborate theories, prove complex properties, or use wicked dependent types yourself. The AI can do the heavy lifting.

Anthropic recently proved this by using Claude to formally verify security properties at the assembly code level (RISC-V) across over 100 real-world open-source software libraries, generating roughly 180 million lines of Rocq proof code. While doing so, the AI discovered bugs that had eluded detection for years, despite trillions of test runs.

The main hurdle has always been the lack of ecosystem libraries—but with AI, that gap is closing at an astonishing rate.

Case in point: We recently had a substantial fragment of libexpat written in Lean in just 2 days. The cost? Under $100.

When you want to guarantee a property holds—like ensuring a program will never crash or trigger a memory-safety error—you can just pay an LLM to prove it for you, and the cost is amazingly low. While there are caveats (unprovable conjectures, AI misinterpretations), if you have a well-specified problem like parsing XML or using a network stack protocol, achieving a formally verified codebase is becoming trivial.

2. Speed: The Ultimate Trump Card

The last and most amazing factor in this shift is performance. Soon, the fastest program in every single domain will be one written in a theorem prover. We're absolutely serious.

If you can specify the behaviour, either with an example program, a specification, or both, you can use numerous techniques to arrive at a semantics-preserving program that is vastly faster. It’s like super-compilation on steroids, and it can be pushed all the way down to the metal.

We call this Vericoding: AI-guided certified program refinement. The artifact you edit is the specification. An AI proposes a faster program, and a theorem prover certifies that the new program refines the old one with the exact same behaviour, for every valid input.

The Proof is in the Data

We’ve run the experiments to back this up. Here is what we are already seeing in the wild:

• LeanIn Beating Node.js: LeanIn is a concurrency runtime for Lean 4 where async code compiles to a state machine, and the model is machine-checked. On a pipelined HTTP benchmark, it reaches 3.05× the speed of Node 22.
• Parsebot (267.9 MB/s Zero-Copy Parsing): A grammar in Rocq yields a certified JSON parser extracted to OCaml. Through vericoding, a zero-copy refinement of that parser reaches 267.9 MB/s on the gsoc-2018.json dataset, and it is mathematically proved to be equivalent to the original.
• SpecAMQP: We created an open Lean specification of AMQP 1.0: one shared description that implementations can follow and prove they comply with. The reference implementation is actively growing into a server that is correct by construction.
• VeLLVM & SIMD: We’ve already performed examples of this with VeLLVM using SIMD enhancements, and the results are frankly insane.

The Death of Conventional Languages? 💀

Previously, we argued there was no excuse for using a conventional language without dependent types. We think this needs to be strengthened: these languages will die.

Even if you continue to use lower-level languages for performance reasons, you will be developing with them inside a theorem prover. Why? Because it will be the only way to get formal proofs of semantic equivalence for your faster programs. (And honestly, in this new world, we can't think of a good reason to keep using Python or JavaScript at all).

We are moving from a world of sampling a few test cases, hoping our fuzz tests catch the worst of it, to a world where a theorem prover checks the rule for every valid state. The standard defences against bugs are no longer sufficient; we need ways to mathematically prove that code is correct.

Verified software is now available at the cost of a test run.

Are you ready for the shift? Let us know what you think in the comments, and check out the deep dives into our experiments at scidonia.ai/vericoding.