Formal Verification × Sovereign AI
σ = 10.000
ρ = 28.000
β = 2.667
Mathematical proof for AI systems
that cannot afford to be wrong.
§01 · Capabilities
We do not test. We do not audit. We provide mathematical evidence — the kind that withstands regulatory scrutiny across jurisdictions.
We translate AI system behaviors into mathematical propositions and prove them in Lean 4 — the same proof assistant used in algebraic topology and homotopy theory. Every claim is machine-checked.
For high-stakes deployments — autonomous transport, healthcare, energy, defense — we produce certificates suitable for the EU AI Act, the UAE AI Charter, and equivalent sovereign frameworks.
SDK and tooling that embed verification directly into the AI deployment pipeline. Continuous proof for systems that continue to learn. Built for sovereign operators.
§02 · Thesis
A passing test is evidence of what a system did. A proof is a guarantee of what a system cannot do.
For ordinary software, the distinction is a craft preference. For an AI system deployed at scale — in clinical care, autonomous transport, or sovereign infrastructure — it is the difference between an approved deployment and an avoidable death. Statistical confidence, however large the dataset behind it, is not a mathematical guarantee.
We close the gap. For a system S and a safety property P, we prove in Lean 4 that S satisfies P for every reachable state — or we prove the precise boundary at which it does not.
theorem safety_invariant (sys : AISystem) : ∀ s ∈ sys.reachable, sys.safe s := by apply Lyapunov.stable_attractor exact sys.verified_proof -- furnished at construction
§03 · Foundation
We use the same proof assistant that mathematicians use to verify theorems in algebraic topology. Every claim we make is checked by a kernel — not by human review.
§04 · Who we serve
We work with the institutions building, deploying, and regulating sovereign AI — particularly across the Gulf region and the European regulatory perimeter.
Government agencies & ministries
Operators of AI in national defense, public health, transport, and energy — where deployment authorization demands more than statistical confidence.
Sovereign AI programs
National-scale AI initiatives requiring verifiable safety guarantees in line with the country's own regulatory and strategic frameworks.
Regulators & certifying authorities
Bodies tasked with assessing high-risk AI under the EU AI Act, UAE AI Charter, and equivalent frameworks — when "passed our tests" is insufficient.
Operators of critical infrastructure
Smart-city, healthcare, energy, and autonomous-transport operators integrating AI into systems where the cost of failure is measured in lives.
Research institutions
Academic and corporate AI labs developing safety-critical models who require formal-verification capability beyond the available open-source tooling.
§05 · Work Featured
Engagements with partners are confidential. The work below is open, public, and demonstrates the engine behind the engagements.
Formal verification for neural networks
Formal verification of ReLU neural network decision regions in Lean 4. Proving that a classifier's decision boundary is mathematically stable under specified perturbations. The foundation of our certification engine.
View on GitHub ↗Natural language → verified Lean 4
An end-to-end pipeline from natural-language mathematical statements to verified Lean 4 proofs, with a self-iterating error-correction loop. The translation layer between the human specification and the machine-checked theorem.
Try FORMA ↗§06 · Founder
Hongwei Wang (王鸿玮)
Incoming MSc · NYU Abu Dhabi · MIDSAI '28
Mathematician and engineer with a focus on formal methods, Lean 4 proof engineering, and AI safety. Undergraduate at XJTLU; incoming MIDSAI researcher at NYU Abu Dhabi. Author of CB-Attractor and FORMA.
Academic homepage ↗§07 · Begin a conversation
We are in early conversations with government partners, sovereign AI programs, and operators of critical infrastructure across the UAE, the Gulf, and Europe. If you are building systems where failure is not an option, write to us.
hello@chaosbutterfly.ai →