# Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack > Source: > Published: 2026-07-20 13:57:41+00:00 # Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack ##### Article: [Yiyun Liu](/about/people/yiyun-liu/), [Kiran Gopinathan](/about/people/kiran-gopinathan/), [Nikhil Pimpalkhare](/about/people/nikhil-pimpalkhare/) [Yiyun Liu](/about/people/yiyun-liu/) 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 construction. In this blog post, we report on results from LLM-guided verification experiments at Basis. Our target was a key component of Linux’s network stack: the nftables firewall compiler and optimizer, which we set out to verify in the Rocq theorem prover. nftables is one such piece of critical infrastructure. It filters the traffic of almost every Linux machine, and vulnerabilities in it are treated with the highest severity, since a firewall that misfilters exposes every machine it was meant to protect. In the process of verifying nftables, we uncovered **two critical bugs** affecting every version of Linux since 2022 (these have been disclosed to maintainers 1). Our verified implementation was *proven to be free*of these semantics-altering bugs, and a secondary experiment showed that the more severe of the two would not be found via a naive LLM bug search. Our experiments suggest that the effort involved in producing proofs and constructing robust verified systems is increasingly automatable. The rest of this post gives an overview of nftables, the bugs we found, and our process for using LLMs to verify critical networking software. # A quick primer on nftables and its bugs nftables is one of the firewall mechanisms provided by the Linux operating system. Every packet your OS receives passes through nftables, which determines which packets are forwarded and which are dropped. Having replaced `iptables` in 2014 as the default packet filter of every major Linux distribution, nftables today guards everything from home routers to container networks; if a Linux machine filters traffic, nftables almost certainly decides what gets through. Firewalls are a critical component of most network security layers, and vulnerabilities in them can compromise whole systems. A verified implementation of nftables would increase assurance in this critical layer. ## nftables rulesets and compilation pipeline The full architecture of nftables is shown below and consists of a userspace CLI tool and a kernel module: This CLI tool takes as input a series of user-supplied policies, expressed as an ordered list of rules, where each rule matches on some part of the packet (its source address, its destination port, its TCP flags) and returns a verdict, i.e. `accept` or `drop` . For example, the following rules tell nftables to accept any packets where the destination address (`daddr` ) is `192.168.50.1` or `192.168.50.2` . ``` ip daddr 192.168.50.1 accept ip daddr 192.168.50.2 accept ``` The `nft` command-line tool parses these rulesets and compiles them into a compact register-based bytecode, which it then loads into the kernel. There, the kernel’s interpreter uses the bytecode to compute a verdict for every packet passing through the network stack: either accepting it through the firewall or dropping it. As this bytecode runs on every packet the system sees, it sits on a hot path of the kernel, and thus its efficiency is critical. For this reason, the CLI tool also provides an optimizer module for the source language that rewrites your input rules to run more efficiently (reducing the number of reads, or removing redundant checks). A critical security property that users rely on the optimizer to guarantee is that it *preserves the semantics* of its input rules. In other words, the verdict computed for a packet should be the same regardless of whether it was passed through the optimized or unoptimized ruleset. We set out to prove the correctness of the `nft` command-line tool, and in the process found two bugs in the system. ## Bugs found Our key results were finding two key cases where the optimizer does *not* produce equivalent programs: The first bug was an invalid optimization, which if applied, resulted in accepting packets that would have been rejected before optimization (!!). The second resulted in the optimizer transforming valid rulesets into invalid rulesets that are rejected by the kernel. We were able to reproduce these bugs in the latest version of the nftables userspace tool, and proved our verified re-implementation was entirely free of these semantics-altering bugs. ### Bug 1: Invalid merging of bitmask fields The first bug relates to an optimization wherein bitmask fields are merged. Packets include a series of control-flag bits — TCP packets, for example, have `SYN` , `ACK` , `FIN` , and others. nftables allows users to write rules that test whether a particular bit is set: `tcp flags syn` matches any packet that has the `SYN` bit on. So the following ruleset drops every packet with `SYN` set and every packet with `ACK` set: ``` tcp flags syn drop tcp flags ack drop ``` The optimizer, `nft -o` , merges these two rules into a single one: ``` tcp flags { syn, ack } drop ``` Unfortunately, this rewrite is **incorrect**. The merged rule does **not** mean the same thing. In particular, the semantics of the nft input language is defined such that a set lookup is an *exact-match* test: the packet is dropped only if its flags byte equals `syn` exactly (the `SYN` bit set and all other bits clear) or `ack` exactly. The original rules asked “is this bit set?”; the merged rule asks “is the flags byte equal to exactly this one bit, with everything else zeroed-out?” The same narrowing applies to any bitmask-typed field matched in this bit-test form. This bug is particularly pernicious as it silently converts a restrictive policy into a more permissive one, and could have *critical* safety implications: in the previous example, most syn and ack packets would have been dropped, but after optimization, only packets with *only* the `SYN` or `ACK` bit set would be dropped (a substantially smaller set of packets). ### Bug 2: Invalid merging of overlapping ranges The second bug we found relates to an optimization that merges rules based on their addresses. When consecutive rules match the same field, `nft -o` merges them into a *verdict map* (`vmap` ) — a lookup table that sends the field’s value to a forwarding verdict. This reduces multiple reads of the field into a single read and then a jump in the bytecode. Consider a ruleset that drops one range of source addresses and accepts another: ``` ip saddr 192.168.50.1-192.168.50.123 drop ip saddr 192.168.50.120-192.168.50.255 accept ``` `nft -o` merges the two rules into: ``` ip saddr vmap { 192.168.50.1-192.168.50.123 : drop, 192.168.50.120-192.168.50.255 : accept } ``` Unfortunately, the implementation of optimization has a bug and the generated map is ill-formed. In particular, nftables requires that a `vmap` must map each address to a *single* verdict: its keys must refer to non-overlapping intervals. In contrast, in our example, the optimizer has reused the original ranges without checking their disjointness, so keys overlap on `.120` –`.123` . As such, after optimization, the generated ruleset is rejected with an error `Error: conflicting intervals` . This bug leads to a valid ruleset being optimized into an invalid one, such that an error is raised to the user when they try to install the optimized ruleset. In this case, the security considerations are less severe, but this still represents an incorrect optimization and ultimately reduces trust in `nftables` . # Formally verifying nftables Both bugs were found autonomously by LLMs during an ongoing effort to verify nftables’ userspace components, that is, while proving that `nft` preserves the behavior of rulesets. To formally prove that an implementation has this property, we first have to pin down what a ruleset means, and then verify the implementation against that meaning. We formalized, in the Rocq theorem prover, four pieces: - the syntax and semantics of the nftables rule language, - the syntax and semantics of the register-based bytecode that the kernel executes, - a compiler from rulesets to bytecode, and - an optimizer that rewrites rulesets into more efficient rulesets. Pieces (3) and (4) are verified counterparts of the two halves of the `nft` CLI tool from our primer, and piece (2) plays the role of the kernel’s bytecode executor. Building on the formalized semantics, we stated and proved that the compiler and the optimizer are both semantics-preserving. That is, the bytecode produced by the compiler accepts and drops exactly the packets that the input ruleset does, and an optimized ruleset matches exactly the packets that the original does: Two pieces sit outside the proofs: the parser, which turns nftables rulesets into a Rocq AST, and the serializer, which installs the bytecode into the kernel. Both are unverified OCaml, packaged in our `nftc_cli.exe` command-line tool, which links against the verified compiler and optimizer. The verified implementation is still a work in progress, but it is close to feature parity with ~90% of the nftables rule language modeled and verified. An LLM was used to write every definition, line of code, and proof in the verified implementation. # An autonomous verification methodology This section describes the methodology we used to automate our development. All code and proofs were generated by Claude CLI running in auto mode, with Opus 4.8 as the model. The LLM started from a detailed prompt that specified the verifier (Rocq, in our case) and the part of nftables to verify, and pointed to prior work on formal verification and networking. The prompt also spelled out the proof-engineering and general engineering practices we expected the LLM to follow, such as test-driven development and frequent code reviews. ## Testing harness We instructed the LLM to launch a virtual machine (VM) with `systemd-vmspawn` and to use network namespaces to construct test environments where nftables rules could be installed and exercised on different network topologies. The VM also gave the LLM a sandbox in which to run the official `nft` command line tool and experiment with its behavior. On top of this harness, we ran end-to-end differential tests: a corpus of rulesets was fed to both our verified compiler and the official nftables implementation, and their outputs were compared. ## Adversarial workflow Development proceeded through an adversarial loop between two LLMs: one wrote the specification, implementation, and proofs, and the other reviewed them for a specific type of flaw and reported what it found. The loop continued until the reviewing LLM was convinced that the type of flaw had been properly fixed. This workflow was particularly effective at exposing fidelity issues in the language semantics, where the implementing LLM prematurely claimed victory even though the meaning of an expression was not precisely modeled (e.g. an effectful expression approximated as a pure one). To surface such semantic gaps, we instantiated the adversarial template with a reviewing LLM that cross-checked the verified code against the actual C implementation of nftables, flagging under-specifications. ## Small Proof-Oriented Tests (SPOT) To further pressure-test the semantics, while also producing an artifact end users can apply to debug their own firewall configurations, we built special test cases in which the LLM had to state and prove properties of real rulesets: either a formal proof that a ruleset captures the user’s intent, or a counterexample showing where that intent can be violated. When a ruleset resisted specification and reasoning, that was a signal that the semantics was not yet precise enough and could be improved. # How were the bugs found? Both bugs we include in this blog post were found autonomously by the LLM throughout the development. What is more interesting than the bugs themselves, however, is how the bugs were found. The overlapping interval bug was found thanks to the testing harness. On June 30th ([ 69666ba](https://github.com/BasisResearch/verified-nftables/commit/69666ba)), the LLM synthesized a battery of artificial rulesets designed to trigger the optimizer rewrites of nftables and better understand its behavior. The harness ran each ruleset through both optimizers and loaded the results into the kernel inside a fresh network namespace. The bug turned up incidentally when one of these rulesets triggered a loud failure ( `conflicting intervals` ) on the `nft` command line.The story behind the unsound bitmask merge bug, however, is a lot more eventful. In commit [ 17c949a](https://github.com/BasisResearch/verified-nftables/commit/17c949a), the LLM added its own, sound version of the bitmask merging optimization. When consecutive rules match on the same bitmask field, its optimizer folds them into an OR of the original “is this bit set?” tests, rather than nftables’ exact-match set. The commit message reveals that the LLM was already aware that the exact-match semantics of a set makes it unsuitable for merging bitmask-typed expressions. However, the LLM only used that unsoundness to justify its own divergence, rather than recognizing it as a bug in nftables itself. In fact, according to the commit message, the LLM tried to rationalize nftables’ buggy merging behavior by pointing out that the field it was merging, the packet’s connection-tracking state `ct state` , can have at most one bit set at a time. Therefore the merged set `ct state { new, established }` , which compares the packet’s connection-tracking state against the exact bits of `new` or `established` , is harmless, and can be found, for example, in the [Arch Linux default ruleset](https://gitlab.archlinux.org/archlinux/packaging/packages/nftables/-/blob/8a56b5d745b7731488a4f2afe437f713bbc0146f/nftables.conf#L14). The bug was not surfaced until we explicitly prompted the LLM to explain its divergence from the official optimizer in a July 14th commit ([ c786563](https://github.com/BasisResearch/verified-nftables/commit/c786563)). That’s when the LLM finally realized that nftables’ optimizer does lead to unsound behavior since there are other bitmask-typed expressions such as `tcp flags` and `ct status` , where multiple bits can be set at once, and managed to confirm the bug through the VM testing harness. Formal verification thus protected us from bugs that neither we nor the LLMs expected.After surfacing these two bugs, we conducted a small experiment where we started a fresh Claude session and instructed it to use the same VM testing harness to look for bugs in the official nftables optimizer. The LLM ran for a few hours, and managed to identify 16 bugs, 3 of which involve silently changing semantics, and 13 of which involve crashing the optimizer due to invalid optimized rules. We are in the process of disclosing these bugs to the maintainers. Did Claude manage to find both bugs surfaced in our verification endeavor? The answer is no! While the overlapping interval bug was indeed found by Claude, the bitmask bug remained hidden after a few hours of running. In fact, from examining the chat history, the LLM would be unlikely to find the bug even if we ran it for longer, as it managed to reproduce the exact ruleset that was able to trigger the optimizer bug, but found the new output reasonable and decided to move on. Unlike the 3 silent bugs that the LLM did manage to find just through eyeballing the buggy output rules, the bitmask bug requires a deeper understanding of the meaning of nftables semantics. Finally, a perhaps even more encouraging result is that the verified implementation is not susceptible to the 3 optimization bugs that Claude managed to find. Despite the verified implementation still being work in progress, the LLM-generated semantics capture more than enough of nftables to reject those buggy optimization rules with the correctness theorem. Smarter models may be better at identifying bugs, but formal verification truly grants us a higher level of assurance. # Findings and Observations Over the course of this initial verification effort, most of the human effort was in validating, reviewing, and refining specifications. While failing proofs were easy to eliminate, as the LLM would keep working until Rocq accepted, a theorem that had been quietly weakened could easily be missed. Given work it does not want to do, we often found LLMs would shrink the task in some way that a casual reading could easily miss. We saw two recurring forms of this: - the LLM weakened its specifications with convenient preconditions and - the LLM warped the design of the system so that hard lemmas never arose. ## Weakening a theorem with a precondition The optimizer’s correctness theorem provides a representative example of this failure mode. Part of the optimizer implementation needs to generate fresh names, which would ordinarily mean threading a name-generation state through the surrounding code. The names are only needed when rewriting rules with effects, rules that update state or modify the packet. Rather than do the plumbing, the LLM narrowed what its theorem had to say: ``` Theorem optimize_table_correct : forall n d c n' d' c' base p, optimize_table n d c = (n', d', c') -> rules_clean (c_rules c) = true -> … -> eval_chain c' (set_env p (env_with_sets base d')) = eval_chain c (set_env p (env_with_sets base d)). ``` In particular, the `rules_clean` assumption that was subtly inserted is a predicate that holds only on pure rules. With this restriction the theorem could be proven without the plumbing infrastructure. The theorem was still named `optimize_table_correct` and proven correct, though the statement now said nothing about rules with effects. ## Register allocation in the parser Sometimes the LLM would shortcut by reshaping the specification definitions themselves rather than the theorem directly. An example of this came in the register allocation implementation: the `nft` compiler targets the kernel’s register-based bytecode interpreter, so at some point in the compilation pipeline, the compiler must allocate registers. The LLM tried to avoid proving lemmas about register allocation, by extending the source AST with registers, leaving the parser, which lives outside the verified core, to assign them. This led to an incomprehensible design where part of the allocation happened during parsing, but in terms of the proof obligations for the LLM, the compiler became easier to verify as complex logic became outsourced to unverified code. # Conclusions Verification is not new. For decades, researchers have dedicated huge amounts of labor to verifying critical software infrastructure, and in the process have historically often uncovered critical bugs. What is new is that this labor is now increasingly automatable through the use of LLMs. While ongoing, even our interim progress on this project would have likely required years of human effort to complete; boosted by LLMs, we reached a working implementation in a manner of weeks. We reap the same benefits as traditional verification: we are working towards a reimplementation with a proof of correctness baked in, and along the way we were able to uncover critical bugs in the nftables optimizer. Some of this labor, however, remains manual. The LLMs repeatedly tried to downscope their task and procrastinate on challenging proofs. Most of the human effort in our development went into catching this behavior. It remains to be seen whether a more sophisticated harness or advances in model capabilities can automate this final step. We intend to find out ourselves. Our next goal is a fully automated pipeline, one that verifies critical software infrastructure at scale without a human in the loop.