  Formal methods have provided approaches for investigating software
engineering fundamentals and also have high potential to improve current
practices in dependability assurance. In this article, we summarise known
strengths and weaknesses of formal methods. From the perspective of the
assurance of robots and autonomous systems (RAS), we highlight new
opportunities for integrated formal methods and identify threats to the
adoption of such methods. Based on these opportunities and threats, we develop
an agenda for fundamental and empirical research on integrated formal methods
and for successful transfer of validated research to RAS assurance.
Furthermore, we outline our expectations on useful outcomes of such an agenda.
