{"id":"943bb493-015f-417d-89c4-4dbda693f585","arxiv_id":"2504.14561","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":2.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A comprehensive survey of proof scores: their algebraic foundations, supporting tools, successful applications, and the adoption challenges the community still faces.","lead":"This survey explains proof scores, a verification method in which system proofs are written in the same algebraic specification language as the system itself, mainly CafeOBJ and Maude. It covers the underlying theory, the supporting tools, dozens of verified protocols, and the reasons the approach has stayed mostly inside academia.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 7 success stories mostly rest on manual proof scores with no machine-checked case coverage; the survey's central 'successfully verified' claim is only as strong as unverified human discipline.","rationale":"The reader's weakest assumption is exactly the completeness of manual proof scores, and this is the load-bearing point. The paper itself states the limitation in §6.1 and §8.1.7, but the abstract and Section 7 present the large set of case studies as successfully verified without separating those that have been independently machine-checked (via CiMPG) from those that rely solely on human-authored case enumerations. The underlying logic is sound, and CiMPG provides a path to formality, but that path has been applied to only a handful of examples. Therefore the central claim of broad success is stronger than the evidence actually presented. This does not warrant rejection: the survey is honest about the methodology's weakness and is a useful reference. However, a conditional acceptance requiring the authors to explicitly annotate which success stories are machine-checked and which are manual would make the claim accurate. The proposed concrete test would settle whether a representative unevaluated case study admits a formal CiMPG proof; if it does not, the overclaim is confirmed for that instance and the paper should be revised accordingly.","tokens_in":54830,"tokens_out":6225,"duration_ms":55525,"concrete_test":"Run CiMPG on the proof scores for one Section 7 success story not among the six previously machine-checked, e.g., the Mondex electronic purse or Suzuki-Kasami protocol, using the repository at https://github.com/ariesco/proof-scores-survey. If CiMPG reports any unprovable subgoal, or the generated CiMPA proof script omits any open-close environment present in the manual proof score, then that case study's verification claim is formally unsupported and the survey must mark it as manual/unchecked rather than 'successfully verified'.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Section 6.1 concedes that in proof scores 'the user is in charge of ensuring that all possible cases have been traversed; if one subgoal is not taken into account none of the tools will warn the user.' Section 8.1.7 repeats that proof scores are 'semi-formal' because soundness is not checked, and Section 7 limits CiMPG-validated examples to Qlock, ABP, SCP, NSLPK, TLS 1.0, and TLS 1.2. Yet the abstract and Section 7 generalize to a 'large number of systems and protocols' verified by proof scores, including Mondex, SET, Fischer, Suzuki-Kasami, post-quantum SSH, and others. For all but the six explicitly cited examples, the claim of successful verification rests entirely on the completeness of manually constructed case analyses. Since the tools do not check coverage, a missing case yields a proof score that still reduces to true but does not prove the property. The theoretical soundness of order-sorted equational logic (Theorem 3.15) and the structured specification calculus (Section 4.6) does not bridge this gap: those results concern the underlying logic, not the user's obligation to enumerate all cases. The central claim is therefore load-bearing on an unverified empirical assumption about the authors' and community's proof-score discipline.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper is a survey of the proof-score methodology used in the OBJ family of algebraic specification languages, primarily CafeOBJ. It presents the historical origins in Goguen's work, the order-sorted equational logic foundations (Section 3), the structured-specification and parameterization theory (Section 4), the main tools (Section 5), a detailed worked example (Qlock, Section 6.1) together with proof-generation and validation tools CiMPA/CiMPG/IPSG (Sections 6.2-6.3), a topic-organized catalog of successful case studies (Section 7), and a discussion of adoption barriers and future directions (Sections 8-10). The paper argues that proof scores are a flexible verification style that shares syntax with the specification language, and that their main weakness, namely lack of machine-checked case coverage, is partially mitigated by tools that relate proof scores to proof scripts.","tokens_in":55062,"tokens_out":8476,"duration_ms":73268,"significance":"The survey is valuable as an up-to-date reference on a niche but long-lived formal verification methodology, and it is unusually honest about the methodology's semi-formal status. Its theoretical sections are standard but clearly presented, and the worked Qlock example with an accompanying repository is a useful tutorial artifact. The main contribution is the systematic bibliography and the discussion of the gap between proof scores as practiced and machine-checked proofs. However, the paper's headline claim of having verified a large number of systems needs to be read together with its own caveats: only six of the listed case studies have been validated by CiMPG, and the rest rest on manual case coverage. With a more precise classification, the survey could be a definitive reference.","major_comments":[{"comment":"The abstract states that proof scores 'have been successfully used to prove properties of a large number of systems and protocols,' and Section 7 lists dozens of systems as verified. Yet Section 6.1 explicitly concedes that 'the user is in charge of ensuring that all possible cases have been traversed; if one subgoal is not taken into account none of the tools will warn the user,' and Section 8.1.7 calls proof scores 'semi-formal' because soundness is not checked. Section 7 itself limits the formally re-validated examples to Qlock, ABP, SCP, NSLPK, TLS 1.0, and TLS 1.2. For the remaining systems, the verification claim depends entirely on the manual completeness of proof scores that no tool checks. This is not an internal inconsistency, but the headline claim overstates what the paper's evidence supports. I recommend rewording the abstract and Section 7 to distinguish 'proof scores were written and claimed as verifications in the literature' from 'proof scores with machine-checked soundness,' and adding a table or column to Section 7 indicating which case studies have been re-validated by CiMPG or another proof assistant. This is a load-bearing precision issue for a survey whose central claim is the practical success of the methodology.","section":"Abstract; Section 7; Section 6.1"},{"comment":"The structured-specification proof calculus is presented as the formal basis for the induction and rewriting steps used in proof scores, but its soundness is never stated as a theorem. Theorem 3.15 covers only the underlying order-sorted equational logic, and the (Rewriting) rule is justified only by a reference to confluence and termination. The paragraph after Definition 4.11 asserts that 'Structural induction (Ind) is sound for all reachable models' without a proof sketch or a citation to the original soundness result. Because the (Ind) rule is the rule that licenses every transition-system proof in Section 6 and Section 7, the survey should state a precise soundness theorem, or at least point to a specific published proof, for the calculus in Definition 4.11, and should make explicit under which conditions on the constructor set C_SP the rule is applicable. Without this, the 'theoretical foundations' part of the survey is incomplete on a load-bearing point.","section":"Section 4.6, Definition 4.11"}],"minor_comments":[{"comment":"The sentence 'OBJ3 was the first programming supporting verification by proof scores' should read 'the first programming language supporting verification by proof scores.'","section":"Section 5.1"},{"comment":"In the discussion after the third open-close block, 'the goal is not completely proven because it depends of some equations' should be 'because it depends on some equations.'","section":"Section 6.1"},{"comment":"The side condition of the (Ind) rule refers to a 'sort decreasing mapping' without defining it; a short explanation or a reference to constructor-based induction would make the rule self-contained.","section":"Section 4.6, Definition 4.11"},{"comment":"The table and the surrounding text use 'Open-close environment' and 'Open-close' inconsistently, and 'Metalevel' appears both as one word and with a hyphen; please standardize the terminology.","section":"Section 5.5, Table 1"}],"recommendation":"major_revision","confidential_remarks":"The Section 7 success-story list is dominated by the authors' own prior work (e.g., Ogata and Futatsugi's OTS/CafeOBJ proofs, Riesco and Ogata's CiMPG, and Tran and Ogata's TLS verifications). This is natural for a survey written by the main contributors, but it makes the 'large number' claim harder to evaluate independently. If the journal values surveys that can be used by outsiders, I suggest the authors add at least one fully worked, machine-checked example from an independent group, or explicitly state when a listed verification has been independently reproduced. This is not a defect in the technical content, but it affects how the editors should weigh the survey's confidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing to know: this is a survey, not a research result. It does a solid job of organizing the proof scores literature, presenting the standard order-sorted equational logic background, and being honest about the method's weaknesses. The running Qlock example and the GitHub repository of examples are useful additions over the short version.\n\nThe theoretical sections are correct and standard: order-sorted signatures, algebras, satisfaction, completeness of the equational calculus (Theorem 3.15), structured specifications, and the specification proof calculus. Nothing new here, but it's a clean reference. The survey also does well to list tools (OBJ3, CafeOBJ, Maude, CafeInMaude) and to discuss CiMPA/CiMPG and IPSG, which attempt to turn semi-formal proof scores into formal proofs.\n\nThe soft spot, and the paper knows it, is the load-bearing success claim. Section 7 lists many protocols 'verified' with proof scores: Mondex, SET, Fischer, Suzuki-Kasami, post-quantum SSH, and more. But Section 6.1 admits that 'the user is in charge of ensuring that all possible cases have been traversed; if one subgoal is not taken into account none of the tools will warn the user.' Section 8.1.7 repeats that proof scores are semi-formal because soundness is not checked. Only six examples are validated by CiMPG: Qlock, ABP, SCP, NSLPK, TLS 1.0, TLS 1.2. For everything else, the claimed verification rests on the completeness of manually constructed case analyses. That doesn't make the survey wrong, but it means the abstract's 'large number of systems and protocols' is stronger than the evidence presented here. A missing case produces a proof score that still reduces to true but proves nothing. The theoretical soundness of order-sorted equational logic doesn't bridge that gap; it concerns the logic, not the user's obligation to enumerate cases.\n\nThe citation pattern is self-heavy, which is expected for a survey by the main contributors to the area; it's not a flaw by itself. The text has some encoding artifacts (odd glyphs) that may be a production issue rather than a substantive one.\n\nWho should read it: researchers and tool builders in algebraic specification, or anyone wanting a bibliography of proof score case studies. It deserves a serious referee. My recommendation: accept with minor revisions, but ask the authors to temper the 'large number' claim or explicitly mark which success stories are machine-checked and which rely on manual proof score discipline.","headline":"A useful, honestly limited survey of proof scores; the theory is standard and the bibliography is valuable, but the 'large number of verified systems' claim rests on manual proof scores whose case coverage no tool checks.","tokens_in":55578,"tokens_out":2457,"would_cite":true,"duration_ms":23728,"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":"Proof scores are a sound, flexible verification methodology: they turn a theorem-proving problem into declarations and rewritings in the system's own specification language, and generators can convert the resulting scores into formal…","keywords":["proof scores","algebraic specification","term rewriting","theorem proving","observational transition systems","formal verification","structured specifications","order-sorted equational logic"],"falsifier":"Take a published proof score for Qlock, delete one entire open-close environment corresponding to a case split, and run the remaining environments. The survey's own caveat predicts that no tool will complain and the remaining reductions will all return true; if a tool or a regenerated formal proof instead flags the missing case, the coverage gap is narrower than claimed, and if it silently passes, the coverage assumption is confirmed exactly.","tokens_in":54623,"feed_emoji":"✅","tokens_out":10133,"duration_ms":94671,"temperature":0.7,"pith_summary":"This survey argues that proof scores—verification scripts written in the same algebraic specification language as the system being analysed—offer a workable middle path between fully automatic and fully manual theorem proving. The core idea, stated at the outset, is that a theorem-proving problem is transformed into declarations and rewritings such that if everything evaluates as desired, the problem is solved. The paper grounds this in order-sorted equational logic and structured specifications, and it catalogs decades of successful verification of mutual exclusion, communication, authentication, e-commerce, TLS, and post-quantum protocols. It also concedes the method's main weakness: the user must ensure every case split and induction hypothesis is covered, because no tool warns about a missed subgoal. If the survey is right, proof scores are a genuinely practical and theoretically sound verification style, with the surprising consequence that their adoption gap is mostly about tooling and coverage assurance rather than expressive power.","feed_headline":"Proof scores verify systems by rewriting the specification itself","feed_subtitle":"A survey argues proof scores written in the system's own language are sound, flexible, and ready for automation.","key_machinery":"The load-bearing mechanism is the proof score itself: an open-close session in an OBJ-family language that extends a specification module with fresh constants, non-executable premises, and reduction commands. Each session corresponds to one subgoal; induction is simulated by adding induction hypotheses as equations, and case analysis is simulated by adding case-splitting equations. The evaluation engine reduces terms by rewriting, so a subgoal counts as discharged exactly when its reduction reaches true. The theoretical backbone is the completeness theorem for order-sorted equational deduction together with the structural-induction rule for constructor-reachable models: this is what lets the survey claim that 'everything evaluates as desired' really entails that the theorem holds. The observational transition system (OTS) style supplies the standard shape for system specifications—a state sort, transition constructors, and observation functions—so that invariants become equations to be evaluated on every transition.","core_discovery":"The paper's central claim is that proof scores are not just a trick for executing reductions but a verification methodology with a defensible formal basis. In its canonical description, a proof score is a set of declarations and rewritings: the user opens a module, introduces fresh constants, states premises and induction hypotheses as equations, and issues reduction commands; when every open-close environment reduces to true, the theorem is regarded as proved. The paper shows this practice sits on the completeness of order-sorted equational deduction, on structured-specification operators (basic, union, translation, free semantics, constructors), and on a structural-induction rule for reachable models. On that basis it collects a broad list of protocols verified this way—including mutual exclusion, authentication, electronic payment, TLS 1.0 and 1.2, and post-quantum key exchange—and it presents the proof assistants and generators (CiMPA, CiMPG, CiMPG+F, IPSG) as the way to turn the semi-formal scores into checked proofs. The paper does not claim proof scores are fully automatic; it claims they are flexible, widely applicable, and, with the new generators, formally redeemable.","pith_inferences":["A practical consequence the paper leaves implicit: any change to a specification invalidates its proof scores, so versioning and regression support for proof scores would be as important as the proofs themselves.","The same architecture could in principle be transplanted to other executable specification languages with a rewriting semantics and a completeness theorem, making the underlying order-sorted equational logic the real exportable asset rather than any single tool.","The mutation-style test of deleting a case split from a finished proof score would give a quantitative measure of how much confidence proof scores actually provide, and would make the paper's coverage caveat concrete for practitioners.","Combining rewrite-based proof scores for invariants with bounded searches for counterexamples on finite instances would probably catch most coverage errors early, even before a formal proof is regenerated."],"forward_implications":["If proof scores are as sound as the survey argues, the accumulated verifications of mutual exclusion, authentication, e-commerce, TLS, and post-quantum protocols amount to a real body of verified results rather than illustrative executions.","Because the proof language is the specification language, the method removes a classic adoption barrier: a specifier can prove properties of a system without learning a separate proof syntax.","The generator tools close the admitted soundness gap: a manual proof score can be lifted to a checked proof-assistant script, so semi-formality is a feature of the workflow, not an irreparable flaw.","Automated case splitting and lemma instantiation, as implemented in the newer generators, move the human burden from proof bookkeeping to lemma conjecture and strategy.","The survey's proposed next steps—narrowing for symbolic simplification, SMT integration, IDE support, and application to quantum and blockchain protocols—follow directly once the coverage machinery is in place."],"supporting_citations":[{"why":"It supplies the original definition of proof scores as declarations and rewritings whose successful evaluation solves the theorem-proving problem.","marker":"[68]"},{"why":"It establishes the formal principles of proof scores in CafeOBJ, grounding the methodology in algebraic specification.","marker":"[56]"},{"why":"It provides the completeness theorem for order-sorted equational deduction, which is the theoretical basis for treating rewrite-based evaluation as proof.","marker":"[75]"},{"why":"It supplies the operational semantics of term rewriting that proof-score reductions rely on.","marker":"[71]"},{"why":"It introduces the OTS/CafeOBJ method, the practical framework in which most of the surveyed proof-score verifications are conducted.","marker":"[128]"},{"why":"It describes the proof generator that reconstructs formal proof-assistant scripts from manual proof scores, directly addressing the soundness gap.","marker":"[146]"},{"why":"It demonstrates the approach on TLS 1.2 with automatically generated proof scores, serving as a recent success story and a benchmark for automation.","marker":"[167]"}],"fun_headline_variants":["Proof scores: verification written in the spec's own language","Proof scores: sound proofs by rewriting specifications","Rewrite to true: the proof-score verification method","Proof scores: formal verification that matches your spec","Proof scores: adopting the spec's syntax for proof"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything rests on the user's having written every necessary case split and induction hypothesis; a missed subgoal simply goes unnoticed by the tools.","fun_headline_variants_meta":{"raw":{"variants":["Proof scores: verification written in the spec's own language","Proof scores: sound proofs by rewriting specifications","Rewrite to true: the proof-score verification method","Proof scores: formal verification that matches your spec","Proof scores: adopting the spec's syntax for proof"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000224,"raw_usage":{"total_tokens":1455,"prompt_tokens":934,"completion_tokens":521,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":448}},"tokens_in":550,"tokens_out":521,"duration_ms":4918,"temperature":1.0,"reasoning_tokens":448,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T11:45:40.406345+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a published proof score for Qlock, delete one entire open-close environment corresponding to a case split, and run the remaining environments. The survey's own caveat predicts that no tool will complain and the remaining reductions will all return true; if a tool or a regenerated formal proof instead flags the missing case, the coverage gap is narrower than claimed, and if it silently passes, the coverage assumption is confirmed exactly.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It supplies the original definition of proof scores as declarations and rewritings whose successful evaluation solves the theorem-proving problem."},{"cited_title":"Goguen and Grant Malcolm","cited_arxiv_id":null,"evidence_quote":"It provides the completeness theorem for order-sorted equational deduction, which is the theoretical basis for treating rewrite-based evaluation as proof."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It introduces the OTS/CafeOBJ method, the practical framework in which most of the surveyed proof-score verifications are conducted."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It describes the proof generator that reconstructs formal proof-assistant scripts from manual proof scores, directly addressing the soundness gap."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It demonstrates the approach on TLS 1.2 with automatically generated proof scores, serving as a recent success story and a benchmark for automation."}],"review_version":1}