Pramaana Labs founder Ranjan Rajagopalan on using formal verification to make AI provably accurate in tax and legal domains

Pramaana Labs

Ranjan Rajagopalan's pitch starts with a problem that the legal industry has already experienced in court. An Australian government lawsuit against one of the Big Four accounting firms centred on AI-generated hallucinations, where a model fabricated legal precedent to fit a specific situation. Meanwhile, major U.S. insurance providers have introduced explicit exclusions, refusing to cover outputs where AI is in the chain. Rajagopalan is building Pramaana Labs to close that gap.

The company focuses on tax, legal, healthcare, and governance — domains where a wrong answer carries legal or medical consequence. The underlying technology is formal verification using Lean, a proof language that has been in use for roughly twelve years. It took the mathematical community about nine years to formalize a significant portion of mathematics in Lean. Pramaana is applying the same approach to the U.S. tax code, converting English-language statutes into Lean constructs, then getting that formalization ratified by practicing CPAs, lawyers, and doctors.

“At Pramana, we try to make AI more provably accurate... We are taking a very formal domain, expressed in English today, we are converting that into Lean, which is a proving language. When we do that, we get it ratified by experts... The key difference between an ontology based approach and a lean based approach is that a lean based approach is intrinsically verifiable. Your answer comes with a proof of correctness.”

How the stack works

The architecture runs four layers. When a question arrives — say, whether a specific transaction is taxable in Illinois — Pramaana converts it into a series of constraints, using LLMs to bridge the gap between natural-language input and formal representation. A solver and prover then work in tandem to produce an answer alongside a machine-checkable proof of correctness. That proof, not just the answer, is the product. The distinction from an ontology-based approach like Palantir's is that the output is intrinsically verifiable rather than checked against a reference dataset.

Rajagopalan is also building foundation models focused specifically on formalization — converting English into valid Lean constructs — separate from the better-known capability of using Lean to verify proofs that already exist. Frontier models are improving at Lean-based reasoning, but the formalization step, turning messy real-world language into formal specifications in the first place, is where Pramaana's research is concentrated.

Background

Rajagopalan was previously a machine learning engineer at Google Maps, where he worked on accurately resolving addresses and phone numbers across a messy, unstructured real-world domain. Khosla Ventures is an investor, with Vinod Khosla having publicly introduced the company ahead of this conversation.

The core bet is that "provably accurate" becomes a commercial requirement in high-stakes professional services before it becomes a technical inevitability. If the insurance exclusions and government litigation continue to accumulate, the firms still relying on probabilistic outputs face a liability problem that a mathematical proof is designed to eliminate.