Leibniz AI
Leibniz AI correctly applies complex rules consistently, so every team, workflow, and agent makes decisions that are traceable to the source.
“Should a dispute arise, two philosophers would need no more argument than two mathematicians.
They would simply take up their pens, sit down, and say to one another: Let us calculate.” Gottfried Wilhelm Leibniz · The Art of Discovery, 1684
What we build
The Leibniz Engine works like a legal compiler for statutes, regulations, contracts, and policies: it classifies what each sentence is doing, translates it into a controlled rule format, checks the rule against its source text, then compiles it to formal logic a solver can run. If the rules change, Leibniz flags which standards moved.
The Leibniz Engine works like a legal compiler for statutes, regulations, contracts, and policies: it classifies each sentence, translates into a controlled rule format, checks the rule against its source text, then compiles to formal logic a solver can run. If the rules evolve, Leibniz flags which standards moved and what workflows change.
Leibniz guardrails agents against your governing texts, eliminating reasoning hallucinations while reducing token usage.
Leibniz EngineSMT proof engine · deterministic
SMT · proof
; obligations surviving termination survivors := { §9 } conf ∈ §12 ; §12 ∉ survivors terminate ⇒ ¬ in_force(conf) §12.4: in_force(conf) (check-sat) → unsat
Leibniz reads an incoming agreement clause by clause and formally checks each one against your governing terms and conditions, with a live audit trail that never hallucinates.
Your Policies, Enforced by the Leibniz Engine
; §9 · choice of law (assert (= governingLaw CT)) ; §20 · payment terms (assert (= paymentNetDays 30)) ; … remaining sections
compiled to machine-checkable rulesLeibniz compiles your regulatory policies to machine-checkable rules. The outcome paths can be visualized as branching trees. Choose a policy and walk through the outcome scenarios.
The problem
Every organization runs on complex, evolving rules: policies, regulations, contracts, and plan documents. Applying them correctly is resource-intensive and brittle to change, especially in highly regulated industries where decisions have to be auditable. As regulators keep moving in, enterprises need to act now to keep their AI systems correct, consistent, and traceable.
The Leibniz Approach
Partners
Leibniz works with organizations putting verifiable reasoning into real decisions, from insurance claims and underwriting to access-to-justice legal services.
Team
Leibniz is a Yale spin-out. Its technical core is the product of years of automated-reasoning research, a collaboration between the Piskac Rigorous Software Engineering (ROSE) group at Yale and the Shapiro Yale Legal AI Lab at Yale Law School.
Chair of the Yale Computer Science Department and a leading scholar of formal methods and automated reasoning, recognized by the National Science Foundation and the ACM, with research awards from AWS, Google, and Microsoft.
Yale
Southmayd Professor of Law and Philosophy at Yale Law School, where he leads the Yale Legal AI Lab. Formerly the Special Assistant for AI Ethics to the Chief AI Officer of CISA/DHS. Co-editor of the Stanford Encyclopedia of Philosophy and The Oxford Handbook of Jurisprudence.
Yale Law School
Computer Science PhD candidate at Yale (on leave), advised by Ruzica Piskac, specializing in neurosymbolic AI. Previously an engineer on the BandLab Audio Engine and a research resident at Grame CNCM.
Yale
Technology executive with a track record across cloud, software, and telecom, including 13 years at Amazon Web Services leading verification and policy product development.
Amazon · AWSPilot
We're working with teams putting AI into regulated decisions. Bring a policy or contract you already work from, and we'll formalize it with you and run it against cases you already know the answer to.