WHY3-PY

Why3-py is a modified version of the Why3 verification platform developed for Python statistical code. It supports the execution and verification of statistical Python programs.

The original Why3 project is available at: https://www.why3.org/

Author

Akira Tanaka and Yusuke Kawamoto at National Institute of Advanced Industrial Science and Technology (AIST)

Structure of the repository

Why3-py/
- README.md                        this file
- statwhy-install.sh               Why3-py installation script
- statwhy-py                       Launcher for Why3-py
- env-why3                         Script to define environment variables
- plugins/                         Plugins
  - python/                        Why3-py Python plugin
  - ...
- examples/                        Examples
  - statwhy-python/                Why3 examples
  - ...
- doc-why3-py/                     user documentation of Why3-py
- ...

Installation

Why3-py installs its dependencies (Python, mypy, etc.) into a dedicated directory. It also creates a dedicated opam switch.

% sudo apt-get install \
  opam \
  wget \
  git \
  rsync \
  ca-certificates \
  build-essential \
  libsqlite3-dev \
  libssl-dev \
  pkgconf \
  autoconf \
  cvc5 \
  libgmp-dev \
  libcairo2-dev \
  libgtk-3-dev \
  libgtksourceview-3.0-dev
% git clone --depth 1 --branch statwhy https://github.com/fm4stats/why3-py.git
% cd why3-py
% ./statwhy-install.sh $HOME/statwhy statwhy
% eval $(opam env)

In the command ./statwhy-install.sh $HOME/statwhy statwhy, the path $HOME/statwhy specifies the installation directory and statwhy specifies the name of the opam switch.

This software has been tested with Debian GNU/Linux 13 (trixie).

Example

After installation, we can execute the first Python example code to compute the combined $p$-value as follows: (env-why3 and statwhy-py must be executed from the Why3-py source directory.)

% cd why3-py/
% ./env-why3 python3 examples/statwhy-python/example0_meta_pv.py
eg_meta_pvs_fisher p-value : 0.115216

We remark that env-why3 must be executed at the Why3-py source directory. The first execution of the tool takes longer time, but subsequent runs can be faster as they reuse cached information.

Next, we can formally verify Python code via our StatWhy tool using the ./statwhy-py command.

% ./statwhy-py examples/statwhy-python/example0_meta_pv.py

where the statwhy-py command must also be executed at the Why3-py source directory.

Then this launches the IDE of Why3 as follows:

In the left pane, there is a single verification condition (VC) to be discharged: main'vc (the VC for Example0_meta_pv), which is equipped with a question mark. Right-click on this goal and select 'StatWhy' (Not 'CVC5' or the other items) from the context menu, or press '4'. Then StatWhy 1.4 performs the formal verification of the goal. If the prover successfully verifies the goal, all descendants of the goal are folded and a green check mark will appear as follows:

More examples can be found in the examples/statwhy-python/ directory and are explained in the user documentation for Why3-py.

Remark on the StatWhy tool

StatWhy is a software tool for automatically verifying the correctness of statistical hypothesis testing programs. StatWhy 1.2 (an old version without dealing with meta-analyses) was presented in our following paper:

StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs.
Yusuke Kawamoto, Kentaro Kobayashi, and Kohei Suenaga. [alphabetical authorship]
Proc. of 37th International Conference on Computer Aided Verification (CAV 2025),
Part II, Lecture Notes in Computer Science, Vol.15932, pp.216-230, July 2025.

Copyright

The modifications and additions specific to Why3-py are licensed under the GNU LGPL 2.1, which is the same license used for Why3. The Python code for statistical analyses and meta-analyses in the examples directory is licensed under the MIT License, which is the same license used for StatWhy.

See the accompanying LICENSE files for details.

The original README.md of Why3 is follows:

WHY3

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

PROJECT HOME

https://www.why3.org/

https://gitlab.inria.fr/why3/why3

DOCUMENTATION

The documentation (a tutorial and a reference manual) is available online.

Various examples can be found in the subdirectories stdlib/ and examples/.

COPYRIGHT

This program is distributed under the GNU LGPL 2.1. See the enclosed file LICENSE.

The files src/util/extmap.ml{i} are derived from the sources of OCaml 3.12 standard library, and are distributed under the GNU LGPL version 2 (see file OCAML-LICENSE).

Icon sets for the graphical interface of Why3 are subject to specific licenses, some of them may forbid commercial usage. These specific licenses are detailed in files share/images/*/*.txt.

INSTALLATION

See the file INSTALL.md.