# StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

arXiv: https://arxiv.org/abs/2405.17492 · HTML: https://mlsanity.com/paper/2405.17492/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 42 references that are in the map.
- First posted on arXiv 25 May 2024.

## Builds on (most cited first, 7 of 7)

- [PAC Verification of Statistical Algorithms](https://mlsanity.com/paper/2211.17096/) (2022)
- [Statistical Epistemic Logic](https://mlsanity.com/paper/1907.05995/) (2019)
- [Towards Logical Specification of Statistical Machine Learning](https://mlsanity.com/paper/1907.10327/) (2019)
- [An Epistemic Approach to the Formal Specification of Statistical Machine Learning](https://mlsanity.com/paper/2004.12734/) (2020)
- [Cameleer: a Deductive Verification Tool for OCaml (extended version)](https://mlsanity.com/paper/2104.11050/) (2021)
- [Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs](https://mlsanity.com/paper/2208.07074/) (2022)
- [Formalizing Statistical Causality via Modal Logic](https://mlsanity.com/paper/2210.16751/) (2022)

## Built on by (most cited first, 1 of 1)

- [Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python](https://mlsanity.com/paper/2607.03951/) (2026)

## Abstract (arXiv)

Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool StatWhy automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how StatWhy can be used to avoid common errors in various statistical hypothesis testing programs.