Verified Nftables

A vibe-coded, formally verified userspace tool that compiles an nftables ruleset to its register-based bytecode representation. The tool also comes with verified optimization passes that roughly matches the functionality of nft -o, the canonical Linux userspace tool that interacts with nftables.

The core compiler is implemented in Rocq, and the unverified command line utility that installs the compiled bytecode to the Linux kernel is implemented in OCaml. The nftables data plane, which lives inside the kernel and interprets the bytecode, is trusted and unverified.

Other than building and running the nftc_cli.exe command line tool, you can also use Rocq to formally prove properties about your ruleset (see proof/theories/Examples/Optiplex_Antispoof.v, which reasons about the ruleset optiplex.nft). A step-by-step tutorial for this analysis workflow — write a .nft file, parse it into Coq terms with make gen, then prove it blocks exactly one IP range (an iff, for all packets) — is in proof/CONFIG_PROOFS.md, with the worked example rulesets/tutorial.nft / proof/theories/Examples/Tutorial_Proofs.v.

The core compiler is tested against the stock nft utility, but the untrusted OCaml code isn't fully exercised. Therefore, you should absolutely not use the code for your home server or any production environment where you care about security. However, using this code base as an analysis tool for finding bugs in your specific ruleset is a perfectly valid and harmless use case.

The Linux network state is not faithfully modeled. For example, the semantics still assumes that each interface can bind to only a single IP address. The long term goal is to eventually close the gap so you can faithfully reason about ct and fib expressions, which depend on conntracking and routing tables states.

There are multiple motivations for this project. First, I want to eventually use the formal semantics to supplement the sparse and incomplete documentation of nftables. For example, my home router uses the bitwise & operator to allow inbound IPv6 traffic to a specific machine whose IPv6 prefix is dynamically allocated by the ISP. The operator is not in the documentation, and I was only able to learn this feature from a blog post and some stackexchange threads. Second, as a follow-up to the verified javascript to wasm compiler experiment, I want to see how well LLM agents can handle a domain specific language with an underspecified semantics. So far, the agent seems to be doing okay but requires lots of manual prompting. A good next step is to figure out whether the process can be fully automated through more aggressive testing, integrated into an adversarial workflow.

The remaining text in the README file is generated by LLM.

The verified compiler (proof/)

• Semantics-preserving compilation + a verified DSL optimizer, machine-checked in Rocq. compile_chain_correct says the bytecode VM agrees with the DSL semantics, compile_chain_default_correct extends that to the default pipeline the CLI actually emits (nft's always-on single-rule linearization — adjacent-payload merge + xor constant fold — composed before compile), and optimize_table_uncond_compile_correct says the default-compiled bytecode of the optimized chain preserves every packet's verdict. The optimizer theorem is per-chain: it quantifies over a single chain and all environments and packets, with no rules_clean or freshness precondition; multi-chain/hook preservation is the separate compile_ruleset_correct/compile_hook_correct family (not composed with the optimizer). The full theorem map is proof/THEOREMS.md.
• Differential-tested against the upstream nftables test corpus. Extracted to OCaml, it reproduces the real tool's bytecode on 2532/2532 (100%) of the corpus's rule-blocks with zero mismatches (cd proof && make corpus). Read that number for what its oracle direction supports: make corpus reconstructs the DSL rule from each corpus netlink block and checks render(compile(reconstruct(b))) = b — a payload-level round-trip fixed point, not a compile-from-.nft-source diff, so a systematic misunderstanding of nft's source→bytecode mapping that the reconstructor and compiler share would round-trip cleanly. The independent cross-checks are make validate (field offsets / meta-ct names vs a live nft, 28/28), make byteorder-gate (host-endian corpus blocks compiled from their # <src> headers), and the difftest/e2e/parse-test source-side diffs vs live nft. The measured source-side coverage of the corpus itself, and why the full source-driven gate is not wired in yet, are in proof/DEVELOPMENT.md § "What the round-trip does and does NOT validate".
• Data-plane semantics hardened by an adversarial red/blue fidelity audit against the linux kernel source — see adversarial.md. Two residual, confirmed model-vs-kernel divergences remain open by design and are ledgered (with vm_compute lock-in pins) in proof/DEVELOPMENT.md § "Known model infidelities" (the historical third — intra-rule set-then-read — is repaired by the single-fold rule semantics; positive pins in proof/theories/Regression/Setread_IntraRule.v).
• Headline guarantees are axiom-free ("Closed under the global context"): the anti-spoofing (env-universal antispoof_general_any_env), established-accept (axiom-free but vacuous as stated — its whole-env pin contradicts its own ct hypothesis; ledgered OPEN in proof/THEOREMS.md §5), NAT-masquerade, multi-address primary-selection, fib host-local, ct-state, fuel-adequacy (the jump strand's fuel budget is a discharged side condition: verdicts are provably fuel-independent above a computable bound — proof/THEOREMS.md §3 "Fuel adequacy"), and the de-vacuized optiplex firewall-mark results (Optiplex_Mark.*_real, proof/THEOREMS.md §5). This is a gated claim, not an eyeballed one: every theorem in this list is in AXIOM_GATE_THEOREMS (proof/Makefile), and cd proof && make axioms fails the build if any of them acquires an axiom or an Admitted (see proof/THEOREMS.md §4 for the exact set).

Start at proof/DEVELOPMENT.md for the design notes and the honest scope of the "2532/2532" claim.

Build & run

Everything below runs from the proof/ directory.

Prerequisites

• Rocq (Coq) 9.1.1 and an OCaml 4.14 / dune toolchain, in an opam switch. If your Rocq lives in a named switch, activate it first, e.g. eval $(opam env --switch=vst).
• A live nft (nftables; tested against v1.1.6) for the differential gates (corpus, validate, difftest, e2e, parse-test).
• git + network access the first time you run make corpus (it clones the upstream nftables test corpus to /tmp/nftables-src, overridable with NFT_CORPUS=...).
• unshare with unprivileged user namespaces for make nl-send / make difftest.

Build & check the proofs (also extracts the verified compiler to extracted/*.ml and builds the OCaml glue):

cd proof
make                 # build/check every theory + extract + build glue

The verified CLI — nftc (parse → optimize/compile → netlink text; the optimize/compile core is the extracted verified term):

make cli             # builds extracted/_build/default/nftc_cli.exe
./extracted/_build/default/nftc_cli.exe optimize ../rulesets/ruleset.nft   # parse->optimize_table_uncond->compile->render
./extracted/_build/default/nftc_cli.exe compile  ../rulesets/router.nft    # parse->compile_chain->render
# equivalently, via dune (note the `--` and the ../../ path from extracted/):
cd extracted && dune exec ./nftc_cli.exe -- optimize ../rulesets/ruleset.nft

nftc has three modes — compile, optimize, and send (the last pushes the verified-compiled rules to the kernel over a real NETLINK_NETFILTER socket; it mutates kernel state and requires --commit, otherwise it dry-runs). Flags: --table T, --chain C, --no-optimize, --commit. Read from stdin with -.

Scope of send: compile/optimize render the full --debug=netlink text for everything the verified compiler supports. The send mode's binary netlink encoder currently covers only a subset of instructions, so it refuses (cannot encode for netlink: …) on rules that use, e.g., ct/named-set lookups. Use compile/optimize to inspect those.

Gates, demos, and other executables (each is make <target> from proof/):

target	what it builds/runs
make corpus	round-trip the upstream nftables corpus through the verified compiler — 2532/2532, 0 mismatches
make validate	field offsets / meta-ct names vs a live nft (28/28)
make semtest	run the extracted DSL semantics + bytecode VM + compiler on concrete packets (a witness of the correctness theorems)
make parse-test	the .nft frontend's round-trip checks (also a CLI: dune exec ./parse_test.exe -- FILE.nft)
make e2e	full .nft → parse → optimize → compile → render, checked against live nft
make nl-send	push verified-compiled rules to the kernel in a fresh net namespace, read back with nft list ruleset
make difftest	byte-identical forward check of a hand-written ruleset vs the local nft
make lib / make example	build the reusable nftc library / build+run its standalone consumer demo
make gen	regenerate the parser-output Coq terms (theories/Generated/*_Gen.v) from the .nft sources (all four rulesets, router.nft included)
make gen-check	drift gate: fail unless every checked-in theories/Generated/*_Gen.v is byte-identical to a fresh nft2coq run over its .nft source
make axioms	axiom-freedom gate: every claimed theorem must be "Closed under the global context" (fails the build otherwise)
make gates	the aggregate enforcement point: proofs + axioms + corpus + validate + parse-test + gen-check in sequence

Sample rulesets to try the CLI on live in rulesets/: rulesets/ruleset.nft, rulesets/router.nft, rulesets/optiplex.nft, rulesets/tutorial.nft.