Docs
Pages
Documentation Home
Imandra Core
A quick tour
Installation
Installer
Manual (opam)
Docker Image
Jupyter Notebook
VSCode
Server Image
Logic and Program modes
Verification
Commands
Attributes
Unrolling
Simplification
Blast
Induction
Waterfall
Proving program termination
Region Decomposition
Background to decomposition
Imandra tools introduction
Iterative Decomposition Framework
Region Probabilities
Imandra Discover
Multifile development
Extracting OCaml modules
Code generation and plugins
Imandra vs.
Examples
Beginner
Analysing Web-app authentication logic
Simple vehicle controller
Simple car intersection model
Rule Conflict Resolution
Tic Tac Toe with ReasonML
Exploring The Apple FaceTime Bug with ReasonML State Machines
Crossing the river safely
Intermediate
Analysing the UBS ATS Dark Pool
Region Decomposition - Exchange Pricing
Creating and Verifying a ROS Node
Key Pair Security in Imandra
Solving Sudoku with Imandra
Synthesising a game solver in Imandra
Exchange Implied Trading
Solving school scheduling during COVID
Advanced
Recursion, Induction and Rewriting
Verifying merge sort in Imandra
Verifying a Ripple Carry Adder
Calculating Region Probabilities
Analysing Machine Learning Models
Probabilistic Reasoning in ReasonML
A comparison with TLA+
Reference
Standard Library
OCaml API Docs
Python API Docs
ImandraX
Imandra Universe
Imandra Protocol Language
Imandra Rule Synth
Products
Use cases
Docs
Company
Financial Services
Overview
Markets
Connectivity
Key Technology
Imandra Core
MBSD
IPL
Explore
Try Imandra Online
Imandra Core in your browser via Jupyter
Core Gallery
Select categorized Imandra Core examples
IPL Gallery
IPL state exploration demos
Industries
Financial Services
Autonomous Systems
Government & Defense
Applications
MBSD
Formal Methods
Trustworthy AI
System Integration
Documentation
Imandra Core
Python API
Languages & Interfaces
IPL
Rule Synthesis
Company
About
Careers
Media
Blog
News
Financial Services
Overview
Markets
Connectivity
Key Technology
Imandra Core
MBSD
IPL
Explore
Try Imandra Online
Core Gallery
IPL Gallery
Applications
MBSD
Formal Methods
Trustworthy AI
System Integration
Industries
Financial Services
Autonomous Systems
Government & Defense
Documentation
Imandra Core
Python API
Languages & Interfaces
IPL
Rule Synthesis
Company
About
Careers
Media
Blog
News
User Area
Login
Verification
¶
Commands
Attributes
Unrolling
Simplification
Blast
Induction
Waterfall
