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.

Software Engineering (cs.SE); Artificial Intelligence (cs.AI)

I.2.3; I.2.7; D.2.4

arXiv:2610.14552 [cs.SE]

(or arXiv:2610.14552v1 [cs.SE] for this version)

https://doi.org/10.48550/arXiv.2610.14552 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.