AI Large Language Models Drive Assembly-Level Formal Verification: Practices and Breakthroughs

1. Introduction: When Large Models Move from “Writing Code” to “Proving Correctness”

In software engineering, a vast gulf separates “writing code that runs” from “proving code never fails.” Traditional software testing—whether unit testing, fuzz testing, or integration testing—is fundamentally sample-based: it can only demonstrate that a program behaves correctly under the specific inputs that have been tested, never under all possible input combinations.

Large language models (LLMs) have recently made remarkable strides in code generation and code completion. An even more ambitious direction is now emerging: using LLMs not just to write code, but to prove it correct. A recent research effort demonstrated that, by leveraging the reasoning capabilities of LLMs, a team formally verified 123 widely security-tested open-source libraries over several weeks—covering 239 test entry points and producing approximately 180 million lines of machine-checked proof code. This represents the first known large-scale use of AI to perform assembly-level formal verification on production-grade software.

This article systematically examines this frontier across five dimensions: technical principles, methodology, real-world cases, engineering challenges, and future outlook.

2. Formal Verification: A Paradigm Shift from “Testing” to “Proving”

2.1 What Is Formal Verification?

Formal verification is a mathematical approach to guaranteeing software correctness. Its core idea is to model program behavior as logical formulas and then use rigorous reasoning to prove that these formulas satisfy predefined specification properties—such as “no buffer overflow can occur” or “no null-pointer dereference is possible.”

The essential differences from traditional testing are summarized below:

Dimension	Traditional Testing (including fuzzing)	Formal Verification
Coverage	Finite sample inputs	All possible inputs (exhaustive)
Conclusion strength	“No errors found”	“No errors of this type exist under the given specification”
Automation level	High (but requires many test cases)	Moderate (requires modeling and reasoning)
Trust metric	Depends on test coverage	Depends on the reliability of the proof system

2.2 Why the Assembly Level?

Formal verification can be performed at the source-code level or at the compiled assembly/machine-code level. This practice chose assembly for three reasons:

1. Closer to real execution semantics: Compiler optimizations can alter control flow; assembly-level verification captures issues introduced during compilation.
2. Avoids source-level ambiguity: Different programming languages have vastly different semantics, while assembly instruction sets are relatively uniform and more direct to model.
3. Covers testing blind spots: Many security vulnerabilities appear precisely in code paths generated by the compiler—paths that source-level testing often misses.

3. The AI-Driven Verification Path: From “Fuzzing” to “Proof-Driven Discovery”

3.1 Inherent Limits of Fuzz Testing

Fuzz testing is a widely adopted automated security technique in industry. It works by feeding a program large volumes of random or semi-random data and monitoring for crashes, hangs, or anomalous behavior.

Its effectiveness depends on input-space coverage, but practical constraints exist:

• Input size limits: To control time and resource consumption, single inputs are typically capped at 1 MB.
• Path-exploration bias: Random mutations struggle to systematically reach deep branch logic.
• State-space explosion: Vulnerabilities that require multi-step specific input sequences are nearly impossible to trigger randomly.

3.2 “Proof as Discovery”: The Power of Inverted Thinking

The core methodological innovation here is not asking AI to “find bugs” but to “prove there are no bugs.”

The logic chain works as follows:

1. Set verification goals: For a given function entry point and safety property (e.g., “no out-of-bounds write under any input”), the AI must construct a formal proof.
2. Attempt proof construction: The AI exhaustively explores all input paths, deriving correctness for each branch.
3. Counter-examples reveal bugs: If any input can trigger a violation, the proof cannot be completed. The AI must explicitly “defend against” every potential counter-example during the attempt.
4. Fix and re-prove: Once a vulnerability is confirmed, the AI patches the code and restarts the proof process on the modified version.

This “proof-driven bug finding” approach transforms fuzzing’s passive “wait for a collision” into active, exhaustive adversarial reasoning—uncovering deep defects that conventional methods cannot reach.

3.3 A Notable Case: A 20 MB Input Triggers a Counter Overflow

In a widely used data decompression library, AI uncovered a subtle flaw: specifically arranged input data of approximately 20 MB caused an internal counter miscalculation, leading the program to write beyond allocated memory and trigger a buffer overflow.

Why didn’t traditional fuzzing catch it? Because conventional tests cap inputs at 1 MB, and triggering this vulnerability required a special input exceeding that limit. Under the task of “proving safety for all inputs,” however, a 20 MB input is squarely within the AI’s scope—if it causes an error, the proof fails.

It was this “no input left unexamined” exhaustive scrutiny that allowed AI to capture a long-dormant security risk. According to the team, following this approach has already yielded hundreds of similar deep defects.

4. Engineering Reality: 391 Lines of Code, 630,000 Lines of Proof

4.1 The Astonishing Proof Expansion Ratio

For a single parsing entry point in a lightweight JSON parsing library, the source code was just 391 lines of C—yet the AI produced roughly 630,000 lines of formal proof code, an expansion ratio exceeding 1,600×.

This “proof bloat” is not inefficiency; it is an inherent characteristic of formal verification:

• Infrastructure modeling: Proofs must cover not only the target function but also the correctness of all underlying functions it calls (memory allocation, string operations, etc.).
• Instruction-level reasoning: At the assembly level, every machine instruction requires individual logical derivation; 391 lines of C may compile to thousands of instructions.
• Auxiliary lemmas and intermediate states: Complex derivations demand numerous lemmas, each of which must also be machine-checked.

4.2 AI’s Self-Tooling Capability

To handle the massive volume of repetitive proof work, the AI demonstrated notable self-tooling ability: it autonomously wrote auxiliary generation scripts that automated over half of the proof content. This included:

• Batch-generating proof templates for similar structures.
• Automatically invoking the underlying proof engine for sub-goal verification.
• Caching and reusing already-verified foundational modules.

This pattern of “AI writing tools to help itself verify” significantly boosted overall efficiency and provided critical support for the feasibility of large-scale formal verification.

5. Technical Challenges and Future Outlook

5.1 Core Challenges Today

1. Enormous compute requirements: Generating and checking 180 million lines of proof demands substantial computational resources.
2. Human cost of specification writing: Formal verification requires precisely defining “what is correct”; specification authoring still needs deep expert involvement.
3. Maintainability: When code changes, associated proofs must be updated synchronously or they become invalid.
4. Scaling bottleneck: Current results mainly cover function-level entry points; end-to-end system-level verification remains a distance away.

5.2 Baidu AI Cloud’s Technical Positioning

Baidu AI Cloud has been investing in related capabilities in this frontier area. Drawing on its expertise in AI infrastructure, large-model services, and cloud-native security, Baidu AI Cloud aims to provide enterprise customers with intelligent code security analysis and verification capabilities. For example, by combining LLM reasoning with formal methods, automated security verification steps can be embedded in CI/CD pipelines, helping developers catch deep defects at the code-commit stage. Meanwhile, Baidu AI Cloud’s container platform and object storage infrastructure also offer elastic compute support for large-scale verification tasks.

5.3 Future Directions

• From function-level to system-level: Extending verification granularity from individual entry points to modules and entire applications.
• Human-AI collaborative specification: Using LLMs to assist in generating formal specifications and lowering the expert barrier.
• Integration with static analysis: Combining formal verification with traditional static analysis tools to build multi-layered security assurance.
• Continuous verification: Embedding verification into the software development lifecycle for automatic re-verification after code changes.

6. Conclusion

The shift from “letting AI write code” to “letting AI prove code correct” marks a new chapter in software engineering. This large-scale formal verification practice shows that LLMs are not only efficient code-generation tools but also have the potential to serve as rigorous logical reasoning engines. Although challenges around resources, specifications, and maintainability remain, the “proof-driven discovery” paradigm has already proven its unique value in mining deep defects. For software systems that demand high assurance, AI-assisted formal verification may become core infrastructure for the next generation of security engineering.