LLM-Assisted Formal Verification Uncovers Two Critical nftables Bugs
Basis used LLM-guided formal verification in Rocq to audit Linux's nftables optimizer, uncovering two critical bugs since 2022.
Basis researchers applied LLM-guided formal verification, using the Rocq theorem prover, to formally verify nftables — the firewall compiler and optimizer that filters traffic on virtually every Linux system. The goal was to prove that nftables' optimizer preserves the semantics of user-defined rules.
The effort uncovered two bugs present in every Linux release since 2022. The first, a flawed bitmask-merging optimization, silently converted restrictive rules into overly permissive ones — turning "any packet with SYN set" into "only packets with exactly SYN set" — which could let unwanted traffic through undetected. The second bug incorrectly merged overlapping address ranges into a verdict map, producing invalid rulesets rejected by the kernel.
The team's verified reimplementation was proven free of both issues, and a follow-up test showed the more severe bug would likely have gone unnoticed by a naive LLM-based bug search — underscoring the added value of formal proofs over ad-hoc LLM scanning for critical infrastructure like firewalls.