Basis Finds nftables Bugs With LLM-Guided Formal Verification
Basis says an LLM-guided formal-verification project found two critical semantics bugs in the nftables compiler and optimizer affecting Linux versions since 2022. The work used machine-checked Rocq proofs, but it does not verify the whole production path: the kernel data plane and parts of the command-line tooling remain outside the proved boundary.
Basis reports that an LLM-guided formal-verification project uncovered two critical bugs in the compiler and optimizer used by Linux's nftables firewall tooling. The result is evidence for pairing language models with machine-checked proofs, but the public implementation is explicitly experimental and does not verify the entire networking stack.
What Basis verified
The project formalized four pieces in the Rocq theorem prover: the nftables rules language, the register-based bytecode executed by the kernel, a compiler between them, and an optimizer for rulesets. Basis says the model generated the definitions, implementation, and proofs, while additional model review, virtual-machine tests, and adversarial test cases checked the work.
The core property is semantic preservation: compiling or optimizing a ruleset should not change whether a packet is accepted or dropped. That matters because a firewall optimization bug can silently turn an intended deny rule into an allow path even when the original policy looks correct.
Basis says the verification effort exposed two critical semantics bugs affecting every Linux version since 2022 and that the issues were disclosed to nftables maintainers. The article also describes a smaller experiment in which a model searched directly for optimizer bugs without the proof workflow. It found several silent problems but missed the more severe flaw, supporting a narrower conclusion: the formal specification and proof obligations were important to the discovery process.
The proof boundary matters
The public verified-nftables repository describes a Rocq implementation of the verified compiler and optimization passes, plus an OCaml command-line utility. Its README says the compiler reproduces the stock nft utility's bytecode on 2,532 of 2,532 tested rule blocks and validates 28 field-offset and metadata cases against a live installation. Those are project-reported test results, not an independent security certification.
The same README is direct about what remains outside the guarantee. The kernel-resident data plane that interprets the bytecode is trusted rather than verified. The OCaml path that parses and installs rules is not fully exercised, and the Linux network-state model does not yet represent every real configuration. The maintainers therefore warn against using the project on production systems where security matters.
Why practitioners should care
The useful pattern is not “an LLM found bugs.” It is a workflow in which a theorem prover checks the model's proof artifacts and exposes inconsistencies between the specification and implementation. Security teams evaluating similar work should inspect the exact theorem statements, axioms, unverified components, reproducible tests, and upstream fixes. A proof can be strong inside its model while leaving operationally important code outside the trusted boundary.
Key Points
- 1Basis says LLM-guided Rocq verification found two critical nftables semantics bugs affecting Linux versions since 2022.
- 2A direct model-based bug search missed the more severe flaw, suggesting that formal specifications and proof obligations contributed materially to the discovery.
- 3The repository warns that its kernel data plane and parts of the OCaml installation path remain unverified, so the project is not production-ready.
Scoring Rationale
The reported bugs affect a widely used Linux packet-filtering component and demonstrate a concrete LLM-assisted formal-verification workflow. The score remains bounded because the findings are reported by the project team and the public implementation explicitly leaves important production components outside the verified boundary.
Sources
Primary source and supporting public references used for this report.
Practice interview problems based on real data
1,625 SQL & Python problems across 15 industry datasets — the exact type of data you work with.
Try 250 free problems
