The use of autonomous systems equipped with the latest technological advances greatly facilitates response operations after a disaster. They can intervene, for example, in places that are inaccessible or dangerous for human rescuers. To be effective, these systems integrate increasingly advanced sensors and therefore become more and more linear. This considerably increases their capabilities but also the cost. It is therefore necessary to ensure the reliability of the system. The objective of this evaluation is to verify that the system survives and completes the mission or aborts it in time to return to its base. For this we propose the use of formal methods. The Event-B method allows us to prove properties on a very abstract model of the system, which is then incrementally refined to a detailed specification of a correct implementation by construction. We also illustrate an approach using graphics specifications using Avatar. These two approaches are illustrated in a very simplified description of our Rover.