Basis | Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack

We used LLMs to verify Linux's nftables `nft` CLI utility. Along the way, we found and patched bugs that had sat in the kernel for years.

LLMs have grown alarmingly capable at finding bugs in production software. This accentuates an already severe risk: much of our critical infrastructure is mediated by software, and every bug in that software is a potential exploit. Formal verification offers the potential to mitigate this risk by producing proofs that entire classes of bugs are impossible, but it has seen limited real-world use because it demands scarce, expensive, specialist expertise. Fortunately, LLMs are increasingly capable of verification too, pointing toward a future where critical software infrastructure is secure by…

saved by

• Davis Brown

related reading

• When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
• A shallow dive into formal verificationvitalik.eth.limo
• Assessing Claude Mythos Preview’s cybersecurity capabilities \ Anthropicred.anthropic.com
• Automatic Formal Verification for Code Generationlogicalintelligence.com
• Formally Verifying the Easy Partbrainflow.substack.com
• From Naptime to Big Sleep: Using Large Language Models To Catch Vulnerabilities In Real-World Code - Project Zerogoogleprojectzero.blogspot.com
• lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
• Formalizing Fermat's Last Theoremanthropic.com
• Tao on “blue team” vs. “red team” LLMs | Hacker Newsnews.ycombinator.com
• LLM-as-a-Verifier: A General-Purpose Verification Framework | alphaXivalphaxiv.org
• Finding Miscompiles for Fun, Not Profit - by Justin Lebarnewsletter.semianalysis.com
• AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com