3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number (Tables I to VII recomputed, including the 232/7, 420/7, 28/7, 36/7 and 524/20 sums), page and section references, Algorithm 1 line numbers, the Appendix A steps, the SMT-LIB listings, quotations and both Verus sketches; changed: the claim that ICMP’s 82 branches was the largest count, the claim that TCP passed every Wireshark-labeled test, syntax errors as the most common refinement, the domain expert credited with the VXLAN misreading, the planner as the only tool user, a section reference (IV-A for the manual RFC cutting), the worked-example miscount claim, the models cluster claim, and four unmarked inferences.

source: Fakhoury, Kuppe, Lahiri, Ramananandro, Swamy (Microsoft Research), arXiv:2404.10362v2, 6 May 2024; 10 pages of text, references, appendices A to C (pp.12-14)

proved, measured, trusted

The paper proves nothing new about parsers. It reuses EverParse, whose earlier proof it restates (§II, p.2): “They prove that every well-typed program assembled from their parser combinators produces a parser that is the inverse of the corresponding serializer, i.e., ∀s. parse (serialize s) == Some s and ∀b v. parse b == Some v =⇒ serialize v == b.” The C code that comes out is therefore correct against the 3D format description, whoever wrote that description.

What the paper adds is a way to get the 3D description from an RFC with GPT-4 agents, and it measures that on 20 protocols. The description itself is only tested, never proved to match the RFC. The paper says so (§II, p.3): “Further, while EverParse guarantees that the generated C code is memory safe, free from bugs that trigger undefined behaviors, and faithfully parses exactly the specified format, the source specification is still subject to audit.” And (§I, p.2): “That said, the specifications 3 D G EN produces are only as good as the tests on which it is evaluated.”

Trusted, by the paper’s own account: the test labels (Wireshark, then two authors’ manual corrections), and the human who picks among surviving candidates. Inference: also trusted and not discussed are F⋆, Karamel, Z3, the C compiler, and the new SMT encoding inside 3DTestGen, for which the paper gives no proof that it agrees with the F⋆ semantics of 3D; it is described only as “grounded in the formal semantics of 3D” (§III-C, p.5).

technique 1: make the model write a small analyzable language, not the final code

What it is. The model’s output is restricted to a declarative DSL (3D: C-like typedefs, structs, casetypes, value constraints). A verified generator turns the DSL into C. The paper’s claim (§I, p.2): “A key enabler of our technique is the use of an effectively analyzable DSL, coupled with a verified code generator, as a medium of interaction between a user’s informal intent and AI-generated output.”

When to use. When the task domain already has a DSL with (a) a checker, (b) an executable semantics and (c) a verified compiler, and when the hard part is getting the specification right from prose.

How it is done.

1. Fix the DSL and its three functions (§III-A, p.3): a syntax and type checker (3DSynChk), an execution function that runs a description on an input and returns accept or reject (3DExec, implemented by compiling to C with EverParse and running it), and the manual with examples (3DDoc).
2. Give the model the manual and the ability to query parts of it, not training: the manual is “around 2,000 lines of text and around 20 examples” (§I, p.1).
3. Have the model emit only DSL text; never ask it for C.
4. Generate the C with the verified compiler after a description has been accepted (technique 2).

The paper’s example (§II, p.3) is a TCP option: a struct with a constrained tag byte and a payload whose type depends on the tag.

typedef struct _OPTION {
    UINT8 Kind { Kind == 0x00 || Kind == 0x01 || Kind == 0x02 };
    OPTION_OF_KIND(Kind) payload;
} OPTION;

Verus form. Inference: the direct Verus counterpart is a parser-combinator library verified in Verus (the Verus note in this collection names Vest as one such system); an agent would then write a format description in that library’s vocabulary and get parser and serializer with the round-trip property from the library’s proofs, writing no proof fn itself. Where no such library fits, the nearest shape is: the agent writes only a spec fn describing the accepted byte sequences, and a separate, fixed exec fn with ensures tying its result to that spec fn is produced and verified afterwards. What changes: Verus has no single checked-once generator from spec fn to exec code, so the proof must be redone per format unless a combinator library carries it. What does not carry over: 3D’s guarantee of double-fetch freedom is a property of EverParse’s generated C; the paper does not say how it is stated, so no Verus form is offered here.

Evidence. Table VII (p.14) gives the size gap for all 20 protocols: the generated 3D descriptions are 6 lines (TPKT) to 99 lines (ICMPv4), mean 26.2 (Table VI, p.12; 524/20, recomputed from Table VII), while the C that EverParse emits from them is 158 lines (UDP) to 1,208 lines (ICMPv4). The paper’s reading (Appendix C, p.14): “Directly generating, say, 1K lines of C code for an ICMP parser, even if it could be AI-generated, would pose a difficult program verification problem; using a DSL like 3D enables analysis such as symbolic test-case generation to systematically test and refine AI generated code, and correct-by-construction code generation ultimately yields verified C code.” There is no baseline in which GPT-4 writes the C directly, so the size of the benefit is not measured.

Where it fails. The model does not know the DSL: syntax errors are frequent (§V-A.2 says the agents frequently make syntax mistakes), and the paper names bitfield notation, the allowed integer primitives, and reserved words such as type used as identifiers (§V-A.2, p.8). Only formats that 3D can express are in scope; the paper names “tag-length-value” style formats (§II, p.2) and lists full protocol implementation as future work (§VI, p.10).

technique 2: keep a set of candidate specifications and prune it with a growing labeled test set (Algorithm 1)

What it is. A loop with three pieces of state: candidates that type-check, positive inputs, negative inputs. Each round either asks the model for a new candidate or asks the symbolic tool for new inputs; then every candidate that misclassifies any labeled input is removed and the failing pair is fed back to the model.

When to use. When a specification must be derived from prose, an executable oracle can label inputs, and the specification language can be executed on inputs.

How it is done (Algorithm 1 and §III-A, pp.3-4).

1. Inputs: the RFC, a labeling function LblImpl, and seed sets of positive and negative packets, which may be empty.
2. Initialize the state st to the manual, the RFC and the seed tests; the candidate set is empty (lines 1-3).
3. Non-deterministically, query the model with st for a candidate p. Run the type checker. On an error, add the pair (candidate, error) to st and go round again; otherwise add p to the candidates (lines 5-13).
4. Non-deterministically, run the test generator on the current candidates and tests, label the new packets with LblImpl, and add them to the positive and negative sets (lines 14-17).
5. For each candidate and each labeled packet: if a positive packet is rejected or a negative one accepted, add the pair (candidate, packet) to st and remove the candidate (lines 18-26).
6. Return the surviving candidates and both test sets (line 28).

The loop’s guarantee is stated as (§III-A, pp.3-4): “The algorithm returns a set of possible candidate 3D specifications CandProgs, along with an augmented set of positive (I + ) and negative (I − ) packets, generated by 3 D T EST G EN and labeled using LblImpl, ensuring that every specification in CandProgs is consistent with the augmented set of packet inputs.”

The experiments instantiate it more narrowly than the algorithm (§IV-B and §IV-C, pp.6-7): GPT-4-32k at temperature 1.0, 5 candidates per protocol, at most 15 syntax or packet refinements per attempt, and the test set built once up front (one loop iteration seeded with real packets, then 200 generated tests), not regenerated every round.

Verus form. Inference: candidates are alternative spec fn accepts(s: Seq<int>) -> bool definitions (or alternative ensures clauses for one function). Step 3’s checker is running Verus on the file that holds only the specification, which catches syntax, type and mode errors. Step 5 needs a specification that can be run on a concrete input. Verus specification functions are not executed, so either (a) each labeled input becomes a small proof fn whose body asserts accepts(...) or !accepts(...) for that constant input and is given to Verus, or (b) the candidate is paired with an exec fn verified to return exactly accepts, and that function is run on the tests. Form (b) is the paper’s 3DExec; it costs a proof per candidate. What does not carry over: for 3D, executing a candidate is free once it type-checks.

Evidence. See technique 7 for the pass rates, which measure this loop together with the labeler.

Where it fails. The surviving set is consistent with the tests and nothing more; the paper shows wrong survivors (technique 6). The paper also notes that more rounds do not reliably help (§IV-B, p.6): “We observe that allowing more refinement loops within the 3 D G EN agent conversation flow does not always lead to a successful attempt at generating a specification.”

technique 3: three agents split by what each can see

What it is. The model query of Algorithm 1 is a group chat of three agents built on AutoGen, split by what each agent has access to (Inference: so that no agent holds every document).

When to use. When the DSL manual, the domain document and the tool feedback together do not fit one context window; the paper’s model had a 32k-token window.

How it is done (§III-B, pp.4-5).

1. Planner agent: the group chat manager. It holds the task prompt and descriptions of the other two, and it has the ability to invoke the type checker and the executor and to report their results to the other agents.
2. 3D developer agent: writes the DSL. It holds the full manual, task examples and tips on syntax.
3. Domain expert agent: holds the RFC and task examples; it tells the developer what the format requires and critiques the generated description.
4. They converse until the executor reports that the candidate passes the test set, or the user-set iteration limit is reached.
5. A typical exchange: the expert passes the relevant RFC parts; the developer writes a candidate; the planner runs the type checker and reports; the developer repairs.

The stated reason for the split (§III-B, p.4): “We choose to use a multi-agent framework over a single agent, to decompose tasks and reduce overall input in the context window, shielding other agents from unrelated intermediate reasoning steps involved in distinct task refinement loops.”

For long RFCs the authors cut the document by hand to the header-format pages before giving it to an agent; the page counts in parentheses in Table I (p.6) are those extracts, for example TCP 10 of 85 pages and DCCP 14 of 129.

Verus form. Inference: the same split is: one agent with the Verus guide and vstd signatures that writes spec fn, requires and ensures; one agent with the requirement document that says what must hold and reviews the result; one tool-holding coordinator that runs Verus and the tests. Nothing in the split depends on 3D.

Evidence. None that isolates it: there is no single-agent run to compare with.

Where it fails. Figure 2 and §V-A.2 (p.8) show the agents misreading prose: for VXLAN the RFC text does not give the order of the flag bits, only its ASCII diagram does, and the first candidate had the Reserved and I fields in the wrong order; a failing 3DExec test exposed it. The paper’s conclusion from that case (p.8): “Ambiguities in the RFC language may cause the agent to misinterpret the true intent.”

technique 4: turn a combinator-defined specification into a first-order SMT function and ask Z3 for inputs

What it is. 3DTestGen. The meaning of a 3D description is a higher-order F⋆ parser built from combinators. SMT-LIB has no higher-order functions, so the tool inlines the combinators and emits one first-order function per format that maps a parser state to a parser state. A satisfiability query over that function yields a concrete accepted or rejected byte sequence.

When to use. To get test inputs from a specification without writing them by hand, when the specification language is small enough to encode completely.

How it is done (§III-C, pp.5-6).

1. Declare the input as an uninterpreted function from position to value, and assert that every value is a byte:

(declare-fun Input (Int) Int)
(assert (forall ((i Int)) (and (<= 0 (Input i)) (< (Input i) 256))))

2. Define a State record with the remaining input size, the current position, a failed flag, and the return value.
3. Encode each primitive parser as a State-to-State function. For one byte: if the state has not failed and at least one byte remains, return the success state with value Input(current-pos), position plus one, remaining size minus one; otherwise the fail state.
4. Specialize: walk the combinator tree of the format and inline parse_pair, parse_refine and the rest, so that the format becomes nested let and if over the primitive functions. The paper’s example, a struct of two bytes whose first must exceed 42:

(define-fun parse-message ((s0 State)) State
  (let ((s1 (parse-uint8 s0)))
    (if (has-failed s1) s1
      (if (> (return-value s1) 42) (parse-uint8 s1) (fail-state s1)))))

5. Declare an initial state that has not failed and is at position 0; leave its remaining size unconstrained.
6. For a positive test assert (not (has-failed (parse-message init))); for a negative test assert (has-failed (parse-message init)). Run check-sat; read the size and the bytes from the model with eval.
7. Read the answer: SAT gives a packet; UNSAT means the format accepts nothing (or, for the negative query, rejects nothing); UNKNOWN is a timeout.
8. For more tests, add assertions that exclude the models already returned and query again.

The statement of the query (§III-C, p.5): “Given a 3D program p, to obtain positive (resp. negative) test cases, 3 D T EST G EN encodes the semantics of p to Z3 and asks for models of the existential predicate: ”does there exist a sequence of bytes that makes p succeed (resp. fail)”.”

Verus form. Inference: Verus does not hand back Z3 models, so this is not done through Verus itself. The same encoding can be written against Z3 directly for a Verus spec fn that is first-order and non-recursive, which a spec fn accepts(s: Seq<int>) -> bool over a fixed-layout header is. Inside Verus the nearest check is the UNSAT half: a proof fn with ensures forall|s: Seq<int>| !accepts(s) that verifies means the specification accepts nothing, which is a cheap test for a contradictory specification. What does not carry over: recursive spec fn with decreases have no inlined first-order form of bounded size; the paper’s encoding relies on 3D having none that need it, and does not discuss arrays of variable-length elements in the encoding.

Evidence. Cost (§III-C, p.6): “Leveraging the existing semantics of 3D and its compact, structured language of parser combinators, our implementation of 3 D T EST G EN took less than 3 person-weeks and around 2000 lines of F⋆ , OCaml, and SMT2.” Z3 timeouts are reported only as rare, with no count. Packet size is unbounded in the query.

Where it fails. Models returned without further guidance can miss branches: the paper says that with this encoding Z3’s models “may not cover all possible branches” (§III-C, p.6), which technique 5 addresses. The generated tests explore the candidate they were generated from, so a constraint missing from that candidate is never violated by a negative test (§IV-C, p.7): “This gives us some confidence that the generated test suite is diverse, though its completeness is limited by the quality of the specification on which 3 D T EST G EN is executed.”

technique 5: force branch coverage with a branch-trace function

What it is. An extra uninterpreted function names which way each instrumented branch must go; fixing a prefix of it makes Z3 return an input that follows that path.

When to use. When tests from technique 4 must reach every case of a specification.

Steps, from Appendix A (p.12).

1. Choose branches to instrument. The tool does not take all of them: it picks “branches of interest, focusing on those that involve value constraints and casetypes”.
2. Declare a global uninterpreted function branch-trace from index to tag, and add a branch-index field to State.
3. Guard each side of an instrumented branch with its tag, and advance the index when the branch is taken. For the constraint x > 42: the true side requires the constraint and tag 0 at the current index; the false side requires its negation and tag 1.
4. To explore one trace, assert the starting index is 0, assert the chosen tags for the prefix, and assert that the final index is at least the user’s branch depth.
5. Enumerate traces depth-first up to the branch depth, querying Z3 for each.

In the paper’s words: “By querying Z3 while fixing the branch trace, we obtain models of the Input that also are compatible with the trace, i.e., the Input is a byte sequence that forces the parser to follow the branch trace.”

Verus form. Inference: no Verus construct does this, since it needs models. The idea that does carry over is the test-selection rule: one positive and one negative input per value constraint and per match arm of the spec fn, written by hand or by the Z3 script of technique 4.

Evidence. The experiment’s setting (§IV-C, p.7): 200 tests per protocol, the tool configured to fully explore a trace with 100 branch points, at least two examples collected from each branch point; the paper gives ICMP with 82 branches as an example of a large count and says none had more than 100 (§IV-C, p.7). No coverage percentage is reported.

Where it fails. The paper’s own worked example has a slip: it describes one failure as the first byte being “less than 42”, while the format’s constraint is first > 42, so the failing case is 42 or less; §III-C (p.5) likewise says the code “checks that first < 42” directly under code that checks first > 42.

technique 6: differential query between two specifications, which is an equivalence proof when both directions are unsatisfiable

What it is. Ask Z3 for an input that one specification accepts and the other rejects. A model is a distinguishing test. No model in either direction means the two accept exactly the same inputs.

When to use. To choose among candidates that all pass the tests; to compare a generated specification with a trusted handwritten one; to show two differently written specifications are the same.

How it is done (§III-C, p.5).

1. Encode both specifications as in technique 4 over the same Input.
2. Assert that the first succeeds and the second fails; check.
3. Swap and check again.
4. UNSAT once: every packet the first accepts, the second accepts. UNSAT both ways: equivalent. SAT: show the packet to the user together with where the two differ.

The paper’s wording: “If Z3 returns UNSAT for both ways, then the 3D programs p1 and p2 accept and reject the exact same packets: they are semantically equivalent.”

A use rule the paper derives (§V-B, p.9): when one candidate is shown strictly more permissive than another, prefer the stricter. “Thus, a user of 3 D G EN could decide to always accept the stricter specification as a pruning heuristic between candidates.” It rests on two cases (ARP and IPv4) where the stricter one matched the RFC.

Verus form. Inference: this one carries over directly as a proof obligation, without models.

verus! {
// sketch, not machine-checked
spec fn accepts_a(s: Seq<int>) -> bool {
    s.len() >= 2 && s[0] > 42
}
spec fn accepts_b(s: Seq<int>) -> bool {
    s.len() >= 2 && 43 <= s[0]
}
// both directions at once: the two candidates are the same specification
proof fn a_equiv_b(s: Seq<int>)
    ensures accepts_a(s) == accepts_b(s),
{ }
// one direction: a is at least as strict as b
proof fn a_implies_b(s: Seq<int>)
    requires accepts_a(s),
    ensures accepts_b(s),
{ }
}

What changes (inference): when the proof fn fails Verus reports the failed ensures, not a distinguishing input, so the differing input must be found another way (the Z3 script, or an agent proposing one and confirming it with a proof fn that asserts accepts_a(x) && !accepts_b(x) for that constant). A failure can also be an incomplete proof rather than a real difference; Z3’s SAT answer in the paper has no such ambiguity because the encoding is quantifier-free apart from the byte-range axiom.

Evidence, candidates against each other (Table IV, p.9): for 8 protocols with more than one passing candidate, every pair was compared; 7 of the 8 had at least two semantically distinct candidates and 1 (VXLAN) had two equivalent ones. Examples: of 3 ARP candidates, 2 were equivalent and the third added a trailing consume-all field the RFC does not have; of 2 IPv4 candidates, one constrained the 3-bit flags field and the other did not, and no test violated that constraint.

Evidence, against handwritten specifications (Table V and §V-C, pp.9-10): 7 protocols have a handwritten 3D specification by the EverParse authors. 2 of 7 (IPv6, Ethernet) were proved equivalent to the generated one. 3 of 7 (UDP, ICMP, VXLAN) differed because the handwritten one was wrong: a missing constraint on the UDP Length field, an ICMP field that read 32 bytes as 32 bits, and a VXLAN identifier two bytes short; after the fixes the tool proved equivalence, and the fixes were merged into EverParse. 2 of 7 (TCP, IPv4) differed because the generated one lacked constraints that the handwritten one has, although it passed its test set (TCP only with the corrected labels, Table II; IPv4 with Wireshark’s labels).

Where it fails. It compares; it does not say which side is right. Inference: each of the five differences needed a human reading the RFC.

technique 7: label generated inputs with an existing implementation, then audit the labels against the document

What it is. The oracle for technique 2 is Wireshark, run on each generated packet. Where candidates keep failing against the oracle, a human checks whether the oracle or the candidate disagrees with the RFC and corrects the label.

When to use. When a legacy implementation exists and the new specification is meant to follow a document, not to copy the implementation.

How it is done (§IV-C and §V-A, p.7).

1. Collect a few real packets; keep only those the oracle accepts, since real rejected packets “are sometimes arbitrarily malformed”.
2. Run one loop iteration seeded with them to get one candidate; generate 200 tests from it (technique 5); label them with the oracle.
3. Make the oracle judge a bare header: the authors used Wireshark’s Export PDU feature, wrapped TFTP in a dummy UDP header, added dummy payloads for six protocols and disabled checksums.
4. Run the loop (technique 2). For a protocol where no candidate passes, read the failing tests against the RFC.
5. Where the oracle accepts what the RFC forbids, flip the label; then recheck the existing candidates on the corrected set, or restart the loop with it.

The authors’ warning (§I, p.2): “As such, we caution that 3 D G EN should not be used to blindly match the behavior of a legacy tool.”

Verus form. Inference: for an agent writing a Verus specification of an existing Rust function, the legacy implementation is the labeler: run it on generated inputs and require the candidate ensures to hold on each observed input and output pair, by executable assertion or by a constant-input proof fn. The paper’s lesson is the second half: a disagreement is first a question about which side is wrong, and the answer comes from the requirement document.

Evidence (Table II, p.8; GPT-4-32k, temperature 1.0, 5 attempts per protocol, at most 15 refinements per attempt).

• With Wireshark’s labels: at least one of 5 attempts passed for 9 of 20 protocols (45%). All 5 passed for 2 of 20 (UDP, IGMP). Summing the Accepted column gives 23 passing attempts of 100 (5+2+2+1+3+3+1+5+1).
• With labels corrected by two authors: at least one candidate passed for all 20 of 20.
• For all 11 failing protocols the authors attribute the failure to the labeler (§V-A, p.7): “We investigate the cause of the errors and find in all cases that 3 D G EN generates a specification that is consistent with the header format described in the RFC, but that Wireshark labels packets as valid despite there being constraint violations, i.e., Wireshark does not fully enforce the RFC.” Table III (p.9) lists 20 unenforced constraints over those 11 protocols; Wireshark gave a warning for 3 of them and none for 17.
• Cost in refinements, averaged per protocol (Table II): syntax refinements from 0.3 (UDP) to 14.25 (DCCP); packet refinements from 0 (UDP, DHCP, IGMP) to 12 (RTP).

Where it fails.

• The corrected labels come from two of the authors who built the system, using the RFC as a guide (§V-A, p.7). Inference: the 20 of 20 figure is therefore not an independent measurement.
• Passing corrected tests still left TCP and IPv4 under-constrained (technique 6).
• Setting up the oracle was costly (§IV-C, p.7): “As such, using Wireshark as a labeler for 3 D T EST G EN outputs involved a non-trivial effort.”

technique 8: generate the tests from a reference specification to surface constraints the oracle’s tests never exercise

What it is. When a trusted specification exists, run the test generator on it, not on the candidate, so that each of its constraints has a negative test.

How it is done (§V-C, p.10). For IPv4 the generated specification lacked constraints on IHL, TotalLength and Options. The authors generated positive and negative tests from the handwritten specification and reran the loop with them.

Evidence. One protocol. With those tests the system produced two passing specifications “after an average of 11 syntax and 4 packet refinements”, both proved equivalent to the handwritten one (§V-C, p.10).

Verus form. Inference: this is the case of porting or re-deriving a specification when a reference model exists; the reference spec fn is the source of tests and the target of the equivalence proof fn of technique 6. It gives nothing when no reference exists, which is the usual case for new code.

Where it fails. It presupposes the answer. The paper presents it as a check of what better tests would allow, not as a method for new formats.

inconsistencies in the paper

• pass@5 has two meanings. §IV-B (p.6) defines it: “We report a pass@5 metric, which counts the number of successful generations out of 5 runs.” The 45% in §V-A and Table II is the share of protocols with at least one success (9 of 20). By the definition’s count the rate is 23 of 100 attempts.
• The refinement averages are said to be “across all attempts” (§V-A, p.7), with 5 attempts per protocol, yet UDP’s 0.3, ICMP’s 7.5 and DCCP’s 14.25 and 0.75 are not multiples of one fifth. The denominator of these averages is not given.
• §IV-B sets “the max number of syntax or packet refinements to 15 per attempt”. If that is one cap on both kinds together, Ethernet’s averages (11.4 + 4.6 = 16) and OSPFv3’s (13.6 + 2 = 15.6) exceed it; the paper does not say whether the cap is per kind.
• Table III’s caption says its rows are RFC constraints Wireshark does not enforce, but the text on IPv6 (§V-A.1, p.8) describes the opposite direction: Wireshark rejects packets the generated specification accepts, because it validates the encapsulated next layer and the RFC section does not.
• Appendix B (p.12) says the IPV6 and TCP generated specifications are missing constraints; Table V and §V-C (pp.9-10) say IPV4 and TCP, and report IPV6 as equivalent.
• The first > 42 example is described as first < 42 twice (technique 5).
• Table VI (p.12) checks against Table VII (p.14) for the seven protocols with handwritten specifications: lines 232/7 = 33.14 generated against 420/7 = 60 handwritten; constraints 28/7 = 4 against 36/7 = 5.14. The 0.42 for casetypes and enums is 3/7 truncated, not rounded.

what was already done, which VL should not redo

• The loop of generate, type-check, test, prune, with tool errors fed back, for a specification language, including multi-candidate bookkeeping (technique 2).
• Using a both-directions satisfiability query to cluster candidate specifications and show a human one distinguishing input per cluster (technique 6).
• The finding that a legacy implementation is a poor oracle for a standard: 11 of 20 protocols here.
• Not done by the paper, by its own statement: a user study (§VII, p.10), retrieval over long RFCs (the cutting was manual, §IV-A, p.6), and anything beyond the parser.

threat to VL

Inference: low as a competitor, high as a precedent. It is a 2024 result with GPT-4-32k, limited to header formats of 6 to 99 lines of DSL, and its output is C through F⋆, not Rust. Its argument, though, is against the approach of having agents write proofs for general code: restrict the agent to a DSL where one proof covers every program. For any domain that has such a DSL (parsers, serializers), a product that has agents write Verus proofs per function is doing more work for the same guarantee. The part of the paper a Verus product most needs and lacks an equivalent for is techniques 4 to 6: an automatic source of inputs that separate two candidate specifications.

techniques for the catalog

• DSL as the agent’s output language — have the agent write a small declarative language with a checker, an executor and a verified compiler, and never the final code
• candidate-set refinement loop — keep all type-correct candidate specifications, grow a labeled test set, drop every candidate that misclassifies a test and feed the failing pair back
• three agents by visibility — a tool-running planner, a developer holding the language manual, and a domain expert holding the requirement document, so no context holds everything
• combinator-to-first-order SMT encoding — inline parser combinators into one state-to-state function per format and ask Z3 for an input that makes it succeed or fail
• branch-trace instrumentation — add an uninterpreted trace of branch tags to the encoding and enumerate traces depth-first to get one input per path
• two-way differential query — an input accepted by one specification and rejected by the other is a distinguishing test; unsatisfiable both ways is an equivalence proof
• prefer the stricter candidate — when one surviving candidate is proved to accept a subset of another, take the stricter one (supported by two cases only)
• legacy implementation as labeler, audited — label generated inputs with an existing tool, and on persistent disagreement decide from the document which side is wrong and correct the label
• tests from a reference specification — generate positive and negative inputs from a trusted specification so every one of its constraints is exercised

Last edited: 2026-10-13