I&#x27;ve got no idea what they do now but Altran UK nee Praxis was mildly (in)famous for using formal methods and verifiable code. The Paris Metro I think is the notable one they did, something with French trains at the least.<p><a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Altran_Praxis" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Altran_Praxis</a>