Traditionally, the application of formal verification has been reserved to highly specialised teams (often with PhDs in the subject) in academia, institutions such as NASA, and safety-critical industries such as avionics and microprocessor design.
At AI, our mission is to democratize formal verification, bringing its power to new industries in a user-friendly and scalable way. These applications to new industries are powered by recent advances, including CDCL-based Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solving, nonlinear decision procedures and scalable techniques for symbolic execution.
For more on our vision for formal verification for finance, see our short explainer video.
AI has published several technical white papers about current application of FV to financial markets:
- Case Study: 2015 SEC Fine Against UBS ATS
- Transparent Order Priority and Pricing
- Creating Safe and Fair Markets
AI has also written several public comments to regulatory proposals by the SEC and CFTC:
- Response to Proposed Rule, Regulation Automated Trading (“Regulation AT”) RIN 3038-AD52
- Response to Release No. 34-76474
If you’re interested in further background on techniques underlying Imandra, see the following academic papers:
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
- A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
- The Strategy Challenge in SMT Solving
- Collaborative Verification-Driven Engineering of Hybrid Systems
For a great non-technical introduction to the discipline of formal verification and some of its history, we recommend “Mechanizing Proof” by Donald Mackenzie.
Some great interactive and automated theorem provers
Here are links to some great interactive and automated theorem provers:
Further academic references
For learning the mathematics behind the techniques, we suggest:
- Handbook of Practical Logic and Automated Reasoning by John Harrison, Intel
- Coq’Art by Yves Bertot and Pierre Castéran, INRIA
- A Computational Logic and subsequent books by Robert S. Boyer and J Strother Moore, UT Austin
- Isabelle/HOL - A Proof Assistant for Higher-Order Logic by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel, Cambridge and T.U. München
- Decision Procedures - An Algorithmic Point of View by Daniel Kroening, Oxford and Ofer Strichman, Technion
- Quantifier Elimination and Cylindrical Algebraic Decomposition by Bob Caviness and Jeremy Johnson (Eds.)
- Symbolic Logic and Mechanical Theorem Proving by Chin-Liang Chang and Richard Char-Tung Lee, NIH
- Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, T.U. Dresden and RWTH Aachen
- Handbook of Automated Reasoning by Alan Robinson and Andrei Voronkov (Eds.)