Pramaana Labs raised $27M to wrap AI in mathematical proof for law, tax, and drug discovery

As companies struggle to turn AI pilots into things they can actually rely on, a new startup is betting the fix looks less like a better chatbot and more like a mathematical proof.

Pramaana Labs announced $27mn in seed funding on Wednesday, led by Khosla Ventures, with Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound also taking part.

The company is going after high-stakes fields where a wrong answer carries real cost: law, drug discovery, and tax preparation.

Its pitch is that those fields are not as messy as they look. “The world’s hardest problems are not unsolvable. They are unformalised,” said co-founder and chief executive Ranjan Rajagopalan. “Every domain where being wrong can cost someone their health, money, or freedom has rules.”

An LLM with a proof-checker bolted on

Pramaana still runs on a conventional large language model, which gives it the flexibility to handle natural-language questions. The difference sits on top.

That layer draws on formal verification, the practice of proving a system behaves exactly as specified. Specifically, Pramaana uses LEAN, the open-source language mathematicians use to verify proofs, to check the model’s work and make the reasoning deterministic rather than probabilistic.

“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 tax code. “Once you have a codified version of it, the reasoning on top of it starts becoming deterministic.”

Pairing an LLM with a verification layer is becoming a common way to attack AI’s reliability problem. What Pramaana claims as its own is the use of formal-proof tooling to do it, an approach that sits closer to provable-guarantee research than to the usual guardrails.

Building the rulebook, domain by domain

The catch is that someone has to codify the rules first, and Pramaana is doing it one vertical at a time, each overseen by domain experts.

For tax, the company is working with former IRS commissioner Danny Werfel. Professors from IIT Delhi, IIT Madras, and UC Berkeley are overseeing the cybersecurity and drug-discovery systems.

There is precedent for the idea. Rajagopalan points to France’s CATALA project, which has turned much of the country’s tax and benefit law into executable code.

For now the work is still ahead of the product. Pramaana has the money, the backers, and a thesis that AI’s accuracy ceiling is really a question of how much of the world we have bothered to write down. The rules just need codifying, and that is the hard part.