In this talk I will describe how formal methods such as synthesis – automatically creating a system from a formal specification – can be leveraged to design robots, guarantee their behavior, and provide feedback about things that might go wrong. I will discuss the benefits and challenges of synthesis techniques and will give examples of different robotic systems including modular robots, swarms, and robots interacting with people.