Legal Engine is the first legal AI company with machine-checkable compliance guarantees. When we say "compliant", there is a mathematical proof behind it.
The Problem
Every legal AI system gives answers. None of them can show their working in a way that a regulator or auditor can independently verify.
When your compliance system says "this structure is permissible" or "this application qualifies", the decision rests on black-box reasoning. There is no audit trail. There is no proof. There is just an output and a hope.
For enterprise customers operating in regulated environments, that is not good enough. Boards, auditors, and regulators increasingly want evidence, not assertions.
What Changes
LegalLean encodes legal rules directly into Lean 4, a programming language designed for mathematical proof. Every step of every compliance decision is checked by a machine before it reaches you.
The result is not just a recommendation. It is a proof object: a machine-readable certificate that anyone can verify independently, in seconds, using free open-source tooling.
This transforms "we believe this is compliant" into "this is provably compliant, and here is the certificate".
Not a chatbot. Not a search engine. A formal verification system built for regulated compliance.
Machine-verified theorems
80 legal rules and properties formally encoded and verified across three jurisdictions, including solver soundness proofs and normalisation idempotence. Each theorem is a machine-checked proof, not a human-written summary.
Generic defeasibility engine
An applicability-aware defeat resolution solver that evaluates legal rules against facts, resolves conflicts by priority, and produces verified compliance determinations. Six property theorems prove correctness.
Independent AI reviews
The framework has been adversarially reviewed by three frontier AI models (Gemini, GPT, Claude) with a cross-model synthesis identifying consensus findings. All reviews are published.
MIT-licensed research
The Lean 4 framework is open source under the MIT licence. Anyone can reproduce the full verification from scratch using Docker. The academic paper, all 80 theorems, and the adversarial reviews are published.
From statutory text to machine-checked proof, in four steps.
Legal rules become formal theorems
Our legal engineers translate statutory rules and regulatory requirements into typed logical statements in Lean 4. Each rule becomes a theorem with a precise, unambiguous definition.
The Lean 4 kernel checks every proof
Lean 4's kernel is a small, trusted piece of code that independently verifies every logical step. It cannot be fooled. If a proof is accepted, it is correct by construction.
Your case is evaluated against proven rules
When a compliance question is submitted, the system evaluates the case facts against the verified ruleset. The output is not a probability score. It is a logical derivation from first principles.
You receive a verifiable compliance certificate
The decision comes with a machine-readable proof certificate. Your legal team, auditors, and regulators can verify the reasoning independently, using open-source tools, at any time.
Three domains where the cost of an unverifiable answer is too high.
Tax Compliance
Corporate tax structures, transfer pricing, and cross-border arrangements generate significant regulatory exposure. LegalLean encodes tax rules formally, so a compliance determination comes with a proof that survives HMRC scrutiny, not just an opinion.
Visa Eligibility
Immigration rules are complex, layered, and frequently updated. LegalLean's verified rule encoding means eligibility decisions are derived from a single, auditable source of truth, with every inference step machine-checked.
Telecommunications Regulation
Regulatory obligations in telecoms span spectrum licensing, consumer protection, and data retention. When Ofcom or the CMA ask for justification, a formal proof is a stronger position than a consultant's memo.
Legal rules can be phrased in many ways. We test that the reasoning stays the same.
Consistency across drafting styles
The same legal rule produces the same verified result regardless of how it is drafted or phrased. We test for this across hundreds of controlled variations using factorial experimental design.
Auditable divergence
When two phrasings produce different results, we can pinpoint exactly why and whether the difference is legally meaningful. Every step from source text through formal encoding to verified proof is inspectable.
Explicit uncertainty
When a legal concept is genuinely ambiguous or discretionary, Legal Lean says so, with a typed marker that distinguishes "this requires human judgment" from "the system is unsure". We measure and report the rate at which the system correctly identifies these cases.
Quantified robustness
Our test coverage is quantified and measurable, not a collection of cherry-picked examples. A structured test suite designed to exercise the interaction effects that cause real failures in legal language processing.
Research foundation
Built at Imperial College London (Department of Surgery & Cancer). Academic paper targeting RuleML+RR and JURIX conferences.
Verification technology
Lean 4, the same formal verification language used in cutting-edge mathematics and systems research
Open standard
Fully reproducible via public Docker image. No lock-in. Your auditors can verify the proofs themselves.
Talk to us about how verified compliance reasoning can strengthen your regulatory position and satisfy the auditors who need more than an AI's say-so.
LegalLean is built on open research. The academic framework is published at legal-lean.aguilar-pelaez.co.uk and the open-source Lean 4 library is available for inspection and reproduction. · Back to Legal Engine