A closed-loop formal-verification workflow for stateful packet processing
Symbolic discovery → machine-checked proof → executable validation
Explores the state space symbolically. Proposes candidate invariants and finds minimal counterexamples. Fast, but not a proof.
Independently formalizes the model and machine-checks every candidate. Accepts, strengthens, weakens, or rejects. No sorry, no axioms for main properties.
A Python reference model plus a real compiled eBPF/XDP program. Differential tests prove the formal model matches what actually runs.
Translates between all three, keeps names consistent, tracks invariant status, and turns every counterexample into a permanent regression test.
Research question: can Wolfram-assisted invariant discovery reduce the manual effort of proving realistic XDP programs correct in Lean?
Memory safety — every packet read within [0, packet_length]
Parser monotonicity — offset never moves backward
Parser boundedness — offset ≤ packet length
Counter monotonicity — counters never silently decrease
No silent overflow — saturating counters, proved
Rate-limit correctness — C ≤ T ⇒ PASS, C > T ⇒ DROP
Packet preservation, determinism, malformed-packet safety
Refinement — model ≡ real XDP program on all vectors
Relevant to DPU / SmartNIC-class systems; described conservatively, not as a vendor implementation.
| Component | Runs on | Status |
|---|---|---|
Wolfram Language (wolframscript) | Windows | installed |
| Lean 4.32.2 / Lake 5.0 | Windows | installed |
| Python 3.12 reference model | Windows + WSL | installed |
| Clang/LLVM (eBPF target), libbpf, bpftool | WSL Ubuntu-24.04 | to install |
XDP execution via BPF_PROG_TEST_RUN | WSL (no NIC attach) | planned |
Why it works: JSON files under generated/ are the only exchange format between Wolfram, Lean, and the executable — so the OS boundary never leaks into the verification logic.
Verify check: all five toolchains answer a version query before anything else is built.
xdp/, model/, wolfram/, lean/, generated/, scripts/, docs/docs/assumptions.md — every assumption explicit, split into model / eBPF verifier / Linux / DPU classesevaluate(packet, state) → (result, state)The reference model is the semantic anchor: Wolfram, Lean, and the eBPF program are all judged against it — and it stays independent of the eBPF implementation.
Packet.lean, State.lean, Parser.lean — defined independently, not imported from Wolfram outputlake build green, zero sorryPacketModel.wl, StateTransition.wl — symbolic packets with byte constraintsgenerated/test_vectors.json, replayed against the Python model — actions must agreeIndependence is the point: if two teams derive the same safety condition from the same spec, agreement is evidence, not coincidence.
The spec forbids building the rate limiter until parser safety is settled. This gate is where the plan is reviewed: representations compared, naming table (packetLength ↔ Packet.length ↔ data_end − data) locked in, assumptions re-checked.
Everything after this gate builds on a proven-safe parser.
invariants.jsonGeneratedInvariants.leancounterexamples.jsonProved results land in invariant_status.json: PROVED / STRENGTHENED / WEAKENED / REJECTED / REDUNDANT — plus proof metrics per theorem.
Every generated theorem keeps its original Wolfram expression alongside the Lean translation, and both are evaluated on test assignments to catch semantic drift in translation.
This is the refinement property (§7.10) made executable: the thing we proved theorems about and the thing that actually runs must agree on every vector — including every counterexample the loop ever found.
sorry appears in final proofsPlus conservative relevance docs: this verifies the software class that runs on DPU / SmartNIC platforms — it does not claim anything about proprietary silicon.
Plan: C:\Amp_demos\Xsightlab\DEMO_PLAN.md · Graph: DEMO_PLAN_Workflow.drawio