| Util | Useful functions |
| Opt | Useful option combinators |
| Lists | Useful list combinators |
| Strings | Additional Useful Functions on Character Strings |
| Getopt | Parsing of command-line options. |
| Extmap | Association tables over ordered types |
| Extset | Sets over ordered types |
| Exthtbl | Association tables over hashable types |
| Weakhtbl | Hashtables with weak key used for memoization |
| Wstdlib | Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types |
| Rc | Rc file management |
| Debug | Debug flag handling |
| Loc | Source locations |
| Pp | Helpers for formatted pretty-printing |
| BigInt | Wrapper for big nums, implemented either with OCaml's |
| Number | General functions for representations of numeric values |
| Mlmpfr_wrapper | |
| Ident | Identifiers |
| Ty | Types |
| Term | Terms and Formulas |
| Decl | Logic Declarations |
| Coercion | |
| Theory | Theories and Namespaces |
| Env | Environments |
| Task | Proof Tasks, Cloning and Meta History |
| Trans | Task transformations |
| Pretty | Pretty-printing various objects from Why3's core logic |
| Printer | |
| Model_parser | Counter-example model values |
| Ptree_helpers | |
| Typing | Typing parse trees |
| Mlw_printer | Pretty printing of Why3 parse trees as WhyML source code |
| Whyconf | Managing the configuration of Why3 |
| Call_provers | Call provers and parse their outputs |
| Driver | Managing the drivers for external provers |
| Args_wrapper | Pre-processing of transformations with arguments, including parsing and typing in the context of a task. |
| Ity | |
| Expr | |
| Pdecl | |
| Pmodule | |
| Vc | |
| Pinterp_core | Basic definitions for Pinterp and Rac |
| Rac | RAC implementation(s) |
| Pinterp | Interpretation of Why3 programs |
| Check_ce | Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking |
| Session_itp | Proof sessions |
| Controller_itp | Controller to run provers and transformations asynchronously on goals of a session |
| Itp_communication | |
| Itp_server | Server for a client/server communication with an external graphical interface |
| Ptree | Parse trees |