How LLMs Are Making Formal Software Verification Viable at Scale

Formal verification has long been regarded as software engineering's "aristocratic tool"—it can mathematically prove that a program is free of certain classes of errors, yet it has been difficult to scale due to its high barrier to entry and substantial cost. A discussion on Hacker News raises a judgment worth taking seriously: large language models are making formal software verification feasible at larger scales. This is not to say that LLMs will replace theorem provers, but rather that they may change the cost structure of the entire process.

What Is the Scalability Bottleneck of Formal Verification

The core idea of formal verification is: first describe the behavior of a program or system precisely with a logical specification, then have a theorem prover or model checker prove that the implementation satisfies the specification. Its value is undeniable—in compilers, operating system kernels, cryptographic protocols, aerospace control, and similar scenarios, a hidden integer overflow or state machine vulnerability can have catastrophic consequences.

The problem is that every step in the process is expensive: writing specifications requires experts who understand both the domain and logic, the proving process often requires extensive human guidance (proof engineering), and the cost of maintaining proofs continuously accumulates as code evolves. Years of academic experience suggest that the investment to verify a small core module may far exceed the cost of writing the module itself.

This constitutes the fundamental scalability bottleneck: it is not that provers are not powerful enough, but that the supply of human labor cannot keep up. LLMs happen to be a tool capable of supplying "understanding and generation" capacity at scale, and the point where the two meet is precisely at this bottleneck.

The difference between theorem provers and model checkers: The two types of tools mentioned in this article follow different technical approaches. Theorem provers (such as Coq, Isabelle, Lean) are based on deductive reasoning, require human guidance of proof steps, can handle infinite state spaces, but have low automation and a steep learning curve. Model checkers (such as SPIN, NuSMV) verify properties by exhaustively exploring finite state spaces; they are fully automatic but face the state explosion problem, and are typically suited to protocols and hardware design. Their cost structures differ: the main cost of theorem provers is human labor, while the main cost of model checkers is compute and state space modeling. The gain from LLMs is more pronounced for the former, because its bottleneck is precisely "understanding and generation."

Several Points Where LLMs Enter the Verification Process

Judging from the direction indicated by the discussion, the gain of LLMs for formal verification is not a single point but distributed across multiple stages of the process.

Specification Generation and Formal Translation

The most direct entry point is the conversion from natural language to formal specifications. Engineers write down their intent in natural language, and the LLM translates it into a draft specification in Coq, Isabelle, Lean, or TLA+ style. This step used to depend almost entirely on scarce experts; now the model can first produce a discussable draft, which is then reviewed and corrected by humans.

Positioning differences among Coq, Isabelle, Lean, and TLA+: Although these tools all belong to the formal methods ecosystem, their applicable scenarios differ. Coq and Isabelle are interactive theorem provers based on dependent type theory or higher-order logic, suitable for verifying complex systems such as algorithms, compilers, and operating system kernels, with an extremely high learning barrier. Lean is a newer theorem prover that has risen in the field of mathematical formalization due to the rapid development of the mathlib library. TLA+ is a temporal logic specification language proposed by Lamport, paired with the model checker TLC, specifically for modeling and verifying concurrent and distributed protocols; its syntax is relatively lightweight and its acceptance in industry is relatively high (AWS once used it at scale). LLM performance differs significantly across tools: because TLA+ has concise syntax and abundant examples in training corpora, the quality of specification drafts generated by models is usually higher than for heavy proof assistants such as Coq/Isabelle.

Drafting and Repairing Proof Scripts

Proof engineering is another major pain point. An LLM can suggest the next tactic based on the current proof state, or analyze error messages and attempt repairs when a proof fails. Although proof fragments produced by the model cannot be trusted directly, turning "constructing a proof from scratch" into "reviewing and repairing a proof" has already significantly reduced cognitive burden.

The meaning of tactic and proof engineering: In interactive theorem proving, a tactic is an imperative proof construction command, such as induction n, simpl, auto; a proof script is essentially a combination of a series of tactics. Proof engineering refers to the large amount of manual debugging work required to make a proof pass—adjusting the order of lemmas, adding auxiliary lemmas, modifying induction hypotheses, and so on—and this workload often far exceeds expectations. The value of LLMs at this stage lies in their familiarity with common tactic patterns, their ability to suggest the next step based on the current proof state (goal stack), or to identify problems such as type mismatches and missing premises when a proof fails. But note that proof scripts are extremely sensitive to context; tactics suggested by the model may fail due to implicit parameters or differences in local assumptions, so the "draft—verify—repair" loop still needs to be led by humans.

Discovery of Invariants and Preconditions

Implicit assumptions such as loop invariants, preconditions, and postconditions are the hardest parts to discover in verification. By reading code context and proposing candidate invariants, LLMs can help engineers lock onto the key properties that need to be formalized more quickly.

Why loop invariants are difficult to discover automatically: A loop invariant is an assertion of properties that hold before and after each iteration of a loop, and it is a core difficulty in program verification (such as Hoare logic). It must be strong enough to imply the target property after loop exit, and weak enough to be maintained after execution of the loop body. This "just right" balance has no general constructive algorithm in mathematics—in fact, invariant generation is theoretically undecidable. Traditional methods rely on expert insight or approximate techniques such as abstract interpretation, and often yield only conservative but useless results. The advantage of LLMs is that they can "guess" meaningful candidate invariants from code semantics and common programming patterns, narrowing the search space from infinite to a finite set of discussable options, which are then checked one by one by the prover. This complements traditional static analysis: the latter guarantees soundness but may miss things, while the former provides breadth but requires verification.

Key Limitation: The Trust Boundary Must Not Be Blurred

Clarity is essential here. Content generated by LLMs is candidate material, not evidence. The entire point of formal verification is that the final conclusion is backed by machine-checkable proofs. If unchecked model output is mixed into the process and treated as proven fact, the credibility of the entire verification system will collapse.

Reasonable engineering practice should be: LLMs propose, provers adjudicate, and humans define the problem boundary. The responsibilities of the three must not be confused. Any practice that treats "the model says there is no problem" as a verification conclusion is a misuse of formal methods.

This is also why the word "feasible" in the discussion deserves attention—it points to cost feasibility, not a relaxation of correctness guarantees.

Potential Impact on Engineering Practice

If the above path holds, the most direct changes may occur in scenarios such as: core modules of safety-critical systems, constant-time properties of cryptographic implementations, state machine correctness of concurrent protocols, and semantics preservation of compiler optimizations. What these fields have in common is relatively stable specifications and extremely high cost of errors—precisely where formal verification yields the greatest benefit, and where cost has historically kept it out.

Another possible change is the "routinization" of verification. When the marginal cost of writing specifications and drafting proofs decreases, teams may incorporate lightweight formal checks into the regular development process, rather than conducting only one expensive major review at the end of a project. This shift from "project-level verification" to "continuous verification" may be more structurally significant than an increase in the scale of a single verification effort.

Questions Still to Be Answered

The discussion itself is limited in length and leaves many open questions: To what extent can LLMs handle cross-module dependencies in large codebases? Is their attribution of proof failure causes reliable enough? What is the error rate of generated specification drafts in terms of semantic deviation? These require empirical data rather than intuitive judgment.

What is certain is that the barrier to formal verification is being repriced. When scarce experts' time shifts from "writing" to "reviewing," the upper limit of the field's scale moves. For engineering teams, what is worth doing now is a small-scale pilot: choose a module with clear specifications and high cost of errors, let the model participate in drafting specifications and proofs, and record the actual savings from human review. Data will be more persuasive than opinions.

One-line Summary

By reducing the human cost of specification writing and proof engineering, LLMs make it possible for formal verification to scale.

Paragraph Summary

Based on a Hacker News discussion, this article analyzes how large language models are making formal software verification feasible at larger scales. The core judgment is: the scalability bottleneck of formal verification lies not in prover capability but in the supply of scarce expert labor. LLMs enter at specification generation and formal translation, drafting and repair of proof scripts, and discovery of invariants and preconditions, transforming "construction from scratch" into "review and repair." But the article emphasizes that the trust boundary must not be blurred: LLM output is only candidate material, and final conclusions must be backed by machine-checkable proofs; "feasible" points to cost feasibility, not a relaxation of correctness guarantees. A more far-reaching impact may be the shift of formal verification from project-level major reviews to continuous verification.