1 Introduction↩︎

The reproducibility crisis in scientific research has drawn increasing attention to the trustworthiness of statistical analyses, particularly meta-analyses that aggregate evidence from multiple studies. However, the correctness of statistical analyses is fundamentally different from that of conventional programs. Statistical methods crucially rely on assumptions about data-generating processes, such as distributional properties on unobservable true populations, which cannot be verified solely from the program and observed data. As a result, statistical programs may produce seemingly plausible outputs while being based on inappropriate or missing assumptions, leading to incorrect scientific conclusions.

This issue is exacerbated in practice by the widespread use of Python and its scientific libraries, which make it easy to apply statistical methods without explicitly stating their assumptions. However, existing program verification techniques focus on functional correctness and do not capture the assumption-dependent nature of statistical reasoning or the usage of external libraries.

To address this gap, we propose a formal verification framework for Python statistical programs, based on explicit specifications of assumptions and interpretations. Specifically, we present Why3-py, a Python front end for the Why3 platform that transforms annotated Python code into , and an extension of StatWhy for specifying and verifying meta-analysis code. Importantly, our goal is not to verify implementations, but to ensure correct use under appropriate assumptions and interpretations, e.g., detecting incorrect integration of \(p\)-values in meta-analysis.

Contributions. Our main contributions are summarized as follows:

• We present Why3-py, a formal verification tool for Python statistical code.

• We extend StatWhy with specifications for meta-analysis methods and show how our approach detects missing assumptions and misuse of meta-analyses.

These tools are available with a range of examples and documentation [@Tanaka:26:manual:why3-py; @Kawamoto:26:UD]. To the best of our knowledge, this is the first approach to formally verifying Python statistical code. Furthermore, this approach is not limited to specific branch of statistics, but can be applied to any situation where analysts and meta-analysts wish to verify the use of statistical methods in python code. This would be the first step in developing a framework to verify the integrity of scientific conclusions.

Related Work. Logic for Statistics. Modal logic has been employed to express statistical properties [@Kawamoto:19:FC; @Kawamoto:23:JELIA]. The work on statistical epistemic logic [@Kawamoto:19:FC; @Kawamoto:19:SEFM; @Kawamoto:20:SoSyM] is the first attempt to define a modal logic to describe properties of statistical methods. Belief Hoare logic (BHL). [@Kawamoto:21:KR; @Kawamoto:24:AIJ] is a program logic equipped with a modal operator for statistical belief. Based on BHL, the StatWhy tool automatically verifies whether a programmer has appropriately annotated a program with the requirements for hypothesis testing and the interpretation of the test results.

Program Verification Tools. Deductive program verification aims to check a program’s correctness by proving that the program satisfies its formal specification. Various tools have been developed to statically verify the correctness of programs; e.g., Why3 [@Filliatre:13:ESOP] for OCaml, Dafny [@DBLP:conf/lpar/Leino10] for imperative programs that compile into Boogie; Frama-C [@DBLP:conf/sefm/CuoqKKPSY12] for C programs; KeY [@KeYBook2016] for Java programs.

Verification of Python Programs. Formal verification of Python programs remains relatively underexplored compared to statically typed languages, such as C, Java, and OCaml. Nagini [@Eilers:18:Nagini] provides automated verification for a statically-typed subset of Python, based on the Viper intermediate verification infrastructure. The PyVeritas tool translates Python programs into C to apply bounded model checking [@Orvalho:25:pyveritas]. Why3 itself provides a front end for micro-Python, a minimal subset of Python programs for an education purpose that does not include real numbers or strings. Several tools translate Python into Dafny [@Leino:13:dafny; @Li:25:dafny_intermediate; @dafny_of_python_tool]. However, these approaches require restrictive subsets of Python and precise semantic modeling. In contrast, our approach supports practical Python statistical programs by combining type reconstruction and abstraction of external libraries, enabling scalable verification.

2 Background↩︎

Statistical hypothesis testing. Hypothesis testing [@Arbuthnot:1710] determines whether observed data provide sufficient evidence to support a claim called an alternative hypothesis. In a hypothesis test, the alternative hypothesis usually claims that there is an effect or relationship between variables, whereas the corresponding null hypothesis represents a claim that there is no effect or no relationship. The purpose of hypothesis testing is to assess whether the available evidence is sufficient to reject the null hypothesis in favor of the alternative hypothesis. This assessment uses a \(p\)-value, which quantifies how unlikely the observed data has been generated under the assumption that the null hypothesis is true. The null hypothesis is rejected if the \(p\)-value is smaller than a threshold, e.g., \(0.05\).

The correctness of a statistical program crucially depends on assumptions about the data-generating process; e.g., many hypothesis testing methods assume that a population should follow a normal distribution. However, such assumptions are inherently unverifiable from the program and observed data, as they concern properties about an unknown true population which we can only partially and empirically learn from data. Consequently, the correctness of statistical programs cannot be derived only from formally provable assertions.

Belief Hoare logic (BHL). To address this limitation, belief Hoare logic (BHL) [@Kawamoto:21:KR; @Kawamoto:24:AIJ] is designed as a program logic equipped with epistemic modal operators for the statistical beliefs acquired by hypothesis testing. The epistemic logic used in BHL is defined by: \(\varphi\,\mathbin{::=}\,\, \eta \mid \neg \varphi\mid \varphi\land \varphi\mid \mathbf{K}\varphi \mid \mathop{\mathbf{K}^{\le \epsilon}_{y, A}} \varphi\) for an atomic formula \(\eta\), a dataset \(y\), a hypothesis test \(A\), and a \(p\)-value \(\epsilon\). Intuitively, \(\mathbf{K}\varphi\) represents that we know \(\varphi\). The knowledge modality \(\mathbf{K}\) is defined as the box operator in the S5 modal logic system. Since the result of the hypothesis test may be wrong, we use the statistical belief modality \(\mathop{\mathbf{K}^{\le 0.05}_{y, A}}\) instead of the knowledge modality \(\mathbf{K}\). \(\mathop{\mathbf{K}^{\le \epsilon}_{y, A}} \varphi\) represents that by a hypothesis test \(\mathit{A}\) on a dataset \(y\), we believe \(\varphi\) with a \(p\)-value \(\alpha \le \epsilon\). The satisfaction of a formula \(\varphi\) in a possible world \(w\) is denoted by \(w \models \varphi\) and is defined straightforwardly in a Kripke model.

In BHL, we describe a procedure for hypothesis testing as a program \(C\). We then describe the requirements for the hypothesis tests as a precondition formula \(\psi_{{\sf pre}}\), e.g., representing that a dataset has been sampled from a uniform distribution. We also specify the statistical belief acquired by the hypothesis test as a postcondition formula \(\varphi_{{\sf post}}\); e.g., \(\mathop{\mathbf{K}^{\le 0.05}_{y, A}}\! \varphi\) denotes that by a hypothesis test \(\mathit{A}\) on a dataset \(y\), we believe an alternative hypothesis \(\varphi\) with a \(p\)-value \(\alpha \le 0.05\).

Finally, we describe the whole inference as a judgment \(\Gamma\vdash\{ \psi_{{\sf pre}}\}\ C \ \{ \varphi_{{\sf post}}\}\), representing that whenever the precondition \(\psi_{{\sf pre}}\) is satisfied, the execution of the program \(C\) results in the satisfaction of the postcondition \(\varphi_{{\sf post}}\). By deriving this judgment using derivation rules in BHL, we conclude that the program \(C\) results in the statistical belief \(\varphi_{{\sf post}}\) whenever the requirement \(\psi_{{\sf pre}}\) is satisfied.

In this framework, specifications may include both verifiable properties and assumption-based statements, which are interpreted as beliefs about the underlying data-generating process. This allows for a clear separation between (i) properties that can be formally verified through deductive reasoning and (ii) assumptions that must be justified empirically or externally.

Deductive program verification for statistical programs. Using BHL as a theoretical foundation, StatWhy provides a verification framework for statistical programs. Given an OCaml program annotated with a formal specification written in the Gospel language [@Chargueraud:19:FM], StatWhy verifies whether a programmer has appropriately annotated the program with the specification, i.e., the requirements for hypothesis testing and the interpretation of the test results. StatWhy’s implementation is based on the Why3 verification platform [@Filliatre:13:ESOP] and the Cameleer [@Pereira:20:CAV] tool using the language, which integrates programming constructs with formal specifications expressed in terms of preconditions and postconditions.

Importantly, this approach attempts not to prove the validity of statistical assumptions, but to ensure that such assumptions are explicitly annotated, hence preventing the misuse and misinterpretation of statistical methods. However, there remains a significant gap between the Why3 platform and statistical programming practice, where Python and its rich libraries are widely used.

3 Motivating Example: Meta-Analysis in Python↩︎

Meta-analysis of harm using Fisher’s method. To illustrate the main idea of the Why3-py tool, consider a meta-analysis in which analysts obtain multiple \(p\)-values, each corresponding to evidence from an independent study on the harm of a medicine, and then combine them into a single \(p\)-value that captures the accumulated evidence of harm using Fisher’s method. In this setting, the goal of formal verification is not to prove the correctness of the implementation of Fisher’s method itself, but rather to verify that the program uses Fisher’s method appropriately to detect the harm of the medicine.

Structure of the code. In Fig. 1, we show a Python code that calls a function for Fisher’s method exec_combine_pvs_fisher, which uses SciPy’s function to compute a meta-analytic \(p\)-value res from independent \(p\)-values pv1, pv2, and pv3. This code consists of two intertwined layers. The executable layer is a Python program that calls the function exec_combine_pvs_fisher. The specification layer is written in comments prefixed by #@. A programmer specifies the requirements and the interpretation of this function by annotating the program 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 Why3. Thus, the same code serves as both an executable Python program and a formally specified verification target.

Details of the code. Although this example has a very simple program structure, its correctness depends on several assumptions, including non-trivial ones. In the precondition, the formula \(\texttt{pvalues pvs}\) checks that \(\texttt{pvs}\) is a list of \(p\)-values, i.e., real numbers over \([0, 1]\). \(\texttt{intend\_to\_detect\_excess\_of\_small\_pv}\) indicates that the meta-analyst intends to detect an excess of small \(p\)-values, which is assumed for Fisher’s method. The formula \(\texttt{indicate\_risk}\) specifies the analyst’s decision rule, which stipulates that observing harm in one of the three experimental situations (denoted by Impl disj_exps observe_harm) lead to reporting a risk. Finally, the postcondition states that the output \(\texttt{result}\) is a \(p\)-value, and that by combining the three \(p\)-values using Fisher’s method, we obtain a statistical belief that the alternative hypothesis \(\texttt{indicate\_risk}\) holds with the combined \(p\)-value \(\texttt{res}\) in the current world \(\texttt{(World !st interp)}\) equipped with a hypothesis testing record \(\texttt{st}\) and an interpretation \(\texttt{interp}\) of private variables.

Program verification and error detection. Given this Python code, the Why3-py tool verifies whether the meta-analysis method is appropriately used by translating it into , generates verification conditions (VCs) using Why3 and StatWhy 1.4, and discharge them using SMT solvers, e.g., cvc5. Then Why3-py fails to verify this code owing to missing requirements in the annotation. However, it helps identify the missing requirements by analyzing undischarged VCs. For instance, analysts can easily identify the missing requirement that the three \(p\)-values should not be collected under publication bias (i.e., the phenomenon that studies reporting statistically significant results are more likely to be published). Importantly, such missing requirements do not manifest as runtime failures and are therefore difficult to detect in practice without verifying the specification annotated in the code.

4 Extending Why3 to Statistical Programs in Python↩︎

Challenges in verifying Python statistical programs. Although the Why3 platform is a powerful framework for deductive verification, it is not directly applicable to Python statistical programs. Specifically, the micro-Python plugin for Why3 has limited expressiveness and lacks support for real arithmetic and calls to external scientific libraries, which are crucial for statistical programming.

To address these limitations, we extend Why3 to support the verification of Python programs that rely on statistical libraries, such as SciPy and statsmodels. Our approach is based on the following key ideas. First, we redesign the Python plugin to support a richer subset of Python and to integrate it seamlessly with Why3’s verification engine. Second, we incorporate static type information obtained from a type checker to bridge the gap between Python’s dynamic typing and , which is a statically typed language. Third, we model statistical functions and external library calls using logical specifications, enabling the verification of their correct usage. Finally, we extend StatWhy modules to the specification of meta-analyses to integrate \(p\)-values from multiple studies. Through these extensions, our framework Why3-py enables analysts to verify the correctness of Python programs for hypothesis testing and for meta-analyses.

A Python Front End for Why3. The Why3-py tool (Fig. 2) provides a new Python front end based on Why3 1.8.0 that targets a subset of Python programs which can be statically analyzed using  [@Lehtosalo:mypy], a static type checker for Python. Unlike the original micro-Python plugin, which relied on a plugin-specific, minimally expressive specification language, our tool supports writing logical specifications in the full language within Python code. This is achieved by embedding expressions in comments of the Python code. In addition, our Python front end supports real number arithmetic, which is essential for statistical programs. It also translates Python-specific constructs, such as keyword arguments, into the appropriate representations. These design decisions are motivated by the need to support expressive constructs for statistical reasoning. As a result, the new front end is not backward-compatible, but significantly improves the expressiveness of the specification for Python code.

Handling Dynamic Typing. Python’s dynamic typing poses a significant challenge when translating programs into , which requires explicit, static type information. Our approach addresses this issue by using for static type checking and inference as a preprocessing step. Specifically, the verification pipeline first applies to the input Python code and uses the resulting type information to parse and construct the abstract syntax tree (AST). This type information is essential for resolving ambiguities in Python syntax. For instance, Python uses the same operator for both integer and real arithmetic, whereas distinguishes between them. Leveraging such type information, Why3-py translates Python operators into the appropriate operators, ensuring the correct handling of numeric computations. By restricting the input language to a subset of Python analyzable by , Why3-py enables sound and tractable verification while still covering a wide range of practical Python programs.

Parsing a Mixed Python– Language To support the embedding of specifications within Python code, we design a custom parser that can handle a mixed Python- language. Since Python and have fundamentally different lexical structures, standard parsing techniques are insufficient. Similar difficulties have been observed in other languages with context-dependent syntax, such as POSIX shell, where parsing is intertwined with complex syntax and conventional parsing pipelines become inadequate [@Regis-Gianas:20:vlc]. For this reason, Why3-py relies on Menhir’s incremental parsing API, which allows tokens to be supplied dynamically from multiple lexers. Specifically, the system maintains both a Python lexer and a lexer, while using a single parser to process tokens from both sources and managing input through a shared lexing buffer that stores the entire program in memory. This enables the backtracking of lexing and parsing, namely, the parser first attempts to interpret input as Python code, and if parsing fails, it resets the input position and reinterprets the same fragment as . This design allows seamless switching between the two languages within a single source file.

Translation to After parsing, the constructed Python AST is translated into a AST. In this translation, Python function calls are mapped to corresponding function calls, and keyword arguments are translated into record constructions. Logical expressions embedded in Python are directly represented as terms.

Verification with External Libraries. External libraries, such as SciPy, cannot be directly verified using Why3. To address this limitation, we adopt a specification-based abstraction approach in Why3-py. Instead of modeling the implementations of external functions, we associate them with logical contracts that describe their behavior and are formalized in our new StatWhy 1.4 modules. Then verification is performed under the assumption that these contracts are satisfied. This approach allows us to reason about the correctness of how library functions are used, rather than their internal implementation details. As a result, Why3-py supports modular verification of Python statistical programs that depend on external scientific libraries.

Scope of Supported Python Code. Why3-py targets a subset of Python programs that can be statically analyzed using . This includes numerical computations, control-flow constructs, and calls to external libraries for which specifications are provided. However, programs relying heavily on dynamic features such as dynamically constructed data structures are currently outside the scope of our approach.

5 Case Studies and Performance Evaluation↩︎

Detections of incorrect requirements for meta-analyses. Our StatWhy 1.4 supports the specification of various meta-analysis methods, including Fisher’s method, Stouffer’s method, and Mantel-Haenszel’s method. Relying on these specifications, our Why3-py tool can verify Python meta-analysis code and detect various incorrect requirements. One of the important requirements is the absence of publication bias, as discussed in Sect. 3. To verify the correct use of meta-analysis methods, analysts need to annotate the code with the requirement sampled d uniform_pv. If this requirement is missing in the precondition, then Why3-py detects that this formula cannot be proven, indicating that analysts cannot reliably apply Fisher’s method under publication bias.

Detections of \(p\)-hacking in multiple comparison. Why3-py can also be applied to Python hypothesis testing code, including multiple comparisons within a single study. Such settings may involve \(p\)-hacking, where multiple hypotheses are tested simultaneously and \(p\)-values are selectively reported or manipulated, which can lead to incorrect scientific conclusions. By annotating Python code with its specification and verifying it using Why3-py, analysts can detect incorrect requirements and interpretations of \(p\)-values, including \(p\)-hacking.

Scalability of Why3-py. We evaluated the performance of the verification of Python code using Why3-py and StatWhy 1.4 to (i) the number of \(p\)-values integrated in meta-analyses and (ii) the larger number of compared groups in multiple comparison. For the evaluation, we conducted experiments using the SMT solver cvc5 1.1.2 on a ThinkPad 480s equipped with Debian GNU/Linux 13, an Intel Core i7-8650U processor, and 24 GB of memory. The execution times of the verification of the Python code computing \(p\)-values using each meta-analysis method are within 8 seconds for practical numbers (e.g., 2 to 30) of studies.

The execution times of the verification of the Python code for multiple comparison are shown in Table ¿tbl:tab:multiple-comparison-methods?. Although the number of comparisons between groups grows rapidly with the number of groups, the verification of these programs is efficient for the practical numbers of groups.

6 Conclusion↩︎

We proposed a formal verification framework for Python statistical programs. Specifically, we developed the formal verification tool Why3-py for Python statistical programs, and extended the StatWhy library to support the specification of meta-analysis methods. To the best of our knowledge, this is the first approach to formally verifying Python code for hypothesis testing and for meta-analyses.