LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies

Zihan Tang; Huibiao Zhu

cs.SEOct 10, 2026

LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies

Authors: Zihan Tang, Huibiao Zhu

Organizations: Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China

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 ( $Δ=+.132$ , $p=.017$ ; $Δ=+.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.

Figures & tables

Figure 1: Local evidence versus certificate closure.

Figure 2: Sparse obligations behind a warranted edge.

Figure 4: Learned search ordering with checker-exclusive warrant.

Local context
Reader	Edge recovery					Proof quality			Decision
	P	R	$F_{1}$	Macro $F_{1}$	Exact	Evid. $F_{1}$	nDCG	Joint	FDR $\downarrow$	Abstain
Previous context	.647	.219	.327	.302	.297	.406	.412	.220	.353	.538
BM25 + source neighbors	.581	.285	.382	.313	.308	.486	.474	.242	.419	.462
Occurrence-centered context	.582	.258	.358	.374	.363	.559	.554	.308	.418	.407
Long-range evidence routing

Table 1: Behavior recovery under a matched 2K evidence budget.

Figure 5: Component ablation and evidence-budget response.

Removed component	Evaluation	$\Delta$ correct/closed	$\Delta$ expansions	Safety effect
Proof paths	25 applicable errata	$-25$ Closed@1	$+0.87$	No unsafe change
Checker feedback	277 controlled routes	$0$	$0.00$	0/167 false routes
Diverse beam	277 controlled routes	$0$	$0.00$	0/167 false routes
Validated union	277 controlled routes	$0$	$+0.18$ path; $+0.90$ atomic	0/167 false routes
Authority checking	20 paired families	$-16$ correct claims	N/A	$+8$ unsafe warrants

Table 2: Removal ablation across controlled evaluations.

Dependency regime
Slice	$n$	Edge $F_{1}$			Exact match		Joint Edge+Proof
		Local	LASER	$\Delta$	Local	LASER	Local	LASER
Remote reference	28	.025	.726	+.701	.000	.643	.000	.321
Local route	63	.579	.688	+.109	.444	.587	.349	.460
Protocol
BGPv4	52	.188	.780	+.592	.173	.692	.096	.404

Table 3: Behavior recovery by dependency regime and protocol.

Routing	Expansion	Edge $F_{1}$	Joint	Remote $F_{1}$
Local	off	.382	.242	.025
Local	on	.382	.242	.025
Reference	off	.396	.253	.054
Reference	on	.700	.407	.719

Table 4: Attributing the remote-reference gains by replaying frozen completions through the same checker. Neither deterministic citation expansion without routing nor routing without the typed expansion closes remote references; the gain requires both components. Remote column: Edge F1 on the 28 reference-required families.

Method	$\Delta$ Joint	CI95	$p$	$\Delta$ Edge
Hybrid	+0.132 ∗	[0.033,0.231]	0.017	+0.256
Cue-gated	+0.110	[-0.011,0.220]	0.096	+0.230
Reference	+0.099	[-0.011,0.209]	0.121	+0.244
Expansion only	-0.066	[-0.143,0.011]	0.182	-0.061
Routing only	-0.055	[-0.132,0.022]	0.262	-0.023

Table 5: Family-paired LASER variants and attribution arms against the strongest local reader (occurrence-centered) on Joint Edge+Proof, 20,000 bootstrap and permutation rounds, family as the unit (

n{=}91

);

p

: two-sided permutation test,

{}^{*}p<0.05

Protocol	Fam.	Fired	Req.	Prec.	Rec.
BGPv4	52	52	25	.48	1.00
DCCP	8	1	2	1.00	.50
TCP	31	0	1	.00	.00
All	91	53	28	.49	.93

Table 6: Public cue-gate transfer audit; Req.: reference required, Prec./Rec.: cue precision/recall. The gate is a fixed, prediction-blind pattern test; gold is used only to evaluate it. It misses two required references (one DCCP and one TCP complement variant) and over-fires on BGPv4, where reference routing never removes a correct local edge.

Reader (GLM-5.3, $n{=}91$ )	Evidence	Edge $F_{1}$	Joint	Exact	$\Delta$ Joint	$p$
Iterative retrieval (2 rounds)	2K	.264	.176	.242	-0.099	0.065
Direct-full (whole document)	29–65K	.276	.209	.253	-0.066	0.240
Local BM25 + source neighbors	2K	.406	.275	.319	+0.000	1.000
Occurrence-centered (strongest local)	2K	.447	.275	.352	—	—
Oracle certificate evidence	$\leq$ 2K	.496	.330	.407	+0.055	0.474
LASER (reference)	2K	.799	.484	.626	+0.209	$<$ .001

Table 7: Full second-model replication on GLM-5.3 (all 91 families; same prompt, checker, and 2K budget).

\Delta

Joint and

p

are family-paired against the strongest local reader. Whole-document reading, two-round iterative retrieval, and even oracle minimal-certificate evidence do not reach LASER: the bottleneck is typed obligation closure, not evidence access. Oracle uses private certificate evidence for selection only.

Corruption	Records	Unsafe	Lost
Held $\rightarrow$ Verified	8	16	0
Verified $\rightarrow$ Held	12	0	24
RFC binding corrupted	20	0	24
Stale text corrupted	20	0	24

Table 8: Joint authority/source-link corruption replay on the 20-family sealed authority suite (40 claims). Clean replay reproduces all 40 expected labels. Unsafe: unsafe warrants; Lost: lost closures. Source-link and binding corruption never creates an unsafe warrant; it degrades to Unknown . Mis-recording a Held erratum as Verified is the only unsafe-warrant mechanism, and it affects exactly the corrupted family.

Window	Warranted	Edges	Edge $F_{1}$	Joint
$\pm$ 64/32	59	92	.667	.418
$\pm$ 128/64	67	121	—	—
$\pm$ 192/96	68	122	.799	.484
$\pm$ 384/192	None	None	.799	.484
$\pm$ 768/384	68	122	—	—
no aliases	68	122	.799	.484

Table 9: Occurrence-checker sensitivity replay over frozen GLM completions; the deployed window is

\pm

384/192. Results saturate at

\pm

192/96 and are unchanged by the alias table or a doubled window; halving the window to

\pm

64/32 loses recall while keeping precision (.880), i.e., degradation is conservative.

Figure 6: UPPAAL model and verification workflow.

Evaluation	Metric	Comparator	LASER
Applicable errata	Closed@1	0/25	25/25
	Mean expansions	1.87	1.00
Unresolved errata	Unsafe warrant	0/6	0/6
Authority claims	Correct claims	38/40	40/40
	Correct pairs	18/20	20/20
Held authority	Unsafe warrant	0/8	0/8

Table 10: Outcomes beyond BehaviorCheck.

Explore similar work

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
Jul 30, 2026Ruslan KhrulevAutomated Theorem Proving Interactive Theorem Proving
Lomonosov Moscow State University
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
May 22, 2026Matthias Cosler, Cas Cremers, Bernd Finkbeiner +2Reinforcement Learning Automated Theorem Proving
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany · Technical University of Munich, Munich, Germany
ClaimReceipt: Verifying Evidence Sufficiency and Coverage in Agent Evaluations
Sep 2, 2026Peiying Zhu, Sidi ChangClaim Verification Data Provenance
Blossom AI Blossom AI Labs San Francisco, CA, USA

Jul 30, 2026J/K move · Enter open · S save

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Ruslan Khrulev

Lomonosov Moscow State University

Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Open paper AskPDF arXiv

LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.

Abstract

Explore similar work

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin

ClaimReceipt: Verifying Evidence Sufficiency and Coverage in Agent Evaluations