Resilient, Provably-Correct, and High-Level Robot Behaviors