{"id":"4e50850d-07a8-428f-9e28-43bcfeaee8e1","arxiv_id":"2504.19852","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A state relation monad plus a two-stage proof style lets algorithms like DFS and KMP be specified and verified in Coq with proofs organized by logical structure.","lead":"This paper introduces a Coq framework for specifying sequential algorithms with a state relation monad and proving them with a two-stage Hoare logic. It demonstrates the framework on depth-first search and the Knuth-Morris-Pratt string matching algorithm.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Soundness of the core Hoare rules (Fix, RepeatBreak) is asserted but not demonstrated, and the artifact is unpinned, so the framework's central claim is not fully auditable from the paper.","rationale":"The reader's weakest-assumption analysis identifies exactly the same gap: the soundness of the Section 3.1 Hoare rules, especially RepeatBreak and Fix, is asserted rather than demonstrated, and the artifact is not pinned to an auditable commit. I examined whether the rules are nevertheless immediately justifiable from the denotational semantics. The basic rules (Bind, Choice, Assume, Consequence, Conjunction) are straightforwardly sound, and the Fix rule is plausibly sound if Lfix is interpreted as the union of finite iterates; however, the text does not state the required definitional details, and the RepeatBreak rule depends on missing definitions of continue_case and break_case. This is a genuine load-bearing gap for a paper whose contribution is a formal framework, but it is a condition that can be satisfied by exposing the artifact and the rule proofs, so the reader's CONDITIONAL verdict is appropriate and no verdict change is needed.","tokens_in":13929,"tokens_out":14185,"duration_ms":159248,"concrete_test":"Check out the repository at the exact commit referenced by the paper and rebuild it with Coq 8.15.2. Locate the Coq statements and proofs of the Fix and RepeatBreak rules; verify that these proofs are closed (no admitted axioms or extra parameters) and that RepeatBreak is derived from the definitions of repeat_break, continue_case, and break_case rather than stated as an axiom. If the derivation requires monotonicity of repeat_break_f, confirm that hypothesis is either listed in the rule or discharged for every use in the DFS and KMP proofs. A passing check settles the concern; any proof relying on admit, axiom, or an omitted side condition would mean the framework's soundness claim is unsupported as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the state-relation monad and the Section 3.1 Hoare rules provide a sound framework, with DFS and KMP as evidence. The load-bearing point is the soundness of the recursion and loop rules. The Fix rule is stated without the monotonicity/continuity hypotheses that footnote 8 indicates are needed for Lfix to be a Kleene fixed point, and RepeatBreak is stated using continue_case and break_case, whose definitions are only described in prose rather than given. From the text alone, a reader cannot verify whether RepeatBreak is derivable from the Lfix definition, whether continue_case and break_case are exhaustive complementary projections of ContinueOrBreak, or whether the postcondition `{P}` in the continue premise is meant to depend on the resumed value. The linked repository is not pinned to a commit and no build instructions are provided, so the claimed Coq proofs of these rules cannot be inspected. If either rule has an unstated side condition that is not discharged in the development, the KMP and DFS theorems do not follow from the definitions shown. This is not an observed inconsistency, but it is the place where the paper's formal claims outrun its formal exposition.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a formal framework, implemented in Coq, for specifying and verifying nondeterministic sequential algorithms. The core idea is a state relation monad in which programs are ternary relations over initial state, return value, and final state, supporting monadic operators, nondeterministic choice, assumptions, and general recursion via least fixed points. On top of this monad the authors build a Hoare logic for partial correctness and introduce a two-stage proof approach that separates natural logical reasoning from mechanical composition. The framework is evaluated by formalizing a nondeterministic depth-first search algorithm and by verifying a two-loop formulation of the Knuth-Morris-Pratt string-matching algorithm, including the table-building procedure.","tokens_in":14122,"tokens_out":6642,"duration_ms":65111,"significance":"If the reported Coq development is correct and the artifact is made available in a reproducible form, the framework is a useful addition to the toolbox for algorithm verification. It addresses a real gap: expressing stateful, nondeterministic algorithms at a high level of abstraction while keeping proofs organized by logical dependency rather than by program syntax. The claimed machine-checked correctness proofs for DFS and KMP would constitute concrete evidence that the framework scales to nontrivial algorithms. The two-stage proof method is a pragmatic organizational idea that could be adopted in other Hoare-logic-based verification settings. However, the contribution is incremental relative to existing monadic Hoare logics and refinement frameworks, and its value depends on the soundness and usability of the presented rules, which the paper does not fully expose.","major_comments":[{"comment":"The Fix rule is stated without any hypotheses on the function F, but footnote 8 acknowledges that Lfix is a Kleene fixed point only when F is monotone and continuous. The paper does not prove the soundness of the rule from the definition of Lfix, nor does it state the side conditions under which the rule is valid. This matters because all recursion and loop reasoning, including the repeat_break construct used in the DFS and KMP case studies, relies on this rule. The authors should provide a proof (or a precise statement with side conditions) in the appendix, or point to a specific, version-pinned location in the artifact where the Coq statement of the rule is proved.","section":"§3.1, Fix rule"},{"comment":"The RepeatBreak rule is stated using continue_case and break_case, whose definitions are only described in prose as \"unwraps\" the corresponding constructor. The soundness of the rule depends on the exact behavior of these operators, including how they act on the opposite constructor and how the state component is threaded. The paper also leaves unclear whether the postcondition {P} in the continue premise is meant to be P(a') for the unwrapped value a' and how this interacts with the loop invariant. A formal derivation of RepeatBreak from the definition of repeat_break as Lfix and from explicit definitions of continue_case and break_case is needed to make the KMP proof auditable from the text.","section":"§3.1, RepeatBreak rule"},{"comment":"The paper states the main evaluation claims only informally. In §2.2, it says \"we proved that a vertex is visited after the DFS if and only if it is reachable from the starting vertex,\" but the formal theorem statement is not given, and it is unclear whether this is a partial-correctness or total-correctness claim. In §3.2, the KMP match correctness is presented as a Hoare triple, but the postcondition is written in informal mathematical notation with an unbound variable i, and the correctness theorem for the table-building procedure is only mentioned in passing. For a verification paper, the exact Coq statements of these theorems are the primary results and should be stated in the text or appendix so that the claims can be checked without loading the artifact.","section":"§2.2 and §3.2, theorem statements"}],"minor_comments":[{"comment":"In the definition of bind for the error monad, the error case is written as \"s∈ bind(c, f ).err ⇐⇒ s∈ c.err ∨ (∃ a s2, (s1,a,s2)∈ c.nrm ∧ s2∈ f(a).err).\" The variable s on the left should be s1, and the first disjunct should be s1∈ c.err, for consistency with the nrm case.","section":"Appendix A.2"},{"comment":"The displayed postcondition for match_loop, \"{λr. { first_occur(i) if r = by_break(i), no_occur(text.len) if r = by_continue(i) }},\" is not a well-formed Coq or mathematical expression because the pattern variable i is not bound in the λr. The authors should present this as a match expression on r, e.g., λr, match r with by_break i => first_occur i | by_continue i => no_occur text.len end.","section":"§3.2, match_loop postcondition"},{"comment":"The footnote stating that Lfix is defined for any f although Kleene's theorem requires monotonicity and continuity raises a concern that is not addressed later. Even if the Fix rule itself is sound as an induction principle over iterates, the paper does not explain how the recursive programs used in the examples are known to be fixed points of their defining equations, which is necessary for unfolding recursive calls in proofs.","section":"§2.1, footnote 8"},{"comment":"The artifact link is a GitHub repository without a commit hash or version identifier, and no build instructions are given. For a formal-verification paper, the artifact should be archived with a permanent DOI and a pinned commit so that the claimed Coq proofs can be inspected and reproduced.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper reports a substantial mechanized development, but the current submission does not make the key soundness proofs or exact theorem statements available in the text, and the artifact is unpinned. This is fixable within the scope of a revision. I would also suggest that the authors clarify the novelty of the two-stage proof approach relative to standard Hoare-logic composition and to the Isabelle Refinement Framework, since the current related-work discussion is somewhat brief."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is that this is a real contribution with a real gap in exposition. Yang, Wu, and Cao build a state relation monad in Coq and pair it with a two-stage proof discipline: first prove grouped Hoare triples for basic blocks following logical themes, then mechanically compose them with conjunction and consequence rules. That separation is the genuinely new piece, and it reads like a true usability improvement for verifiable algorithm specifications. The DFS formulation is concise, and the KMP verification, including the table-building procedure, is substantial evidence that the framework works on non-toy examples.\n\nThe writing is clear, and the related work is positioned fairly. The comparison with Nigron et al. and with Lammich's refinement framework is accurate rather than self-serving.\n\nNow the soft spots, both in the formal exposition. Section 3.1 states two rules that carry the whole framework: Fix and RepeatBreak. The text does not show their soundness proofs, nor even the definitions of continue_case and break_case, only a prose description. Footnote 8 concedes Lfix is only the Kleene fixed point when f is monotone and continuous, but the Fix rule as printed has no such hypotheses, and the paper never states where these side conditions are discharged in Coq. The RepeatBreak rule likewise has unstated details: whether the postcondition in the continue premise is meant to depend on the resumed value, and whether continue_case and break_case really partition ContinueOrBreak. This is not an observed inconsistency, but it is exactly the load-bearing part that the reader cannot check from the PDF. The artifact link is a bare GitHub URL with no commit hash or build instructions, so even the existence of the formalizations is not independently auditable from the paper.\n\nThese are fixable in revision. The authors should pin a commit, add a short appendix or precise pointers to the .v files and lines for the soundness proofs, and make the case-splitting operators explicit. The two-stage method itself does not collapse. I would send this to peer review, but reviewers should be expected to obtain the artifact and inspect the stated rules.\n\nMy bottom line: treat it as a conditional accept-shaped paper. The contribution is clear, the case studies are credible, and the missing pieces are expositional—but for a formal verification paper, leaving the core inference rules unverifiable from the text is a real incompleteness. For a reading group, it is worth a session. I would cite it if I worked on monadic Hoare logics.","headline":"A genuinely useful two-stage proof framework for Coq with real case studies, but the core Hoare rules' soundness and the artifact are under-exposed, so it needs a condition-led review.","tokens_in":14664,"tokens_out":4217,"would_cite":true,"duration_ms":38517,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A state-relation monad lets algorithm proofs follow logical structure rather than program syntax, and the paper demonstrates it by formalizing DFS and verifying KMP.","keywords":["formal verification","state relation monad","Hoare logic","nondeterministic algorithms","two-stage proof","Knuth-Morris-Pratt","depth-first search","proof assistant"],"falsifier":"Check the paper's linked proof development for whether the Fix and RepeatBreak rules are derived lemmas from the relational semantics rather than assumed axioms; if they are axioms, the claimed soundness of the framework is not established. More directly, exhibit any program and precondition for which the two rules certify a Hoare triple but the relational definition contains a terminating run violating the postcondition.","tokens_in":13711,"feed_emoji":"🧩","tokens_out":13291,"duration_ms":126329,"temperature":0.7,"pith_summary":"This paper proposes a framework for specifying and verifying sequential algorithms in a proof assistant, and claims that it lets formal proofs mirror the structure of a natural mathematical argument instead of the syntax of the program. The key move is to represent a program as a state relation monad, i.e. a ternary relation on initial state, return value, and final state, which makes nondeterministic steps and abstract operations expressible as logical relations. On top of this, the paper builds a Hoare logic for partial correctness and a two-stage proof method: first prove logical groups of properties about individual basic blocks, then mechanically compose these into an end-to-end correctness proof. If the approach works as claimed, formal verification of stateful algorithms such as DFS and KMP becomes more modular, more readable, and closer to how an algorithm designer would write the correctness argument; the paper provides formalizations of DFS and a verified KMP as evidence.","feed_headline":"A state-relation monad makes algorithm proofs follow logic, not syntax","feed_subtitle":"DFS and KMP are formalized in a proof assistant; proofs are split into logical groups then composed mechanically","key_machinery":"The load-bearing object is the state relation monad, written in the paper as `program $\\Sigma\\,A := \\Sigma \\to A \\to \\Sigma \\to \\mathrm{Prop}$`: a program is a ternary relation linking an initial state, a return value, and a final state. On this foundation sit operators `choice`, `assume`, `any`, and `update`, recursion defined through the least fixed point `Lfix` (from the Kleene fixed-point theorem), and `repeat_break`, a loop-with-break combinator built from `Lfix` and a `ContinueOrBreak` sum type. The Hoare logic gives rules for each operator and for `Fix` and `RepeatBreak`; the conjunction rule is the piece that makes the two-stage proof method work, because it lets separately proved properties of the same basic block be merged into a single triple before mechanical composition.","core_discovery":"The central claim, stated on the paper's own terms, is that a denotational relation monad is a suitable interface for algorithm specification and verification. A program is defined as a ternary relation $\\Sigma \\to A \\to \\Sigma \\to \\mathrm{Prop}$, so a computation is a set of possible runs; nondeterministic choice, assumptions, arbitrary value selection, and state updates are all defined as operations on such relations, and recursion plus loops with break are obtained from a least fixed point. Over this monad, a Hoare triple asserts partial correctness in the usual sense: every terminating run from a state satisfying the precondition returns a value and final state satisfying the postcondition. The paper's additional claim is that with the conjunction rule and a two-stage proof discipline, one can prove the correctness of KMP by first establishing groups of invariants in the order a human would use, then composing the resulting triples with largely mechanical rule applications.","pith_inferences":["Because program equivalence in this framework is just double inclusion of relations, the same monad offers a natural route to refinement proofs: showing an implementation refines a specification reduces to proving one relation is contained in another.","The two-stage split suggests an automation strategy: a tactic or tool could synthesize the mechanical composition stage from the logical groups, leaving only the essential implications for the user.","The errorful variant has not been exercised on realistic examples in the paper; a natural test is an algorithm whose correctness depends on explicit bounds or assertion checks.","The DFS formulation indicates that stateful graph algorithms beyond DFS, such as strongly-connected-components algorithms, could be handled by changing only the state record and basic operations while keeping the Hoare rules unchanged."],"forward_implications":["Users can specify nondeterministic algorithms at a high level, e.g. 'pick any unvisited neighbor of u', without fixing traversal order or concrete data structures; the DFS formalization is the demonstration.","Algorithms with multiple layers of loops and breaks, such as KMP's match and table-building procedures, can be formalized with their natural imperative structure rather than flattened into single-layer loops.","The two-stage proof approach is claimed to be general: it can be applied to any Hoare-logic-based framework, not only to this particular monad.","The errorful variant of the monad supports both functional correctness and error-freedom proofs, so algorithms with assertion-like checks can be verified within the same framework.","For DFS, the framework yields a reachability theorem: after the search from a starting vertex, a vertex is visited if and only if it is reachable from that start."],"supporting_citations":[{"why":"Supplies the set and relation library on which programs-as-relations are built.","marker":"[3]"},{"why":"Provides the Hoare-logic foundation that the paper's partial-correctness triples adapt.","marker":"[5]"},{"why":"Defines the KMP algorithm whose match and table-building procedures are verified.","marker":"[7]"},{"why":"Introduces monads for structuring computation, the abstraction the state relation monad instantiates.","marker":"[10]"},{"why":"A prior Hoare-style type-theory approach whose typing judgements the paper adapts into Hoare rules for a relational semantics.","marker":"[11]"},{"why":"Formalized graph-theory library used to define directed graphs and the step relation for the DFS case study.","marker":"[18]"},{"why":"Supplies the Kleene fixed-point theorem used to define recursion and loops via Lfix.","marker":"[19]"},{"why":"Companion work proving a C program refines the KMP specification, cited as evidence of real-world applicability.","marker":"[20]"}],"fun_headline_variants":["State-relation monad: algorithm proofs that mirror human logic","Proofs in two stages: logic then mechanics, via Coq monad","Coq framework verifies DFS and KMP with human-style proofs","A monadic Hoare logic that keeps natural proof structure","State-relation monad splits algorithm proofs into logic and mechanics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The soundness of the recursion and break-loop Hoare rules is asserted rather than derived in the paper, so the verified DFS and KMP theorems inherit their truth from proof obligations the text does not itself carry out.","fun_headline_variants_meta":{"raw":{"variants":["State-relation monad: algorithm proofs that mirror human logic","Proofs in two stages: logic then mechanics, via Coq monad","Coq framework verifies DFS and KMP with human-style proofs","A monadic Hoare logic that keeps natural proof structure","State-relation monad splits algorithm proofs into logic and mechanics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000719,"raw_usage":{"total_tokens":3206,"prompt_tokens":902,"completion_tokens":2304,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":2215}},"tokens_in":518,"tokens_out":2304,"duration_ms":15776,"temperature":1.0,"reasoning_tokens":2215,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:41:38.727812+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check the paper's linked proof development for whether the Fix and RepeatBreak rules are derived lemmas from the relational semantics rather than assumed axioms; if they are axioms, the claimed soundness of the framework is not established. More directly, exhibit any program and precondition for which the two rules certify a Hoare triple but the relational definition contains a terminating run violating the postcondition.","supporting_citations":[{"cited_title":"Electronic Proceedings in Theoretical Computer S cience 400, 79–95 (04 2024)","cited_arxiv_id":null,"evidence_quote":"Supplies the set and relation library on which programs-as-relations are built."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the KMP algorithm whose match and table-building procedures are verified."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Formalized graph-theory library used to define directed graphs and the step relation for the DFS case study."},{"cited_title":"MIT Press, Cambridge, MA, USA (1993)","cited_arxiv_id":null,"evidence_quote":"Supplies the Kleene fixed-point theorem used to define recursion and loops via Lfix."}],"review_version":1}