Pramaana will focus on highly sensitive verticals like law, drug discovery, and tax preparation — where errors can be costly and reliability is at a premium. Deploying AI in those systems will require stronger protections against hallucinations and errors than we currently have. But as Pramaana co-founder and CEO Ranjan Rajagopalan sees it, they’re also uniquely suited to formalization.

“It’s like math in the sense that you have a lot of rules that you need to abide by,” Rajagopalan told TechCrunch, describing the rules of the tax code. “Once you have a codified version of it, the reasoning on top of it starts becoming deterministic.”

Pramaana’s system still runs on a conventional LLM, giving it the flexibility to answer natural language questions and tackle complex problems that conventional computers can’t handle. But there’s a deterministic layer on top of that LLM ensuring the LLM’s work checks out.

This combination of an LLM engine with deterministic verification is a popular setup; Pramaana’s unique approach is to use the tools of formal verification — drawing on the open source LEAN programming language used to verify mathematical proofs. There’s real precedent for much of this work; Rajagopalan points to France’s CATALA project, which formalizes much of the country’s tax and benefit system into executable code.