{"id":"91dc7402-ac88-47d8-b424-b4e594065a99","arxiv_id":"2602.10746","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Continuation-based weakest-precondition rules let structured programs be verified against LTL properties like 'always eventually a tick occurs' using nested induction/coinduction hypotheses.","lead":"Programs are hard to prove correct against 'eventually this happens' requirements; this paper gives a weakest-precondition recipe for checking such temporal guarantees in ordinary structured code. It packages known ideas—continuations, step-normal forms, and placeholder hypotheses—into a rule set that auto-active verification tools could adopt.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unproved recurrence simplification H(ω)⇒□H(ω) (after eq. 20) is false for rule (18) instances; e.g., H'(ω)=p∨◦(ω⇒q) fails, so the nested-hypothesis drop is unsound as stated.","rationale":"The reader identified the recurrence property as the primary fragile assumption. My analysis confirms that the stated claim is not merely unproved but false for a concrete instance of rule (18), which is central to the advertised uniform hypothesis-generation mechanism. Because the simplification is used to drop hypotheses when stacking nested (co)inductive arguments, an invalid recurrence property can lead to verification conditions that are too weak, i.e., the calculus could prove properties that do not hold. This is a soundness bug, not a minor omission. The paper's claimed Isabelle/HOL formalization is not inspectable from the submission, so I cannot verify whether the formalization actually contains the same unsound simplification; either it does (making the formalization incorrect) or it does not (making the paper inconsistent with the formalization). Either way, the presented argument is not acceptable as is. The side condition in rule (12) is a secondary issue; the recurrence gap is the load-bearing one. A concrete counterexample can be checked instantly, so the verdict should be REJECT rather than CONDITIONAL.","tokens_in":9959,"tokens_out":19005,"duration_ms":173944,"concrete_test":"Run a proof check (Isabelle/HOL) or LTL satisfiability solver on the formula (p ∨ ◦(ω⇒q)) ⇒ □(p ∨ ◦(ω⇒q)) with p,q constant false and ω true exactly at time 2. The finite trace s0,s1,s2 refutes it. If the authors' formalization rejects this instance or proves recurrence only for a restricted class (e.g., hypotheses of the form (φW+ω)⇒false), that restriction must be stated and the omitted hypotheses reinserted; otherwise the simplification is unsound.","verdict_should_be":"REJECT","load_bearing_attack":"The most load-bearing point is the unproved assertion in §4, after eq. (20): 'Induction/coinduction over LTL operators in fact produces hypotheses that are recurrent, i.e., H(ω) =⇒□H(ω), and we can omit such hypotheses from within Φ(...) resp Mδ(...).' The soundness of the nested-hypothesis mechanism depends on this: when a hypothesis H is generated and later reused inside another hypothesis, it is dropped because it is assumed to persist. The claim is not a consequence of the rule forms. Instantiate rule (18) with the standard least-fixpoint body Φ(X)=p∨◦X, H(ω)=true, φ=q. The generated hypothesis is H'(ω)=p∨◦(ω⇒q). Over the LTL trace where p and q are always false and ω is true only at time 2, H' is true at time 0 (next state has ω false, so ω⇒q vacuously true) and false at time 1 (next state has ω true and q false, so ω⇒q false). Hence H'(ω) ⇒ □H'(ω) is invalid. Since rule (18) is part of the advertised uniform mechanism, and since such an H' can be the 'previous hypothesis' in a subsequent application of (20), the simplification can weaken the verification condition and yield unsound results. No proof or restriction to a recurrent subclass is given.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a weakest-precondition calculus for a nondeterministic imperative language with linear temporal logic specifications over infinite traces. The main idea is to represent programs and residual computation as continuations, use a step-normal form to move through time, and introduce placeholder variables for inductive/coinductive hypotheses when reasoning about iterations. The calculus is presented as a set of syntactic rules, with two worked examples: a safety property over an infinite incrementing loop and a liveness property (□♢tick) for a prime-enumerating loop. The paper claims that the main results are formalized in Isabelle/HOL and implemented in a Scala embedded DSL, with a Zenodo artifact.","tokens_in":10408,"tokens_out":11321,"duration_ms":123905,"significance":"If the calculus were sound and as syntax-directed as claimed, it would provide a useful bridge between auto-active verification and temporal specifications, avoiding user-written history variables for liveness proofs. The paper is honest about assembling ideas from the literature and gives carefully worked examples. The claimed Isabelle/HOL formalization and Scala implementation are strengths, but the manuscript itself does not state or prove a soundness theorem for the calculus, and, as detailed below, some of the stated rules are unsound as written. The intended contribution is therefore not yet established at the level required for publication.","major_comments":[{"comment":"The assertion that every generated hypothesis is recurrent, H(ω) ⇒ □H(ω), is false. Instantiate rule (18) with Φ(X) = p ∨ ○X, H(ω) = true, and φ = q. The generated hypothesis is H'(ω) = p ∨ ○(ω⇒q). Consider the trace where p and q are always false and ω is true only at time 2. At time 0, H' holds because the next state has ω false, making ω⇒q vacuously true. At time 1, H' fails because the next state has ω true and q false. Thus H'(ω) ⇒ □H'(ω) is invalid. Since such H' can be the 'previous hypothesis' in a later application of (18)–(20), the simplification of omitting hypotheses inside Φ(...) and Mδ(...) can weaken verification conditions and yield unsound conclusions. A proof of recurrence for a restricted, explicitly characterized class of generated hypotheses is required, or the simplification must be removed.","section":"§4, after Eq. (20)"},{"comment":"The rule wp(κ,p) ⇐⇒ p with the side condition κ≠false is not valid. Take κ=q and p=false. Then wp(κ,p) is q⇒false, which is not equivalent to false when q is satisfiable. The side condition does not ensure the left-to-right direction; the text immediately following the rule says 'always unfolding eq. (12) left-to-right without checking is probably reasonable,' which is unsound. The condition must be strengthened (e.g., require κ to be valid, or track reachability explicitly), and the rule as stated cannot be used safely in the calculus.","section":"§4, Eq. (12)"},{"comment":"No soundness theorem is stated or proved for the iteration-rule mechanism. The surrounding text gives meta-level justifications, but these are not formal derivations from the fixpoint laws, and they do not address the recurrence failure pointed out above. The paper should state precisely which hypothesis templates H are admissible, what side conditions must hold, and then prove (or provide a machine-checked certificate) that each rule preserves the semantics of wp. This is central to the paper's claim of a uniform mechanism for nested hypotheses.","section":"§4, Eqs. (18)–(21)"},{"comment":"The definition c* = νκ. c;κ has no base/exit case. The greatest fixpoint of X ↦ c;X denotes only infinite repetition when c cannot produce an empty trace. Consequently, the calculus as presented cannot express guarded while loops with termination, despite the paper's claim to support 'structured programs'. The examples all involve nonterminating iterations; in Example 1 the appended skip* is never reached, since c* cannot terminate. Either the intended scope must be explicitly restricted to nonterminating loops, or the program grammar and the iteration rules must be extended with a proper guarded iteration construct.","section":"§3, Eq. (3)"}],"minor_comments":[{"comment":"'rests on the ability to effectively the translation' appears to be missing a word (e.g., 'perform').","section":"Abstract"},{"comment":"'Itisalwayspossible' should read 'It is always possible'.","section":"§4, around Eq. (15)"},{"comment":"'primesgoes' and 'ineach step' are missing spaces; also the first sentence uses 'primes' as a program name without explaining the notation.","section":"§5"},{"comment":"A footnote marker appears after 'respectively' in the sentence introducing rules (18)–(20), but the footnote text is not included in the manuscript.","section":"§4"},{"comment":"The functions 'unfold' and 'cfn' are used in the transformation to step form but not formally defined; a precise definition would improve reproducibility.","section":"§4, step form"},{"comment":"The command 'skip' is used in 'skip*' but is not introduced in the program grammar (1); this should be clarified.","section":"§5, Example 2"}],"recommendation":"major_revision","confidential_remarks":"The claimed Isabelle/HOL formalization should be checked against the specific counterexample to the recurrence simplification in §4. If the formalization indeed proves the simplification, the formal statements or the paper's account of them are inconsistent. The editor may also want to verify that the Zenodo artifact corresponds to the rules as written, since the manuscript provides no theorem statements that can be checked independently."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nQuick take: this is a readable, honest synthesis of existing ideas — continuations, step form, placeholder hypotheses — into a weakest-precondition calculus for LTL. The genuinely new bit is the uniform wp* rule set for stacking nested inductive/coinductive hypotheses (eqs. 18–20). That is a real contribution, and the worked examples (especially the primes/liveness one) show the machinery in action. The paper also credits prior work properly and does not oversell novelty.\n\nThe problem is the unproved recurrence assertion in §4, right after eq. (20): hypotheses generated from LTL operators are claimed to be recurrent, H(ω) ⇒ □H(ω), so they can be dropped inside Φ and Mδ. No proof is given, and the stress-test counterexample suggests the claim is false in general. Instantiate rule (18) with Φ(X)=p∨◦X, H(ω)=true, φ=q to get H'(ω)=p∨◦(ω⇒q). On a trace where p,q are always false and ω holds only at time 2, H' is true at time 0 and false at time 1. So H' is not recurrent. The same construction works for rule (19) instances as well. Since this recurrence is what justifies omitting the accumulated hypotheses from the definitions of new H', the simplification as stated can change the hypotheses to stronger claims that are not supported by the induction/coinduction principles. That is a load-bearing gap, not a cosmetic one.\n\nThe displayed rules (18)–(20) do include the previous H(ω), so a conservative reading is that the calculus might be sound without the simplification. But then the rules are heavier, and the paper explicitly relies on the recurrence to make the method practical. The Isabelle/HOL formalization and Scala implementation on Zenodo could settle this — but the submission gives no pointer beyond the DOI, no excerpt, no statement of which lemmas are proved. That makes the gap hard to check.\n\nOther soft spots are minor by comparison: rule (12)'s side condition κ≠false is not tracked in the automatic left-to-right direction, and the step-form transformation is described at a high level. Both are addressable.\n\nWho should read this: anyone building a VCG for temporal properties in Why3/Dafny/Viper would find the rule structure and the examples useful, provided the recurrence issue gets fixed or the formalization confirms soundness. I'd send it to a serious referee, but I'd want the referee to push on the recurrence lemma before acceptance. If the gap is real, the paper needs a proof of recurrence for the actual hypotheses generated, or a restriction on placeholders that makes it true.\n\nRecommended action: engage with it — the contribution is worth a careful look, but the current version is not yet a sound foundation without addressing the counterexample.","headline":"A useful synthesis of known ideas into a WP calculus for LTL, but the unproved recurrence claim looks false — the calculus's main simplification rests on a load-bearing gap.","tokens_in":10832,"tokens_out":9205,"would_cite":false,"duration_ms":83067,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"A weakest-precondition calculus brings linear temporal logic liveness proofs into the reach of auto-active verification tools.","keywords":["weakest precondition","linear temporal logic","liveness","verification condition generation","auto-active verification","coinduction","loop invariants","infinite traces"],"falsifier":"Check the recurrence property on the hypotheses generated by rules (18)–(20): exhibit one generated formula H(ω) for which there is a trace satisfying H(ω) but not □H(ω). In LTL's standard trace semantics this would be a finite counterexample to the unproved claim, and it would invalidate the simplification that makes the loop-elimination rule (21) sound.","tokens_in":9863,"feed_emoji":"🔁","tokens_out":5676,"duration_ms":54611,"temperature":0.7,"pith_summary":"The paper shows that a weakest-precondition style calculus can be extended to linear temporal logic (LTL) specifications over infinite traces, covering liveness as well as safety. It assembles known ideas—continuations, step-normal form, and placeholder variables for inductive and coinductive hypotheses—into a purely syntactic set of rules that turn a program and a temporal guarantee into a plain temporal logic proof obligation. The central technical contribution is a uniform mechanism that generates multiple nested hypotheses for a loop before the iteration is split into base and step cases, so properties like 'infinitely often φ' can be proved by combining an outer coinduction with an inner well-founded induction. If the calculus is sound, auto-active verifiers could accept temporal specifications as first-class without requiring users to write history or prophecy variables.","feed_headline":"Temporal liveness becomes checkable in weakest-precondition form","feed_subtitle":"Programs get syntax-driven proof obligations for properties like 'infinitely often tick'—no user-written history variables.","key_machinery":"The central object is the continuation κ, which prefixes a temporal formula with a computation, and the placeholder ω that stands for the residual of an iteration after one step. The workhorse is the operator wp*, which accumulates a list of hypothesis templates H1,…,Hn, each derived from an LTL operator's fixpoint characterization: least-fixpoint rules for eventually-like properties, greatest-fixpoint rules for always-like properties, and well-founded measure templates Mδ(φ) that assert φ for all future states in which δ has decreased. The key identity that carries the argument is the claim that hypotheses generated from LTL operators are recurrent, H(ω) ⇒ □H(ω), which justifies dropping pr","core_discovery":"The paper's central claim is that a weakest-precondition operator wp(κ, ψ), defined as the implication κ ⇒ ψ, can be the basis of a syntax-directed calculus over program continuations. The rules distribute wp over nondeterministic choice, shift sequential composition into the continuation, and handle atomic steps by first bringing the guarantee into step-normal form and then applying the ordinary state-based weakest precondition. Iteration is handled by a family of rules that introduce parametric hypothesis templates H(ω) corresponding to least fixpoints (eventually), greatest fixpoints (always), and well-founded measures Mδ, collected by a variant wp* that stacks multiple hypotheses. A fina","pith_inferences":["With the recurrence assumption made explicit as a proof obligation, the same template could extend to richer fixpoint logics such as the μ-calculus; the paper only instantiates the mechanism for LTL operators.","The side condition κ≠false in rule (12) suggests that a practical implementation must either check for non-false continuations or restrict that rule to terminating programs; otherwise a naive left-to-right application could prove properties that do not hold for non-terminating executions.","The loop-handling rules likely compose with existing invariant and decreases-clause machinery, allowing a tool to layer temporal reasoning on top of standard partial-correctness verification condition generation.","The primes example suggests a reusable proof pattern for recurrence properties: choose a measure that decreases toward the next occurrence, and use the outer always-hypothesis to restart the measure after each occurrence."],"forward_implications":["Auto-active verification tools could accept LTL specifications as first-class, generating proof obligations for liveness properties without user-written history variables.","Recurrence properties like always-eventually φ become provable through a structured combination of outer coinduction and inner well-founded induction.","The calculus supports nested temporal operators, since hypotheses are stacked independently of the decomposition of the loop.","Because verification conditions are plain temporal logic formulas, they can be handed to automated theorem provers that reason about LTL, as demonstrated by the examples.","The approach avoids intermediate assertion invention for sequential composition, preserving the standard weakest-precondition workflow."],"fun_headline_variants":["Liveness checkable via weakest precondition rules","Syntax-directed wp for linear temporal liveness","Prove 'infinitely often' with wp, no history vars","Weakest preconditions tame temporal liveness","Universal wp calculus for temporal specs"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The calculus is sound only if every hypothesis generated from the LTL fixpoint rules is recurrent—H(ω) implies □H(ω)—so that previously established hypotheses can be dropped inside new hypotheses and inside the well-founded-measure template Mδ; this property is asserted but not proved in the paper, and if it fails for some generated formula, the rule that eliminates loops could over-approximate and prove false properties.","fun_headline_variants_meta":{"raw":{"variants":["Liveness checkable via weakest precondition rules","Syntax-directed wp for linear temporal liveness","Prove 'infinitely often' with wp, no history vars","Weakest preconditions tame temporal liveness","Universal wp calculus for temporal specs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000259,"raw_usage":{"total_tokens":1365,"prompt_tokens":629,"completion_tokens":736,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":373,"completion_tokens_details":{"reasoning_tokens":667}},"tokens_in":373,"tokens_out":736,"duration_ms":7807,"temperature":1.0,"reasoning_tokens":667,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T00:59:14.902251+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check the recurrence property on the hypotheses generated by rules (18)–(20): exhibit one generated formula H(ω) for which there is a trace satisfying H(ω) but not □H(ω). In LTL's standard trace semantics this would be a finite counterexample to the unproved claim, and it would invalidate the simplification that makes the loop-elimination rule (21) sound.","supporting_citations":[],"review_version":1}