{"id":"8b869d33-f5ae-4303-a1fc-e300c302a895","arxiv_id":"2508.21302","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"Locus uses an LLM agent to synthesize and validate intermediate predicates that make directed fuzzing reach target bug states faster, reporting an average 41.6x speedup across eight fuzzers.","lead":"Locus is a framework that writes semantic checkpoints into programs so directed fuzzers can stop early and reach target bugs faster. On the Magma benchmark, it reports large time-to-exposure speedups across eight fuzzers, but it ships no code and its safety guarantee is explicitly limited.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Semantic validation via bounded KLEE is incomplete, so the central admissibility guarantee can fail; a missed ¬φ∧ψ path would let early termination reject canary-reaching executions and inflate TTE speedups.","rationale":"The reader's weakest assumption correctly identifies the semantic validator's incompleteness as the central risk. My independent reading reaches the same point: the paper's formal admissibility argument (Theorem 1) is conditional on predicates being true relaxations, and the only mechanism establishing that is bounded symbolic execution, which the paper explicitly disclaims in Section 6. This concern is load-bearing because the headline speedups are measured as TTE improvement, and if a predicate is not a relaxation, early termination can reject executions that would have reached the canary, making the instrumented program faster precisely by being unsound. The suggested concrete test is feasible because Magma provides known triggering inputs, and it would empirically falsify the admissibility claim for any predicate that rejects such an input. I do not think this forces a different verdict from CONDITIONAL: the empirical results are extensive and the limitation is disclosed, but the central guarantee remains unverified. Thus the correct action is to keep the reader's CONDITIONAL verdict and require the proposed audit before accepting the speedup claims at face value.","tokens_in":25887,"tokens_out":3822,"duration_ms":41737,"concrete_test":"For each Magma vulnerability, execute the known triggering input (Magma PoC or any input known to reach the canary in the original binary) under the Locus-instrumented binary P'. If any such input is rejected before the canary by an inserted predicate, the validator is unsound for that predicate and Theorem 1 is violated. This directly tests whether the relaxation guarantee holds on the exact ground-truth inputs that define TTE.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing premise is that every synthesized predicate is a relaxation of the canary (Def. 3, Thm. 1). The semantic validator (Sec. 3.4) checks this by running KLEE on a Chopper-pruned CFG from ¬φ to ψ; absence of a found path is treated as proof that φ relaxes ψ. This is an incomplete decision procedure. KLEE's loop unrolling and path exploration are bounded, and Chopper pruning removes nodes not statically reachable, which can drop alias- or indirect-call-dependent flows. If a real execution reaches ψ but violates φ earlier, the inserted early exit terminates it in P' while P would reach ψ, so fuzzing admissibility fails exactly along the dimension that reduces TTE. The paper concedes this in Sec. 6 ('we cannot formally guarantee that the relaxation... is always valid'). Because many headline numbers are ratios where baseline times out at 24h, an unsoundly terminating predicate can masquerade as a large speedup without any progress toward the canary. This does not require the LLM to be wrong; it is a property of the validation oracle.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Locus, an LLM-agent-based system that synthesizes predicates at arbitrary program points to guide directed fuzzing toward a given target state (canary). The synthesized predicates are validated by compilation and by KLEE-based symbolic execution to ensure they are 'strict relaxations' of the canary, enabling early termination of executions that cannot reach the target. The framework is fuzzer-agnostic and is evaluated on the Magma benchmark with eight fuzzers, reporting large average TTE speedups (e.g., 70.3x for directed fuzzers) and seven newly discovered bugs.","tokens_in":26192,"tokens_out":6536,"duration_ms":68455,"significance":"The core idea—synthesizing semantic milestones at arbitrary program points via an LLM agent, then validating them before deployment—is novel and practically relevant. The evaluation is unusually broad: eight fuzzers, ten vulnerability classes, ten trials per setting, and statistical tests. The discovery of previously unpatched bugs in well-fuzzed targets (VLC, libarchive, libming) lends credibility to the practical value of the approach. The paper also ships a detailed cost analysis. However, the central theoretical guarantee (fuzzing admissibility via absolutely reliable predicate relaxation) is not soundly established, and the headline speedup numbers are affected by the treatment of timeouts. The contribution would remain significant if reframed as a best-effort, empirically successful guidance mechanism with a clearly bounded validation oracle.","major_comments":[{"comment":"The semantic validator is not a sound decision procedure for the relaxation property, so Theorem 1's premise is not established. KLEE explores with loop-unrolling and path limits, and the Chopper-style CFG pruning can drop alias- or indirect-call-dependent paths. The paper itself concedes in §6 that 'we cannot formally guarantee that the relaxation brought by the generated predicates is always valid.' This is load-bearing because an invalid predicate that fails to reject a canary-reaching execution (i.e., a missed ¬φ ∧ ψ path) would violate fuzzing admissibility and could inflate TTE improvements without making progress toward the canary. Please either provide a sound (even if conservative) validation method, or explicitly reframe the guarantee as empirical and quantify how often validation is inconclusive.","section":"§3.4 and §6"},{"comment":"The formalization does not connect Definition 3 to the actual instrumentation semantics. Definition 3 states a pointwise implication ψ(s) ⇒ φ(s), but φ is evaluated at a different program point than ψ; the required property is path-based: every execution that reaches ψ must have φ true at the instrumented point. As written, Theorem 1 does not follow from Definition 3 because the state s is ambiguous. The validation in §3.4 checks path feasibility between ¬φ and ψ, which is closer to the correct property, but the paper's formal apparatus should be aligned with that operational meaning.","section":"§3.1, Def. 3 and Thm. 1"},{"comment":"Timeouts are recorded as the 24h cap and treated as exact TTE when computing speedup ratios. For baseline timeouts this is conservative, but for Locus timeouts (e.g., SSL001 in Table 3, ratio 0.9) it overstates Locus's performance, because the true TTE is >24h and the ratio would be smaller. The reported averages also exclude rows where both sides time out, changing the comparison population. The headline speedups (70.3x, 41.6x, etc.) therefore mix censored and exact observations in a way that biases the results. Please report censored outcomes separately, use survival analysis, or provide a sensitivity analysis with conservative bounds (e.g., treating all timeouts as >24h and computing worst-case ratios).","section":"§4.1 and Tables 2/3"}],"minor_comments":[{"comment":"The abstract reports 'eight previously unpatched bugs,' while Section 4.5 and Table 7 list seven and the conclusion says 'seven.' Please reconcile these numbers.","section":"Abstract vs. §4.5/Table 7 vs. Conclusion"},{"comment":"The diff snippet shows 'if (a > b) EXIT 0;' which exits when the predicate is true. The text (and Algorithm 1) says early exit occurs when the predicate is not satisfied. The figure appears to have inverted polarity and should be corrected.","section":"Figure 2"},{"comment":"Theorem 2 uses φ′ for the canary, which is confusing and inconsistent with the rest of the paper (the canary is ψ). Please rewrite the statement with consistent notation.","section":"Theorem 2"},{"comment":"The Ensure line says 'target-conditional equivalent program,' but the paper only argues for fuzzing admissibility, not program equivalence. The header should match the weaker property.","section":"§3.3, Algorithm 1 header"},{"comment":"The phrase 'strictly relaxes' does not match Definition 3, which is an ordinary implication (non-strict relaxation). If a strict version is intended, it should be defined.","section":"§3.4"}],"recommendation":"major_revision","confidential_remarks":"The paper is a strong empirical systems contribution with a useful framework, but the formal guarantee is overstated and the TTE analysis needs rework. I see the issues as fixable within the manuscript's scope: weaken the 'ensures' language, make the validation caveat prominent in the contribution claims, and re-analyze the timeout data. The new-bug findings are a plus, but they do not compensate for the unsoundness of the central admissibility claim."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core idea is genuinely new: instead of asking an LLM to generate inputs or harnesses, Locus has an agent synthesize boolean predicates at arbitrary program points, validated (as best it can) to be preconditions of the canary. That shifts the LLM task to a more local, checkable form, and the refinement loop that moves predicates earlier in the call chain is clever. The evaluation is extensive: eight fuzzers, Magma, ablations, cost, and a case study showing the agent can synthesize a more precise canary than the ground truth. The 27/28 patch-to-canary translation result is also a nice sanity check.\n\nThe soft spots are real but not fatal. The formal claim that every predicate 'strictly relaxes' the canary rests on a bounded KLEE check after Chopper-style pruning. The paper's own Section 6 concedes this is not a formal guarantee, so Theorem 1 is conditional on a heuristic oracle. That is not disqualifying for a fuzzing paper, but the write-up should not present it as a proof. Also, the evaluation omits the closest prior predicate-based approaches (FuzzFactory, CAFL, T-Fuzz); comparing against those would sharpen the claimed novelty.\n\nOne concern from my reading is actually the opposite of the usual timeout complaint: treating 24h timeouts as exact TTE for the baseline is conservative, because the true baseline TTE is larger, so the speedup ratios are lower bounds. The paper says this correctly. The bigger interpretive risk is that a predicate that is unsound in a way that rejects some canary-reaching paths could make TTE better or worse depending on which paths get pruned; the per-vulnerability p-values do not address that.\n\nMinor: abstract says eight new bugs, conclusion says seven; Table 7 lists seven. Needs cleanup.\n\nOverall: this deserves peer review. The engineering and evaluation are solid enough to stand as a systems paper, with the formal framing softened and a comparison to existing predicate-injection methods added. I would not desk reject it.","headline":"Locus is a promising engineering contribution that automates intermediate predicate synthesis for directed fuzzing, but the formal admissibility guarantee is not actually delivered, and the evaluation would benefit from missing baselines and an artifact.","tokens_in":26641,"tokens_out":2986,"would_cite":true,"duration_ms":29496,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Locus claims that verified progress predicates—guards that safely terminate executions which cannot reach a target bug—produce average 70.3x speedups for directed fuzzers and 13x for coverage-guided fuzzers.","keywords":["directed fuzzing","predicate synthesis","symbolic execution validation","LLM agents","program instrumentation","fuzzing admissibility","vulnerability canary","early termination"],"falsifier":"Take one of the accepted predicates and symbolically explore all entry-to-canary paths with a bounded number of loop iterations; if any path satisfies the canary but violates the predicate, the validator's no-counterexample verdict was an artifact of pruning. Concretely, for a known crashing input, instrument the program with the predicate and run it: if the instrumented run exits before the canary, the predicate is not a relaxation and the fuzzing-admissibility guarantee fails.","tokens_in":25836,"feed_emoji":"🎯","tokens_out":9741,"duration_ms":93659,"temperature":0.7,"pith_summary":"Locus is built around a simple guarantee: if a synthesized predicate is a strict relaxation of the vulnerability canary, meaning every execution that reaches the vulnerable state also satisfies the predicate, then terminating executions that violate the predicate can never discard an input that would have found the bug. The paper argues that existing directed-fuzzing feedback, such as branch distances or hand-written input constraints, is too coarse or too specialized, and that an LLM-based agent with code-navigation tools can synthesize better milestone predicates at arbitrary program points, then iteratively push them earlier in the program. A validator compiles each candidate, prunes the control-flow graph, and runs symbolic execution to search for a path that violates the predicate yet satisfies the canary; if none is found, the predicate is accepted. On a published benchmark of real-world vulnerabilities across eight fuzzers, the paper reports that instrumenting with these predicates reduces time-to-exposure by 70.3x on average for directed fuzzers and 13x for coverage-guided fuzzers, and that the approach has surfaced several previously unpatched bugs. If correct, this turns directed fuzzing from a search over raw inputs into a search guided by semantically meaningful intermediate states, and it makes LLM-suggested code usable because every suggestion is checked before deployment.","feed_headline":"Validated predicate guards speed directed fuzzing by 70x","feed_subtitle":"Early-exit milestones checked by symbolic execution help fuzzers reach target vulnerabilities faster.","key_machinery":"The central object is the progress-capturing predicate, a boolean condition over program state placed at an arbitrary program point, required to be a strict relaxation of the canary: whenever the canary holds, the predicate also holds. A canary is an explicit predicate that is true exactly in the vulnerable program state. The carrying mechanism is an agentic synthesizer-validator loop: the synthesizer localizes a candidate function, generates the predicate, and iteratively propagates it toward the program entry, while the validator checks syntactic correctness by compiling and semantic correctness by symbolic execution over a pruned control-flow graph, searching for a counterexample path whe","core_discovery":"The paper's central claim is that progress toward a target bug can be represented as a sequence of predicates that dominate all paths to the canary, and that such predicates can be synthesized automatically and verified before use. Formally, a predicate is admissible when it is a strict relaxation of the canary: for every state, canary true implies predicate true. The instrumented program is then fuzzing admissible to the original program, meaning it never rejects an input that would have reached the vulnerability. Synthesis is done by an agent that reasons about the canary, localizes candidate functions, generates predicates, validates them, and iteratively refines placement toward the prog","pith_inferences":["The practical soundness of the whole approach rests on how thoroughly the symbolic validator explores paths: if chopping or loop unrolling causes it to miss a violating path, early termination could silently discard an input that reaches the target, and the reported time-to-exposure gains would be partially an artifact of that bias.","The relaxation-checked predicate machinery could be reused beyond fuzzing, for example as runtime guards in production that are only deployed after proving they cannot reject inputs reaching a critical state, or as filters that discard test cases guaranteed not to exercise a target.","Because refinement pushes predicates toward the entry while preserving meaning, the validated predicates may double as human-readable documentation of the deep precondition chain guarding a bug, which could aid debugging and patch review even when fuzzing is not the goal.","A natural next experiment is to compare accepted predicates against exhaustive bounded verification on small programs to measure the validator's miss rate, and to test whether pushing every predicate to the earliest possible program point is always beneficial relative to the added runtime overhead of evaluating it."],"forward_implications":["Any fuzzer can be accelerated without modifying the fuzzer itself, because Locus's source-level instrumentation is agnostic to fuzzer implementation and is a one-time offline cost.","Coverage-guided fuzzers also benefit, because synthesized predicates add extra coverage feedback and early-exit guards, not just distance signals.","The strict-relaxation property makes early termination safe in principle: no validated predicate rejects an input that would have reached the target canary.","Predicates can be refined backward toward the program entry, letting invalid inputs be rejected earlier and increasing the effective number of mutations per unit time.","Canary conditions can themselves be generated from security patches and static-analysis alerts, extending the approach beyond pre-defined target states; the paper reports that 27 of 28 tested patches were translated correctly, with one case producing a more precise canary than the manually written one."],"supporting_citations":[{"why":"Supplies the ground-truth vulnerability canaries and benchmark protocol that Locus's main evaluation uses to measure time-to-exposure with and without instrumentation.","marker":"[32]"},{"why":"Defines the distance-guided directed-fuzzing baseline that Locus instrumentations are integrated with and accelerate.","marker":"[6]"},{"why":"Directed fuzzer with selective path exploration used as a baseline and integration target; Locus reports its largest speedup on it.","marker":"[56]"},{"why":"Directed fuzzer with path pruning included as a baseline; its early-termination concept is closely related to Locus's guards.","marker":"[35]"},{"why":"Multi-target directed fuzzer included as a baseline to show the generality of Locus's improvements.","marker":"[36]"},{"why":"Coverage-guided fuzzer used as a baseline, demonstrating that Locus also accelerates non-directed fuzzers.","marker":"[27]"},{"why":"Symbolic execution engine used by the semantic validator to search for counterexample paths to the relaxation claim.","marker":"[7]"},{"why":"Chopped symbolic execution strategy used to prune the control-flow graph so validation avoids exploring irrelevant paths.","marker":"[82]"},{"why":"Static value-flow analysis used for lightweight reachability analysis and for generating canaries from static-analysis alerts.","marker":"[80]"},{"why":"Reasoning-and-acting pattern that underlies the agent's tool-use loop for iterative predicate synthesis and refinement.","marker":"[97]"}],"fun_headline_variants":["Agentic predicates as milestones speed directed fuzzing 42x","Synthesized predicate milestones lead fuzzers to bugs faster","Guaranteed-safe predicates accelerate directed fuzzing","Agent-synthesized guard predicates speed up bug finding"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The guarantee that a predicate is safe rests on the validator's ability to search all relevant execution paths: if that search misses a path that reaches the target despite violating the predicate, early termination could wrongly discard a bug-finding input.","fun_headline_variants_meta":{"raw":{"variants":["Agentic predicates as milestones speed directed fuzzing 42x","Synthesized predicate milestones lead fuzzers to bugs faster","Guaranteed-safe predicates accelerate directed fuzzing","Agent-synthesized guard predicates speed up bug finding"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000433,"raw_usage":{"total_tokens":2070,"prompt_tokens":797,"completion_tokens":1273,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":541,"completion_tokens_details":{"reasoning_tokens":1205}},"tokens_in":541,"tokens_out":1273,"duration_ms":9604,"temperature":1.0,"reasoning_tokens":1205,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T14:24:41.601749+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take one of the accepted predicates and symbolically explore all entry-to-canary paths with a bounded number of loop iterations; if any path satisfies the canary but violates the predicate, the validator's no-counterexample verdict was an artifact of pruning. Concretely, for a known crashing input, instrument the program with the predicate and run it: if the instrumented run exits before the canary, the predicate is not a relaxation and the fuzzing-admissibility guarantee fails.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Directed fuzzer with selective path exploration used as a baseline and integration target; Locus reports its largest speedup on it."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Chopped symbolic execution strategy used to prune the control-flow graph so validation avoids exploring irrelevant paths."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Static value-flow analysis used for lightweight reachability analysis and for generating canaries from static-analysis alerts."}],"review_version":1}