Using formal verification to develop higher assurance, more maintainable financial software
Manfred Kerber, Colin Rowat, Neels Vosloo · Journal of risk management in financial institutions · 2019
Formal verification — a sibling of artificial intelligence — uses computers to prove that a design — whether hardware, software or a mathematical proof — is correct. As such, it offers higher assurances than testing, which cannot provide guarantees beyond the test data. As formal’s cost comes down, it is spreading beyond its roots in computer hardware and aerospace software into consumer technology and finance. This paper surveys successful use cases outside finance, as well as more recent applications to finance, including by industry leaders such as Bridgewater and Goldman Sachs.