Imandra Protocol Language - VS Code Plugin
Imandra Protocol Language (IPL) is the first formal language for expressing system connectivity logic (e.g. FIX specifications) resulting in precise and executable specifications.
A specification expressed in IPL may be used to automatically:
The current implementation supports the FIX protocol (versions 4.2, 4.4 and 5.0), but our roadmap includes other widely used protocols such as SWIFT, FAST and ITCH.
The following blog posts give context to IPL, and the notion of machine reasonable APIs:
For documentation, see https://docs.imandra.ai/ipl. For IPL examples, see https://github.com/AestheticIntegration/ipl-examples
For further information, see our website https://www.imandra.ai
Roadmap and Known Issues
Imandra is a formal verification start up with offices in London, Edinburgh and Austin.
Created by leading innovators in software safety, trading system design and risk management, AI’s patent-pending Imandra formal verification technology is revolutionising the safety, stability and transparency of global financial markets.
For further information, see https://www.imandra.ai.
About formal verification
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 democratise 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:
And here are links to some great interactive and automated theorem provers:
For a great non-technical introduction to the discipline of formal verification and some of its history, we recommend "Mechanizing Proof" by Donald Mackenzie.
For learning the mathematics behind the techniques, we suggest:
If you have other relevant publications or academic papers related to application of formal verification (or formal methods, etc) to financial markets, please create a PR.