Have you explored using a formal verification tool to prove out the safety/liveness properties of your (or the end user's) autonomy specifications? Could you model the system in something like Spin/NuSMV/PRISM and then ensure that certain properties hold (useful states are reachable and dangerous ones are not)?
No, we haven't looked into formal tools like that, good suggestion!
TBD on if these approaches bode well for real world robotics, (due to model complexity and model/real world fit problems) but at least there seems to be some applications to path planning and controls:
https://ieeexplore.ieee.org/document/5509686
