Autonomous Robots are taking a more important place in our lives every day; the recent situation has even accelerated their use in health-care applications: for (medical or family) telepresence, people assistance, or place disinfecting. Using an autonomous robot in contact with humans requires some guarantees on the robot behavior. These guarantees go from high-level behaviors (capability to assist the person, respond to a situation) to low-level behaviors (avoiding collisions, stopping on time). In that context, I will present some works related to the use of formal models and associated verification techniques at several layers of robot software architectures: (1) component-based models for developing the functional architecture, with guarantees on the real-time constraints, (2) formal models of robot skills based on a domain specific language, and (3) the use of Petri net models to program and verify robot missions.