  Statistical methods have been widely misused and misinterpreted in various
scientific fields, raising significant concerns about the integrity of
scientific research. To develop techniques to mitigate this problem, we propose
a new method for formally specifying and automatically verifying the
correctness of statistical programs. In this method, programmers are reminded
to check the requirements for statistical methods by annotating their source
code. Then, a software tool called StatWhy automatically checks whether the
programmers have properly specified the requirements for the statistical
methods. This tool is implemented using the Why3 platform to verify the
correctness of OCaml programs for statistical hypothesis testing. We
demonstrate how StatWhy can be used to avoid common errors in a variety of
popular hypothesis testing programs.
