In this article, we delve more deeply into incorporating safety into the formal definition of the program. It takes a closer look at the initial implementation.

Back to “Run”

Now the contract for “Go_Forward” has been changed, the loop in “Run” must be revisited as it’s quite clear that it won’t prove in its current state:

This loop doesn’t meet the precondition on “Go_Forward”. In the first iteration, it’s known only “Rover.Cannot_Crash” from the precondition on “Run”, which is weaker than “Rover_HAL.Get_Sonar_Distance >= Distance_Threshold”. And in subsequent iterations, it’s still known only “Rover.Cannot_Crash” because that’s all the loop invariant establishes.

Regardless of any other changes, the postcondition on “Find_New_Direction” must be strengthened to “Rover_HAL.Get_Sonar_Distance >= Distance_Threshold”. And since “Find_New_Direction” currently has no precondition (other than “Initialized”), it’s sensible to put it first in the loop:

This way, the precondition on `Run` could be dropped altogether, allowing the Rover to start arbitrarily close to an obstacle and still avoid crashing.

Let’s see what it will take to get “Find_New_Direction” to promise “Rover_HAL.Get_Sonar_Distance >= Distance_Threshold”.

Improving “Find_New_Direction”

Here’s the current implementation of “Find_New_Direction”:

The logic here is to look to the left and the right and measure the distance to obstacles in both directions; then reorient the vehicle based on those measurements. If both left and right are too close (closer than 50 units), turn around. Otherwise, turn toward whichever direction has an obstacle further away.

This is intuitive, but it doesn’t guarantee that it will end up pointed in a direction with an obstacle more than 40 units — our distance threshold and the precondition for “Go_Forward” — away. For example, what if it doesn't turn far enough to the left or the right? The delay was chosen based on Rover dynamics. However, there’s no guarantee (in software!) that it will end up pointed in a direction with an obstacle more than 40 units away.

What if motor power drops during the turn and it doesn't turn as far as expected? Worse, what if the Rover finds itself inside of a (small) box with no exits? The current code would turn around and start moving forward without confirming that the way out is clear!

Now, it could be argued that these corner cases are impossible. But safety is about identifying corner cases and either removing them or arguing through risk assessment that the consequences are accepted if the corner case occurs (e.g., the Rover drives into a canyon on Mars and is blocked in by a rockfall).

Before the postcondition is strengthened to “Rover_HAL.Get_Sonar_Distance >= Distance_Threshold” and this subprogram updated to meet it, pause, and ask: “How is the current postcondition proved?” given the problems noted above.

The answer is, again, the safety property is (much) weaker than the new postcondition. Here, it’s met entirely because “Find_New_Direction” always leaves the Rover in a state in which it’s not moving straight forward. And that’s enough to satisfy the safety property, so the current postcondition proves. But it’s not enough to satisfy the precondition of our now-proved-safe “Go_Forward”.

Fortunately, fixing “Find_New_Direction” isn’t difficult. Here’s the updated, fully proved implementation:

The current functionality has been wrapped in a while loop that continues searching for a new direction until the distance is greater than or equal to the threshold of 40 units. A new local function was introduced to measure the distance straight ahead, as this behavior is required twice; encapsulation therefore keeps the implementation DRY (Don’t Repeat Yourself).

Notably, no loop invariants or assertions were required. SPARK proves that the revised postcondition holds based solely on the updated implementation.

Finalizing “Run”

There’s one more change needed to make to “Run”. Since “Find_New_Direction” promises “This.User_Exit” or “Rover_HAL.Get_Sonar_Distance >= Distance_Threshold”. It’s necessary to check for user exit before commanding forward motion:

And that’s it. The safety property throughout autonomous mode is fully proven, including while the Rover is driving forward in “Go_Forward”.

Conclusion: The Analysis of Our Demo

The Mars Rover demo shows how cyber-physical systems benefit from rigorous, provable software. Starting from SPARK Silver (absence of run-time errors), the team introduced a meaningful Gold-level safety property — “the rover must not proceed straight when an obstacle is within the safety threshold” — and encoded it through a clean HAL model with Ghost getters, a composable safety monitor, and targeted contracts.

In doing so, the exercise surfaced and removed a latent assumption in remote-control mode and then strengthened autonomous mode with a simple dynamics model and modularized assumptions. This enabled full proofs of Go_Forward and Find_New_Direction with minimal auxiliary annotations.

Beyond the specific rover, this work illustrates a repeatable pattern for CPS: isolate hardware effects, express intent as contracts, attach proofs where they matter, and let the analysis expose unsafe edge cases before they reach hardware. The result is not only higher assurance, but clearer software architecture and more maintainable code.