SPAR’s Adversarial Loop

SPAR turns the testable model into a refinement mechanism. It begins with RFC text, produces a formal format and a reference parser as separate interpretations, and then uses each artifact to challenge the other. The focus here is the causal loop: how a packet exposes a mismatch, how related RFC context is selected, and why reaching a fixed point means consistency under tested cases rather than proof of every protocol behavior.

Start with the RFC, not the deployed implementation

A deployed parser is tempting as a starting point because it already contains executable logic. But using it as the specification would make it difficult to find a missing rule. If the implementation accepts a packet that violates the RFC, an inference method built entirely around that implementation may learn the omission as if it were intended behavior.

SPAR instead starts with structured RFC documents. The paper describes an initial divide-and-conquer process over the RFC’s section tree. Smaller sections are interpreted into pieces of a packet format and pieces of a parser, then those pieces are merged into complete artifacts. The approach gives the language model manageable portions of the source and preserves a trace from generated elements back to the sections that supplied them.

The initial artifacts are not assumed to be correct. The paper’s Babel example makes that explicit: the first formal format can omit the relationship between AE and Omitted, even though the reference parser may contain the corresponding check. The omission is not a reason to treat the whole initial format as useless. It is a reason to put the two interpretations into a process where their differences can become evidence.

The section tree supplies an important kind of ownership. A field or type is not merely generated; it is associated with the part of the RFC that described it. When several small interpretations are merged, that association gives the later refinement step somewhere to look. If a mismatch involves a length condition, the system can revisit the section that introduced the length and then follow any type or field dependency that determines how the length is computed. Without that trace, refinement would have to guess which parts of a long document might explain the discrepancy.

Merging also creates a distinction between composition and correction. The initial format is assembled from local pieces so that the LLM does not need to hold every protocol detail in one prompt. The later loop can then challenge a particular piece without throwing away the entire structure. This is useful for the Babel case: the Update layout can remain intact while the relationship between AE and Omitted is reconsidered. A local repair is not guaranteed to be correct, but it is easier to compare with the relevant source and less likely to disturb unrelated fields.

The same traceability applies to the reference parser. A parser fragment generated from a section can be exercised by packets whose constraints came from the corresponding format fragment. If the two fragments disagree, the mismatch is not only a runtime fact; it is a pointer to the source relationship that needs review. This does not remove ambiguity from natural-language RFCs. It makes the ambiguity visible at the boundary where it affects a concrete packet decision.

There is one bibliographic distinction worth keeping separate from the protocol mechanism.