-
Notifications
You must be signed in to change notification settings - Fork 359
(data) add success story for Imandra #2868
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
+202
−0
Merged
Changes from all commits
Commits
Show all changes
3 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
--- | ||
title: Financial Compliance with Automated Reasoning | ||
logo: success-stories/imandra.svg | ||
card_logo: success-stories/white/imandra.svg | ||
background: /success-stories/imandra-bg.jpg | ||
theme: black | ||
synopsis: "Imandra leverages OCaml to develop automated reasoning tools that enable financial institutions to mathematically verify their trading algorithms meet regulatory requirements." | ||
url: https://www.imandra.ai/ | ||
priority: 7 | ||
why_ocaml_reasons: | ||
- Expressive Type System | ||
- High Performance | ||
- Unified Tech Stack | ||
- Strong Ecosystem | ||
- Interoperability | ||
- Community and Resources | ||
--- | ||
|
||
## Challenge | ||
|
||
The 2008 financial crisis fundamentally altered the regulatory landscape for financial institutions. Banks faced stringent new compliance requirements that demanded mathematical proof of algorithmic correctness—a challenge the industry was ill-equipped to handle. Trading algorithms, characterized by nonlinear mathematical behaviors and complex decision trees, were typically specified through informal PDF documentation prone to ambiguity and human error. | ||
|
||
Grant Passmore, drawing on his doctoral research in decision procedures for nonlinear arithmetic at Edinburgh, identified a critical capability gap. While existing formal verification tools like SAT and SMT solvers could handle bounded problems, they lacked the sophistication to reason about the recursive functions, higher-order logic, and nonlinear arithmetic inherent in modern trading systems. The autonomous systems sector faced similar verification challenges, requiring tools capable of reasoning about nonlinear control flow in applications from drone controllers to analog circuits. | ||
|
||
## Solution | ||
|
||
Imandra developed a comprehensive automated reasoning system built entirely in OCaml. Their Imandra Modeling Language (IML), a carefully designed subset of OCaml, provides the expressiveness needed for complex specifications while maintaining decidability properties essential for automated reasoning. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. essential for industrial automated reasoning |
||
|
||
The company's primary innovation lies in formalizing previously informal specification processes. Financial institutions transitioned from error-prone PDF documentation to formal IML specifications, authored using Imandra's VSCode extension. This formalization enables automated analysis, systematic edge-case discovery, and streamlined regulatory certification. | ||
sabine marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
A pivotal demonstration came through their 2017 partnership with Goldman Sachs. Imandra formally modeled and verified the SIGMA X MTF Auction Book, proving key properties about fairness and correctness. These verified models were deployed to production, where they continue to validate trading operations in real-time. | ||
|
||
Imandra's "digital twin" technology compiles formally verified models into efficient executable code that runs alongside production systems, providing continuous mathematical assurance of correct behavior. | ||
|
||
[Watch Imandra's explainer video](https://vimeo.com/123746101) to understand Imandra's approach to automated reasoning. | ||
|
||
sabine marked this conversation as resolved.
Show resolved
Hide resolved
|
||
## Why OCaml | ||
|
||
While Imandra's initial prototype utilized PolyML, the team strategically migrated to OCaml based on four compelling factors: | ||
|
||
• **Industry Credibility**: OCaml's established presence in financial institutions through Jane Street and LexiFi provided crucial market validation. LexiFi's integration within Bloomberg terminals offered immediate credibility when engaging potential clients unfamiliar with formal verification. | ||
|
||
• **Type System Optimality**: OCaml occupies an optimal position in the type system spectrum for automated reasoning. It provides sufficient type safety for building reliable theorem provers without the implementation complexity imposed by dependently typed languages. | ||
|
||
• **Architectural Consistency**: Unlike competitors employing C++ for reasoning engines and disparate technologies for interfaces, Imandra maintains unity through OCaml. From theorem proving kernel to Eliom-based web frontend, this consistency enables fluid knowledge transfer and reduces architectural impedance. | ||
sabine marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
• **Ecosystem Maturity**: Industrial-strength tooling through opam and Dune, combined with resources like *Real World OCaml*, accelerates engineer onboarding. The robust FFI facilitates integration with existing C or Rust components, which Imandra systematically replaces with pure OCaml implementations. | ||
sabine marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
## Results | ||
|
||
**Used by Key Industry Players**: Goldman Sachs operates Imandra's verified models in production, validating trades in real-time. Citi and other major institutions have followed suit. Beyond finance, DARPA and the US Navy employ Imandra for critical infrastructure verification. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. validating trades and gaining deep insights through Imandra's formally verified digital twins. |
||
|
||
**Industry Transformation**: Financial institutions broadly adopted Imandra's formal specification approach, abandoning error-prone PDF processes for mathematically rigorous alternatives. Imandra compresses FIX protocol certification from days to hours, directly enhancing banks' ability to onboard trading partners. | ||
|
||
**Development Flexibility**: Engineers transition seamlessly between frontend development and theorem prover implementation. The unified architecture eliminates specialization silos and maximizes knowledge utilization. | ||
|
||
## Lessons Learned | ||
|
||
**Architectural Uniformity**: Employing OCaml across all system layers eliminates technology boundaries. Engineers can progress from accessible frontend tasks to sophisticated theorem proving work within a single language ecosystem. | ||
|
||
**Community Scale Matters**: OCaml's larger community relative to alternatives like PolyML provides richer tooling, comprehensive learning resources, and deeper talent pools. | ||
|
||
**Ecosystem Investment Compounds**: Mature tooling and high-quality educational materials significantly reduce time-to-productivity for new team members. | ||
|
||
**Type System Balance**: OCaml's type system provides strong guarantees without excessive ceremony—particularly well-suited for verification systems where both correctness and development efficiency are paramount. |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.