Refine2Diff: Detecting Protocol Specification–Implementation Inconsistencies via Specification-Driven Code Refinement

Abstract

Detecting specification–implementation inconsistencies is critical and fundamentally challenging due to the semantic gap between natural-language specifications and executable code. Existing approaches often require substantial manual effort to translate specification requirements into formal properties for verification or testing. While recent LLM-based methods have shown promise in automating this process, they suffer from hallucination and unreliable reasoning, producing false positives. To address these limitations, we present Refine2Diff, a novel framework for automatically detecting and validating specification–implementation inconsistencies in network protocols. Rather than relying solely on a direct binary judgment from an LLM, we use the specification as an instruction to refine the implementation, thereby exposing inconsistencies through observable behavioral differences between the original and refined implementations. Specifically, Refine2Diff performs context-aware refinement to construct a reference implementation and supports refinement-guided PoC generation by deriving preconditions that trigger behavioral differences and satisfying them through specification-guided mutation. We evaluate Refine2Diff on 10 real-world implementations spanning six network protocols. For inconsistency detection, Refine2Diff achieves a precision of 0.84 (1.4× higher than the strongest baseline), improving further to 0.98 after the PoC-based confirmation. For PoC generation, Refine2Diff achieves an 82% success rate, outperforming all baselines by 3×–9× while requiring up to 5.7× fewer executions. In total, Refine2Diff uncovers 30 previously unknown inconsistency bugs, 22 confirmed by developers.