I think Ada guarantees for embedded in particular with Spark are about ensuring that no inputs or transitions in your state machines will produced undefined or unwanted behavior (no way to switch off autopilot for example, or locked door with no manual override).
This is something I also would like to see and I proposed a path forward using Z3: <https://github.com/nim-lang/RFCs/issues/222>
