| Args_wrapper | Pre-processing of transformations with arguments, including parsing and typing in the context of a task. |
| BigInt | Wrapper for big nums, implemented either with OCaml's |
| Call_provers | Call provers and parse their outputs |
| Check_ce | Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking |
| Coercion | Support for coercions in the logic language |
| Controller_itp | Controller to run provers and transformations asynchronously on goals of a session |
| Debug | Debug flag handling |
| Decl | Logic Declarations |
| Driver | Managing the drivers for external provers |
| Env | Why3 Environments |
| Expr | WhyML program expressions |
| Exthtbl | Association tables over hashable types |
| Extmap | Association tables over ordered types |
| Extset | Sets over ordered types |
| Getopt | Parsing of command-line options |
| Ident | Identifiers |
| Itp_communication | Communication protocol for the ITP server |
| Itp_server | Server for a client/server communication with an external graphical interface |
| Ity | Types in WhyML programs |
| Lists | Combinators on |
| Loc | Source locations |
| Mlmpfr_wrapper | Wrapper module for computation on extended floating-point numbers |
| Mlw_printer | Pretty printing of Why3 parse trees as WhyML source code |
| Model_parser | Model |
| Number | General functions for representations of numeric values |
| Opt | Combinators on |
| Pdecl | WhyML program declarations |
| Pinterp | WhyML Program Interpreter |
| Pinterp_core | WhyML program interpreter: basic definitions |
| Pmodule | WhyML program modules |
| Pp | Helpers for formatted pretty-printing |
| Pretty | Pretty-printing various objects from Why3's core logic |
| Printer | Task printing |
| Ptree | Parse trees |
| Ptree_helpers | Helpers for constructing program with the parse tree API |
| Rac | Runtime Assertion Checkers for WhyML programs |
| Rc | Configuration file management |
| Session_itp | Proof sessions |
| Strategy | Proof strategies |
| Strings | Utility Functions on Character Strings |
| Task | Proof Tasks, Cloning and Meta History |
| Term | Terms and Formulas |
| Theory | Theories and Namespaces |
| Trans | Task transformations |
| Ty | Types |
| Typing | Typing parse trees |
| Util | Various Utility Functions |
| Vc | WhyML VC generators |
| Weakhtbl | Hashtables with weak key used for memoization |
| Whyconf | Managing the configuration of Why3 |
| Wstdlib | Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types |