LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies

Abstract

Protocol specifications rarely justify executable behavior in one place: a transition may inherit its source state from a remote control block, name its events only by number, and remain subject to a later correction. Recovering the nearby clause is therefore insufficient; the system must assemble a source-linked certificate and determine whether any stronger rule applies. We introduce LASER, a proof-carrying search method for sparse, defeasible protocol evidence. LASER represents missing support and unresolved corrections as explicit obligations, searches typed evidence routes, and lets an occurrence-aware symbolic checker alone decide whether a certificate warrants, refutes, or leaves a behavior unresolved. On 91 BehaviorCheck families under a matched 2K budget, LASER improves Joint Edge+Proof over the strongest local reader on two model families ($\Delta=+.132$, $p=.017$; $\Delta=+.198$, $p<.001$) while cutting false discoveries by 2--3$\times$. Controlled replays attribute the gain and its limits: neither reference routing nor deterministic citation expansion alone exceeds the local baseline; whole-document reading (29--65K tokens), two-round iterative retrieval, and even oracle minimal-certificate evidence all fail to reach LASER, localizing the bottleneck in typed obligation closure rather than evidence access. An authority-corruption replay shows source-link errors only cause abstention, while the only unsafe-warrant mechanism is mis-recording a Held erratum as Verified, confined to that erratum's family. LASER thus improves long-range dependency recovery while converting incomplete evidence and uncertain authority into explicit residual obligations rather than unsupported behavior.