Case Studies
From IEEE standards to neural networks, from financial exchanges to classical mathematics — these case studies showcase the breadth of ImandraX as a verification platform.
Industry & Financial Systems
Production Deployments
ImandraX is deployed at leading financial institutions, verifying trading systems, exchange infrastructure, and arithmetic standards with mathematical certainty.
UBS Dark Pool Verification
Financial Services Production DeploymentFormal verification of the UBS ATS dark pool matching engine, discovering a subtle transitivity violation in order ranking. Winner of the 2015 UBS Future of Finance Challenge.
SIX Swiss Exchange Pricing
Financial Services Exchange InfrastructureRegion decomposition analysis of SIX Swiss Exchange auction pricing logic, automatically enumerating all 44 distinct behavioral regions from seemingly simple conditional code.
IEEE P3109 Posit Arithmetic
IEEE Standard Hardware VerificationFormal verification of posit number arithmetic for the IEEE P3109 standard — next-generation floating point. Collaboration with the IEEE standards body.
AI Safety & Neural Networks
Verified AI
ImandraX provides formal guarantees for neural network safety, from certificate checking to controller verification.
DNN Verification with Farkas Certificates
AI Safety Peer-Reviewed (ITP 2025)A verified proof checker for neural network safety properties, using Farkas certificates to prove unsatisfiability of linear arithmetic systems. Presented at ITP 2025.
Vehicle: Neural Network Controller Safety
AI Safety Autonomous SystemsIntegration with the Vehicle DSL for specifying and verifying neural network properties, enabling formal safety guarantees for autonomous systems.
Hardware & Systems Verification
From Bits to Compilers
ImandraX verifies systems at every level of abstraction — from individual logic gates to complete compilers.
Ripple-Carry Adder Verification
Hardware Verification Bit-Level ProofsCorrectness proof of a ripple-carry adder circuit, verifying that the hardware correctly computes binary addition for arbitrary-width inputs. Proved fully automatically.
Stack Machine & Compiler Correctness
Compiler Verification SystemsEnd-to-end verification of a compiler from arithmetic expressions to stack machine instructions, proving that compiled programs always produce correct results.
Autonomous Vehicle Controller
Autonomous Systems Safety-CriticalVerification of the Boyer-Green-Moore car controller — proving that a vehicle under arbitrary wind conditions always remains in a safe state.
Algorithms & Classical Proofs
Deep Reasoning
ImandraX tackles classic problems in combinatorics, logic, and computer science with its powerful inductive waterfall and custom induction schemes.
Mutilated Chessboard
Combinatorics Classic ProblemThe classic proof that a chessboard with two opposite corners removed cannot be tiled by dominoes — formalized as a coloring argument in IML.
Gilbreath's Card Trick
Combinatorics HistoricalA correctness proof of the famous Gilbreath card trick, with a lineage from de Bruijn → Huet → Moore → Boyer → Passmore. Uses custom induction schemes.
Verified SAT Solver
Logic Verified SoftwareA verified tautology checker in the style of Boyer-Moore '79 — both soundness and completeness proved, with ordinal-based termination for the if-normalization algorithm.
Mathematics
Top 100 Theorems
An ongoing project formalizes results from Freek Wiedijk's "100 Theorems" list in ImandraX, positioning it alongside Lean, Coq, and Isabelle as a platform for mathematical reasoning.
Top 100 Mathematical Theorems
Pure Mathematics Theorem ProvingA showcase of formalized mathematical results — from the irrationality of √2 to the infinitude of primes, the Pythagorean theorem, the binomial theorem, and more.
Overview
12 Case Studies
Spanning financial systems, AI safety, hardware verification, classical algorithms, and pure mathematics.
Production Deployed
Verified at UBS, SIX Swiss Exchange, and in IEEE standards development.
Peer-Reviewed Research
Results published at ITP 2025, ARITH 2025, and in Lecture Notes in AI.
Full Spectrum
From bit-level hardware to neural networks, from card tricks to number theory.