⚡ The B WORKBOOK is now available on CLEARSY’s GitHub: (https://github.com/CLEARSY/BWORKBOOK).
After several months of collaborative 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 from Europe and South America who made this release possible.
✅ The B WORKBOOK currently offers 7 exercises of increasing complexity, providing a step-by-step introduction to Atelier B.
It covers the main phases of development: 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 ProB.
🔎 A next iteration (planned for 2026) will extend the scope with new exercises on:
- Event-B modelling
- graphical animation with VisB
- Rust code generation
- interactive proofs, proof tactics, and rule writing.
🌍 In the meantime, we welcome error reports, suggestions, and new exercise ideas through GitHub.