Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License 
3.4 ProvingIn Section 3.2.7, we learned what proof obligations are generated by Rodin from an EventB model. We validate the model by discharging proof obligations. This is what we call proving.
