Pith. sign in

REVIEW 1 major objections 4 minor 23 references

A Python front-end to Why3 can verify that hypothesis tests and meta-analyses are used under the assumptions they actually require.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

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.

T0 review reviewed 2026-07-11 challenge →

load-bearing objection 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. the 1 major comments →

arxiv 2607.03951 v1 pith:VDE4AW6A submitted 2026-07-04 cs.SE cs.AIcs.LOcs.PL

Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python

Akira Tanaka , Yusuke Kawamoto This is my paper
classification cs.SE cs.AIcs.LOcs.PL
keywords formal verificationWhy3Pythonhypothesis testingmeta-analysisBelief Hoare logicstatistical programsprogram verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

Core claim

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.

What carries the argument

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.

Load-bearing premise

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.

What would settle it

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.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

1 major / 4 minor

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.

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 (1)
  1. 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.
minor comments (4)
  1. 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.
  2. 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.
  3. 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.
  4. 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.

Circularity Check

0 steps flagged

No significant circularity; tool paper whose verification outcomes are external SMT checks on user annotations, not self-derived predictions.

full rationale

This is a systems/tool paper (Why3-py front-end + StatWhy 1.4 meta-analysis modules) whose central claims are engineering: a mypy-assisted translation of annotated Python into WhyML, contract-based abstraction of SciPy/statsmodels, and generation of VCs discharged by independent SMT solvers (cvc5). Success or failure of verification is an external check against user-supplied requires/ensures clauses and hand-written library contracts, not a numerical constant or statistical quantity fitted from the same data being “predicted.” Self-citations to the authors’ prior BHL/StatWhy papers supply the logical foundation (belief modalities, Gospel annotations) but are not load-bearing uniqueness theorems that force the present results by construction; the paper does not redefine a quantity as its own prediction, smuggle an ansatz via self-citation, or rename a known empirical pattern. The acknowledged soft spot (fidelity of library contracts) is a modular-verification limitation, not circularity. Derivation chain is therefore self-contained against external solvers and benchmarks; steps array left empty.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 2 invented entities

The central claim rests on the soundness of the Why3 platform, the correctness of mypy’s type reconstruction for the supported subset, the fidelity of the hand-written library contracts, and the earlier Belief Hoare Logic / StatWhy foundation. No numeric free parameters are fitted; the only “invented” entities are the tool itself and its contract library, both of which are software artifacts rather than physical postulates.

axioms (4)
  • standard math Why3’s VC generation and the underlying SMT solvers are sound for the WhyML fragment used by the front-end.
    Invoked throughout Section 4; the paper never re-proves Why3.
  • domain assumption mypy’s static type information is a sound over-approximation of the runtime types of the supported Python subset.
    Section 4 “Handling Dynamic Typing”; required for the translation of arithmetic operators and function calls.
  • ad hoc to paper The logical contracts written for SciPy/statsmodels and for the meta-analysis combiners correctly capture every precondition that the real implementations rely on.
    Section 4 “Verification with External Libraries”; these contracts are new and not independently verified against the library source.
  • domain assumption Belief Hoare Logic correctly models the epistemic content of statistical hypothesis testing and p-value combination.
    Background Section 2 and all StatWhy modules; inherited from the authors’ earlier papers.
invented entities (2)
  • Why3-py front-end (mixed Python–WhyML parser + type-directed translation) independent evidence
    purpose: Bridge Python statistical programs into Why3 so that existing provers can be applied.
    The entire contribution; independent evidence is the public GitHub artifact and the case studies that exercise it.
  • StatWhy 1.4 meta-analysis contract modules (Fisher, Stouffer, Mantel-Haenszel, publication-bias predicates) independent evidence
    purpose: Supply the logical obligations that make missing assumptions detectable.
    New library content; independent evidence is the same public repository and the failing/succeeding examples.

reviewed 2026-07-11 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python." pith.science (2026). https://pith.science/paper/VDE4AW6A

@misc{pith2026260703951,
  author       = {Pith},
  title        = {Pith review of: Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VDE4AW6A}},
  note         = {Machine review of arXiv:2607.03951}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

The reproducibility crisis in scientific research has received widespread recognition, thereby increasing the importance of meta-analyses that integrate statistical analyses from multiple studies. However, statistical methods often have ambiguous and implicit underlying assumptions, which can lead to their erroneous applications and interpretations. To address this issue, we propose a formal verification framework for statistical programs written in Python. Specifically, we present Why3-py, a Python front-end for the Why3 verification platform that transforms Python programs into verification-oriented WhyML representations suitable for formal verification, addressing the challenges arising from Python's dynamic typing and runtime polymorphism. Furthermore, we extend the StatWhy tool to support the verification of meta-analysis methods. These tools enable users to identify overlooked assumptions and misuse of analyses, and to verify the correctness of Python programs for hypothesis testing and for meta-analyses.

Figures

Figures reproduced from arXiv: 2607.03951 by Akira Tanaka, Yusuke Kawamoto.

Figure 1
Figure 1. Figure 1: A Python code that uses Fisher’s method for computing a meta-analytic [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The overview of the construction of the Why3-py tool. ification layer is written in comments prefixed by #@. A programmer specifies the requirements and the interpretation of this function by annotating the pro￾gram with the precondition in the requires clause and the postcondition in the ensures clause using Gospel. The Why3-py tool then parses these comments and generates VCs, which are discharged by Why… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 2 linked inside Pith

  1. [1]

    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: De- ductive Software Verification - The KeY Book - From Theory to Practice (2016)

    2016

  2. [2]

    Philosophical Transactions of the Royal SocietyofLondon27(328),186–190(1710).https://doi.org/10.1098/rstl.1710.0011

    Arbuthnot, J.: An argument for divine providence, taken from the constant regu- larity observ’d in the births of both sexes. Philosophical Transactions of the Royal SocietyofLondon27(328),186–190(1710).https://doi.org/10.1098/rstl.1710.0011

    doi:10.1098/rstl.1710.0011

  3. [3]

    Charguéraud, A., Filliâtre, J., Lourenço, C., Pereira, M.: GOSPEL - providing ocamlwithaformalspecificationlanguage.In:FM’19.pp.484–501.Springer(2019)

    2019

  4. [4]

    GitHub repository (2020), https://github.com/arsalan0c/dafny-of-python

    Choudhury, A.: dafny-of-python: A tool for deductive verification of Python pro- grams. GitHub repository (2020), https://github.com/arsalan0c/dafny-of-python

    2020

  5. [5]

    In: SEFM’12

    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - A software analysis perspective. In: SEFM’12. pp. 233–247 (2012)

    2012

  6. [6]

    In: Proc

    Eilers, M., Müller, P.: Nagini: A static verifier for python. In: Proc. CAV 2018, Part I. LNCS, vol. 10981, pp. 596–603. Springer (2018)

    2018

  7. [7]

    In: ESOP’13

    Filliâtre, J., Paskevich, A.: Why3 - where programs meet provers. In: ESOP’13. LNCS, vol. 7792, pp. 125–128. Springer (2013)

    2013

  8. [8]

    In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy

    Kawamoto, Y.: Statistical epistemic logic. In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. LNCS, vol. 11760, pp. 344–362. Springer (2019)

    2019

  9. [9]

    In: Proc

    Kawamoto, Y.: Towards logical specification of statistical machine learning. In: Proc. SEFM 2019. pp. 293–311 (2019)

    2019

  10. [10]

    Software and Systems Modeling20(2), 293–310 (2020)

    Kawamoto, Y.: An epistemic approach to the formal specification of statistical machine learning. Software and Systems Modeling20(2), 293–310 (2020)

    2020

  11. [11]

    Kawamoto, Y., Kobayashi, K., Suenaga, K.: User Documentation for StatWhy v1.4 (2026), available at https://github.com/fm4stats/statwhy

    2026

  12. [12]

    In: Proc

    Kawamoto, Y., Sato, T., Suenaga, K.: Formalizing statistical beliefs in hypothesis testing using program logic. In: Proc. KR’21. pp. 411–421 (2021)

    2021

  13. [13]

    In: Proc

    Kawamoto, Y., Sato, T., Suenaga, K.: Formalizing statistical causality via modal logic. In: Proc. JELIA’23. LNCS, vol. 14281, pp. 681–696. Springer (2023)

    2023

  14. [14]

    Kawamoto, Y., Sato, T., Suenaga, K.: Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs. Artif. Intell.326, 104045 (2024)

    2024

  15. [15]

    Lehtosalo, J., van Rossum, G., Levkivskyi, I., Sullivan, M.J.: mypy: Static typing for python (2026), https://github.com/python/mypy

    2026

  16. [16]

    In: LPAR’16

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR’16. LNCS, vol. 6355, pp. 348–370. Springer (2010)

    2010

  17. [17]

    In: ICSE ’13

    Leino, K.R.M.: Developing verified programs with dafny. In: ICSE ’13. pp. 1488–

  18. [18]

    IEEE Computer Society (2013)

    2013

  19. [19]

    arXiv preprint arXiv:2501.06283 (2025)

    Li, Y.C., Zetzsche, S., Somayyajula, S.: Dafny as verification-aware intermediate language for code generation. arXiv preprint arXiv:2501.06283 (2025)

    Pith/arXiv arXiv 2025

  20. [20]

    CoRRabs/2508.08171(2025)

    Orvalho, P., Kwiatkowska, M.: Pyveritas: On verifying Python via LLM-based transpilation and bounded model checking for C. CoRRabs/2508.08171(2025)

    Pith/arXiv arXiv 2025

  21. [21]

    In: Proc

    Pereira, M., Ravara, A.: Cameleer: A deductive verification tool for OCaml. In: Proc. CAV 2021, Part II. LNCS, vol. 12760, pp. 677–689. Springer (2021)

    2021

  22. [22]

    Régis-Gianas, Y., Jeannerod, N., Treinen, R.: Morbig: A static parser for POSIX shell. J. Comput. Lang.57, 100944 (2020)

    2020

  23. [23]

    Tanaka, A., Kawamoto, Y.: User Documentation for Why3-py v1.0 (2026), avail- able at https://github.com/fm4stats/why3-py

    2026

This paper was first reviewed by grok-4.5 on July 11, 2026.