The user manual for B Method, the B WORKBOOK, is now available on CLEARSY’s GitHub: (https://github.com/CLEARSY/BWORKBOOK).
After several months of effort, this first version (122 pages) can now be used as a resource for training in formal methods and for teaching the B method.
We warmly thank the contributors and reviewers such as the IMD/Universidade Federal do Rio Grande do Norte UFRN (Natal, Brazil), the Universidade Federal de Pernambuco UFPE (Recife, Brazil), the Heinrich-Heine-Universität Düsseldorf (Düsseldorf, Germany) and Télécom Paris (Paris, France) who made this release possible.
The B WORKBOOK currently offers 7 exercises of increasing complexity, providing a step-by-step introduction to the tool Atelier B.
It covers the main phases of development with B Method : formal specification, implementation, proof, code generation, and compilation of the final executable.
Each exercise comes with:
- modelling files
- proof files with automatic demonstrations
- complementary manual source code and Makefile for Unix environments (Windows WSL, Linux, MacOS)
- instructions for animating models with the dedicated tool ProB
A next iteration (planned for 2026) will extend the scope with new exercises on:
- Event-B formal system modelling langage
- graphical animation with the tool VisB
- Rust code generation
- interactive proofs, proof tactics, and rule writing
We welcome error reports, suggestions, and new exercise ideas through GitHub collaborative network.