As businesses struggle to turn experimental AI projects into reliable, real-world tools, the need for dependable systems has become a top priority. A new company aims to tackle this challenge by applying the principles of mathematical formalization, merging one of computer science’s most rigorous frameworks with AI’s inherent unpredictability. On Wednesday, Pramaana Labs announced it has raised $27 million in seed funding, with Khosla Ventures leading the round. Additional backing came from Accel, Boldcap, Nexus Venture Partners, Premji Invest, and Unbound. The startup plans to focus on high-stakes industries such as law, drug discovery, and tax preparation—fields where mistakes can be extremely costly and reliability is critical. Deploying AI in these areas requires much stronger safeguards against hallucinations and errors than current systems provide. However, according to Pramaana’s co-founder and CEO, Ranjan Rajagopalan, these sectors are also particularly well-suited for formalization. “Once you have a codified version of it, the reasoning on top of it starts becoming deterministic,” he explains.

EMBED_PLACEHOLDER_0

The company’s system still runs on a conventional large language model (LLM), which allows it to respond to natural language questions and handle complex problems that traditional computers cannot manage. But on top of that LLM, there is a deterministic layer that verifies the model’s outputs are correct. This combination of an LLM engine with deterministic verification is a common approach, but Pramaana’s distinctive method lies in using formal verification tools—specifically, the open-source LEAN programming language, which was originally designed to verify mathematical proofs. There is real precedent for this kind of work; Rajagopalan points to France’s CATALA project, which formalizes much of the country’s tax and benefit system into executable code. For each specific use case, Pramaana will create its own LEAN-style formal verification system, overseen by domain experts. In tax law, the company is collaborating with former IRS commissioner Danny Werfel, while professors from IIT Delhi, IIT Madras, and UC Berkeley are supervising the cybersecurity and drug discovery systems. “The world’s hardest problems are not unsolvable. They are unformalized,” Rajagopalan says. “Every domain where being wrong can cost someone their health, money, or freedom has rules.” Now, those rules simply need to be codified.