{random.ramblings} model checking

The funny thing is, I don't know what system I am trying to verify. Is it the software of the robot controller, or the robotic manipulation tasks? How is this going to affect the mechanical design of robots? Higher levels of abstraction might be easier to verify, but would they be sufficient to implement a reliable system?