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:

AI has also written several public comments to regulatory proposals by the SEC and CFTC:

If you’re interested in further background on techniques underlying Imandra, see the following academic papers:

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: