REVIEW 3 major objections 4 minor 20 references
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
T0 review · 3 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash
Pith's one-line read 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.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (3)
- [§3.1, Fix rule] 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.
- [§3.1, RepeatBreak rule] 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.
- [§2.2 and §3.2, theorem statements] 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.
minor comments (4)
- [Appendix A.2] 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.
- [§3.2, match_loop postcondition] 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.
- [§2.1, footnote 8] 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.
- [References] 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.
Circularity Check
No circularity found: the case-study proofs are developed from explicit monadic definitions, not from their own conclusions.
full rationale
The paper's derivation chain is formal and definitional rather than empirical. It defines programs as ternary relations, defines Lfix and repeat_break, defines Hoare triples, and then states proof rules and applies them to DFS and KMP. The correctness claims are proved against those explicit definitions; there are no fitted parameters and no quantity is predicted from a fitted input. The self-citations are not load-bearing: [3] is a set library used for basic infrastructure, [18] supplies graph definitions but not the DFS correctness theorem, and [20] is a separate follow-up refinement result. No uniqueness theorem is imported from the authors' prior work, and no ansatz is smuggled in via citation. The rules Fix and RepeatBreak, and footnote 8's caveat about Lfix monotonicity/continuity, raise an auditability and soundness-exposition concern: the paper states these rules without demonstrating their derivability from the denotational semantics, and the artifact is not pinned to a commit. That is a correctness/verifiability risk, not circularity: the rules are not justified by the case studies they are used to prove. The KMP and DFS theorems are stated independently of the framework's claimed advantages, and the paper does not rename a known result or define a concept in terms of the conclusion it is supposed to derive. Overall, the central claims have independent formal content.
Assumptions & free parameters
assumptions (3)
- domain assumption Program meaning is exactly the ternary relation of initial state, return value, and final state.
- standard math Kleene fixed-point recursion requires monotone and continuous program transformers; the paper defines Lfix for arbitrary f and relies on monotonicity for recursion and loops.
- domain assumption The stated Hoare rules, including Fix and RepeatBreak, are sound for the relational semantics.
invented entities (1)
-
State relation monad
Cite this review
Pith. "Pith review of A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms." pith.science (2026). https://pith.science/paper/BLYYRP6P
@misc{pith2026250419852,
author = {Pith},
title = {Pith review of: A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms},
year = {2026},
howpublished = {\url{https://pith.science/paper/BLYYRP6P}},
note = {Machine review of arXiv:2504.19852}
}
read the original abstract
Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For verification, formal proof based on Hoare logic cannot reflect the logical structure of natural proof. To address these challenges, we introduce a formal framework for naturally specifying and verifying sequential algorithms in Coq. We use the state relation monad to integrate Coq's expressive type system with the flexible control flow of imperative languages. It supports nondeterministic operations and customizable program states, enabling specifying algorithms at an appropriate level of abstraction. For verification, we build a Hoare logic for the monad and propose a novel two-stage proof approach that separates natural logical reasoning from mechanical composition. It reflects the logical structure of natural proof, enhancing modularity and readability. We evaluate the framework by formalizing the Depth-First Search (DFS) algorithm and verifying the Knuth-Morris-Pratt (KMP) algorithm.
Reference graph
Works this paper leans on
-
[1]
Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, 2nd edn. (2007)
work page 2007
-
[2]
Appel, A.W.: Verified Functional Algorithms, Software Fo un- dations, vol. 3. Electronic textbook (2024), version 1.5.5 , http://softwarefoundations.cis.upenn.edu
work page 2024
-
[3]
Electronic Proceedings in Theoretical Computer S cience 400, 79–95 (04 2024)
Cao, Q., Wu, X., Liang, Y.: A Coq library of sets for teachin g denotational se- mantics. Electronic Proceedings in Theoretical Computer S cience 400, 79–95 (04 2024). https://doi.org/10.4204/EPTCS.400.6
-
[4]
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: I ntroduction to Algorithms, Third Edition. The MIT Press, 3rd edn. (2009)
work page 2009
-
[5]
Hoare, C.A.R.: An axiomatic basis for computer programmi ng. Commun. ACM 12(10), 576–580 (Oct 1969), https://doi.org/10.1145/363235.363259
arXiv 1969
-
[6]
Journal of Functional Programming 28, e20 (2018)
Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birked al, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-ord er concur- rent separation logic. Journal of Functional Programming 28, e20 (2018). https://doi.org/10.1017/S095679681800014X
-
[7]
Knuth, D.E., Morris, J.H., Pratt, V.R.: Fast pattern matc h- ing in strings. SIAM J. Comput. 6, 323–350 (1977), https://api.semanticscholar.org/CorpusID:11697579
work page 1977
-
[8]
Lammich, P.: Refinement for monadic programs. Archive of F ormal Proofs (Jan- uary 2012), https://isa-afp.org/entries/Refine_Monadic.html, Formal proof development
work page 2012
Show all 20 references
-
[9]
Lammich, P., Neumann, R.: A framework for verifying depth -first search algo- rithms. p. 137–146. CPP ’15, Association for Computing Mach inery, New York, NY, USA (2015), https://doi.org/10.1145/2676724.2693165
2015
-
[10]
Informati on and Computation 93(1), 55–92 (1991)
Moggi, E.: Notions of computation and monads. Informati on and Computation 93(1), 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4
1991 doi
-
[11]
Nanevski, A., Morrisett, J., Birkedal, L.: Hoare type th eory, poly- morphism and separation. J. Funct. Program. 18, 865–911 (09 2008). https://doi.org/10.1017/S0956796808006953
2008 doi
-
[12]
In: Cohen, L., Kaliszyk, C
Nigron, P., Dagand, P.E.: Reaching for the Star: Tale of a Monad in Coq. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on In teractive Theorem Prov- ing (ITP 2021). Leibniz International Proceedings in Infor matics (LIPIcs), vol. 193, pp. 29:1–29:19. Schloss...
2021 doi
-
[13]
Springer-Verlag, Berlin, Heidelberg (2002)
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: a p roof assistant for higher- order logic. Springer-Verlag, Berlin, Heidelberg (2002)
2002
-
[14]
Arch ive of Formal Proofs (November 2023), https://isa-afp.org/entries/KnuthMorrisPratt.html, For- mal proof development
Paulson, L.C.: Knuth–Morris–Pratt string search. Arch ive of Formal Proofs (November 2023), https://isa-afp.org/entries/KnuthMorrisPratt.html, For- mal proof development
2023
-
[15]
Pierce, B.C., de Amorim, A.A., Casinghino, C., Gaboardi , M., Greenberg, M., Hriţcu, C., Sjöberg, V., Tolmach, A., Yorgey, B.: Programmi ng Language Founda- tions, Software Foundations, vol. 2. Electronic textbook ( 2024)
2024
-
[16]
In: Proceedings of the 17th Annual IEEE Symposium on L ogic in Computer Science (LICS 2002)
Reynolds, J.C.: Separation logic: A logic for shared mut able data struc- tures. In: Proceedings of the 17th Annual IEEE Symposium on L ogic in Computer Science (LICS 2002). pp. 59–78. IEEE Computer Soci ety (2002). https://doi.org/10.1109/LICS.2002.1029817 18 C. Yang et al
2002 arXiv
-
[17]
https://coq.inria.fr/doc/V8.19.0/refman (2024)
The Coq Development Team: The Coq reference manual – rele ase 8.19.0. https://coq.inria.fr/doc/V8.19.0/refman (2024)
2024
-
[18]
Wang, S., Cao, Q., Mohan, A., Hobor, A.: Certifying graph -manipulating C programs via localizations within data structures. Proc. A CM Program. Lang. 3(OOPSLA) (Oct 2019), https://doi.org/10.1145/3360597
2019 doi
-
[19]
MIT Press, Cambridge, MA, USA (1993)
Winskel, G.: The Formal Semantics of Programming Langua ges: An Introduction. MIT Press, Cambridge, MA, USA (1993)
1993
-
[20]
Al though we can use a state relation monad with unit state (as we’ve done in previous examples), it is more convenient and natural to use a monad that is intrin sically stateless
WU, S., WU, X., Cao, Q.: Encode the ∀∃ relational Hoare logic into standard Hoare logic (2025), https://arxiv.org/abs/2504.17444 A Formal Framework for Naturally Specifying and Verifying A lgorithms 19 A Stateless and Errorful Variants of the State Relation Monad A.1 Set Monad...
2025 arXiv
Reviewed August 16, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.