{"id":"091b782f-8fc5-430a-a568-647045c2f7c3","arxiv_id":"2607.03951","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Why3-py is a Python front-end to Why3 plus an extended StatWhy that verifies annotated hypothesis-testing and meta-analysis programs by discharging assumption and interpretation obligations.","lead":"Why3-py turns annotated Python statistics code into WhyML so automated provers can check that hypothesis tests and meta-analyses state their assumptions correctly. It gives scientists a practical way to catch silent misuse of p-values and combination methods that ordinary testing never reveals.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified beyond the reader's already-noted contract-fidelity limitation.","rationale":"The reader's strongest claim accurately restates the paper's contribution and is backed by the concrete examples, performance data, and released artifact. The weakest assumption the reader isolates—fidelity of the hand-written SciPy/statsmodels and meta-analysis contracts—is indeed the single most load-bearing point; nothing in the manuscript supplies a stronger technical vulnerability. Because that limitation is standard for the verification style the authors adopt and is already reflected in the reader's low correctness_risk and ACCEPT verdict, no adjustment is warranted. The concrete test above simply operationalizes the claim the authors already make about detecting missing requirements, providing an independent reproducibility check without altering the evaluation.","tokens_in":8599,"tokens_out":557,"duration_ms":4917,"concrete_test":"Take the Fisher meta-analysis example of Fig. 1 / §3; deliberately omit the publication-bias precondition (sampled d uniform_pv) while leaving all other annotations intact, re-run Why3-py + StatWhy 1.4 + cvc5, and confirm that at least one VC remains undischarged and that the tool's residual goals point to the missing formula. Then restore the precondition and confirm all VCs discharge within the reported ~8 s bound. Success of both directions corroborates the detection claim under the stated contracts.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that Why3-py + StatWhy 1.4 can automatically detect missing assumptions and certain misuses of hypothesis tests and common p-value combiners (Fisher, Stouffer, Mantel-Haenszel) on realistic, mypy-checkable Python code that calls SciPy/statsmodels. That claim is supported by a concrete motivating example (Fig. 1 and §3), explicit detection of publication-bias and p-hacking omissions (§5), performance numbers for practical sizes (Table 1 and the 2–30-study meta-analysis timings), and a public artifact. The only load-bearing soft spot is exactly the one the reader already flags: the hand-written logical contracts for external library functions and combiners (Section 4, “Verification with External Libraries”). If a contract is incomplete or overly strong, verification can accept incorrect usage or reject correct usage. This is an inherent and acknowledged limitation of contract-based modular verification rather than an internal inconsistency or unsupported leap in the paper's argument. No stronger technical concern (soundness of the mixed Python–WhyML parser, type reconstruction via mypy, or the BHL encoding of meta-analysis) is evidenced by the manuscript.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper proposes Why3-py, a Python front-end for the Why3 platform that translates mypy-checkable, Gospel-annotated Python statistical programs into WhyML for automated verification of hypothesis-testing and meta-analysis code. It addresses Python’s dynamic typing via static type reconstruction, embeds full WhyML specifications in comments, abstracts external libraries (SciPy, statsmodels) by logical contracts, and extends StatWhy 1.4 with modules for Fisher’s, Stouffer’s and Mantel-Haenszel methods (including publication-bias predicates). The central claim is that the resulting framework can detect missing assumptions and certain misuses (e.g., p-hacking, publication bias) on realistic Python programs; this is illustrated by a motivating Fisher meta-analysis example, case studies that correctly fail or succeed according to the presence of required annotations, and performance numbers for practical problem sizes.","tokens_in":8928,"tokens_out":876,"duration_ms":15843,"significance":"If the claims hold, the work supplies the first practical, automated formal-verification path for Python statistical code that is actually used by analysts, directly addressing a recognised source of the reproducibility crisis. Concrete strengths that raise the contribution above a pure engineering exercise are: (i) a public artifact containing the tool, documentation and examples; (ii) machine-checked verification conditions discharged by independent SMT solvers rather than by hand; (iii) explicit detection of non-runtime errors such as omitted publication-bias assumptions; and (iv) timing data (Table 1 and the 2–30-study meta-analysis experiments) showing that verification remains feasible for the sizes that appear in practice. The contract-based treatment of libraries is a pragmatic enabler of modularity, even though it shifts the soundness burden onto the contracts themselves.","major_comments":[{"comment":"Section 4 (“Verification with External Libraries”) and the corresponding StatWhy 1.4 modules: the soundness of every verification result rests on the hand-written logical contracts for SciPy/statsmodels functions and for the meta-analysis combiners. The paper correctly notes that only usage, not implementation, is checked, yet it provides no systematic evidence (cross-checks against library documentation, differential testing, or a contract-validation suite) that the contracts are neither incomplete nor overly strong. Because an incomplete contract can accept incorrect usage and an overly strong one can reject correct usage, this is a load-bearing assumption for the central claim that “overlooked assumptions and misuse” are reliably identified; a short validation subsection or appendix would make the claim substantially more robust.","section":null}],"minor_comments":[{"comment":"Throughout the manuscript (especially the abstract and §§1–3) many words are concatenated without spaces (“widespreadrecognition”, “meta-analysesthat”, “Why3-pytool”, etc.). These appear to be transcription artefacts; they should be corrected for readability.","section":null},{"comment":"Table 1, Tukey HSD row for 7 groups: the reported time “87,86” uses a comma as decimal separator inconsistently with the rest of the table; standardise to a period.","section":null},{"comment":"Figure 2 is referenced but never described beyond the caption “overview of the construction”; a one-sentence walk-through of the pipeline stages would help readers who cannot consult the artifact immediately.","section":null},{"comment":"Related-work discussion of other Python verifiers (Nagini, PyVeritas, dafny-of-python) is accurate but could briefly note which of them already support real arithmetic or external-library contracts, clarifying the precise novelty of Why3-py’s design choices.","section":null}],"recommendation":"minor_revision","confidential_remarks":"The paper is a solid tool contribution that fits a software-engineering or formal-methods venue well. The only novelty-risk is that the core logical framework (BHL + StatWhy) is already published; the present manuscript’s value lies almost entirely in the Python front-end and the meta-analysis modules. Provided the contract-validation point is addressed, I see no reason to reject."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This is a solid tool paper that delivers something usable. The new piece is Why3-py: a real Python front-end for Why3 that handles mypy types, real arithmetic, keyword arguments, and a mixed Python–WhyML parser, plus the StatWhy 1.4 modules that give contracts for Fisher, Stouffer, Mantel-Haenszel and the usual meta-analysis side-conditions. Prior work already had BHL, StatWhy for OCaml, and various Python verifiers; the combination that can discharge (or fail on) realistic SciPy-using meta-analysis code is new.\n\nWhat it does well is concrete. The motivating example (Fig. 1) fails cleanly when publication bias is omitted and succeeds when the right predicates are present. Section 5 shows the same for p-hacking in multiple comparisons. Timings stay under a few tens of seconds for practical sizes (2–30 studies, up to 7 groups). The artifact is public. The translation story (mypy preprocessing, Menhir dual-lexer, contract abstraction of external libraries) is described carefully enough that a referee can check it.\n\nThe soft spot is exactly the one the reader already flagged: the hand-written logical contracts for SciPy/statsmodels and the combiners. If a contract is incomplete or too strong, you get false accepts or false rejects. That is the standard limitation of modular contract verification; the paper does not hide it. Nothing in the manuscript suggests the mixed parser or the BHL encoding itself is broken. Circularity is low—the VCs go to independent SMT solvers.\n\nThis is for people who already care about formal methods for statistics or about making meta-analysis code less error-prone. It will not rewrite statistics, but it gives a practical way to force the assumptions into the open. I would send it to peer review; the contribution is real and the evidence matches the claim. Worth engaging if you work on verification of scientific code or on meta-analysis tooling.","headline":"Working Python front-end + meta-analysis contracts that actually flag missing publication-bias and p-hacking assumptions; the only real soft spot is the usual hand-written library contracts.","tokens_in":9498,"tokens_out":495,"would_cite":true,"duration_ms":4211,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"A Python front-end to Why3 can verify that hypothesis tests and meta-analyses are used under the assumptions they actually require.","keywords":["formal verification","Why3","Python","hypothesis testing","meta-analysis","Belief Hoare logic","statistical programs","program verification"],"falsifier":"Take a published Python meta-analysis that is known to ignore publication bias or to misuse Fisher combination, annotate it with the paper's required contracts, and check whether Why3-py correctly reports the missing assumption and refuses verification.","tokens_in":9500,"feed_emoji":"✓","tokens_out":602,"duration_ms":4798,"temperature":0.7,"pith_summary":"Scientific code often applies hypothesis tests and meta-analyses without stating the assumptions those methods need, which is a major driver of unreproducible results. This paper presents Why3-py, a front-end that turns annotated Python statistical programs into WhyML so that Why3 can generate and discharge verification conditions. The same framework is extended with specifications for common p-value combination methods (Fisher, Stouffer, Mantel-Haenszel). The goal is not to prove that the library implementations are correct, but to force the programmer to declare the necessary preconditions and the intended statistical interpretation, then to check that those declarations are consistent. When a required assumption such as the absence of publication bias is missing, the verifier fails and the undischarged conditions point to the gap. The authors show that this works on realistic Python code that calls SciPy and statsmodels, and that verification finishes in seconds for practical numbers of studies or comparison groups.","feed_headline":"Python stats code can now be checked for missing assumptions","feed_subtitle":"Why3-py flags when Fisher or Stouffer combination is used without the conditions it needs","key_machinery":"Why3-py: a mixed Python/WhyML parser and translator that uses mypy type information, embeds full WhyML contracts inside Python comments, and replaces external library calls by logical contracts, so that Belief-Hoare-logic verification conditions can be generated and discharged by Why3.","core_discovery":"Why3-py together with the extended StatWhy modules is the first practical system that can automatically verify, for ordinary Python statistical programs, that the programmer has correctly annotated the assumptions and statistical interpretations required by hypothesis tests and by standard meta-analysis combiners.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Why3-py verifies Python stats code for missing assumptions","Formal checks catch invalid Fisher/Stouffer use in Python","Why3-py flags overlooked assumptions in hypothesis tests","Verify meta-analysis assumptions in ordinary Python code","Python hypothesis testing now checked for required conditions"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The hand-written logical contracts supplied for SciPy, statsmodels and the meta-analysis combiners must faithfully capture every precondition the real library functions rely on; if a contract is incomplete or too strong the verifier will either reject correct code or accept incorrect code.","fun_headline_variants_meta":{"raw":{"variants":["Why3-py verifies Python stats code for missing assumptions","Formal checks catch invalid Fisher/Stouffer use in Python","Why3-py flags overlooked assumptions in hypothesis tests","Verify meta-analysis assumptions in ordinary Python code","Python hypothesis testing now checked for required conditions"]},"model":"grok-4.5","effort":"low","cost_usd":0.004188,"raw_usage":{"total_tokens":1206,"prompt_tokens":666,"num_sources_used":0,"completion_tokens":78,"cost_in_usd_ticks":41880000,"prompt_tokens_details":{"text_tokens":666,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":462,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":666,"tokens_out":78,"duration_ms":12510,"temperature":1.0,"reasoning_tokens":462,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T22:47:10.216779+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Take a published Python meta-analysis that is known to ignore publication bias or to misuse Fisher combination, annotate it with the paper's required contracts, and check whether Why3-py correctly reports the missing assumption and refuses verification.","supporting_citations":[],"review_version":1}