Pramaana Labs Raises $27M to Bring Formal Verification to AI in Drug Discovery and Medical Diagnosis
核心洞察
Pramaana Labs (搜索) has raised $27 million in seed funding led by Khosla Ventures (搜索) to develop a formal verification system that ensures AI outputs are provably correct before being returned to users.
The startup targets high-stakes regulated verticals including drug discovery, medical diagnosis, tax preparation, and cybersecurity, where errors can be costly or life-threatening.
The system combines a conventional large language model with a deterministic proof engine built on the Lean formal verification language, which audits outputs against codified domain rules.
Pramaana Labs (搜索) Inc., a startup founded by three Indian Institute of Technology Madras alumni, announced Wednesday that it has raised $27 million in seed funding to build a formal verification layer that makes artificial intelligence prove its answers before delivering them. The round was led by Khosla Ventures (搜索), with participation from Accel (搜索), BoldCap, Nexus Venture Partners, Premji Invest, and Unbound Capital Ltd.
The company is targeting high-stakes regulated fields where errors carry severe consequences, including drug discovery, medical diagnosis, tax preparation, cybersecurity, and financial compliance. Its system pairs a conventional large language model (LLM) with a deterministic proof engine that audits every output against codified domain rules, refusing to return an answer unless it can be proved correct.
A Deterministic Layer on Top of Probabilistic AI
Pramaana's architecture rests on a simple premise: large language models can generate answers that sound right, but they cannot demonstrate that an answer is right. In fields governed by strict rules—clinical protocols, tax codes, financial regulations—that gap is critical.
The company rewrites a domain's rules in a formal language that a machine can reason over. When a user poses a question, the system restates it as a formal claim and hands it to a proof engine. If the answer holds, the engine returns a machine-checkable proof. If it does not, the system points to the specific rule that breaks.
"It's like math in the sense that you have a lot of rules that you need to abide by," CEO Ranjan Rajagopalan told TechCrunch, describing the tax code. "Once you have a codified version of it, the reasoning on top of it starts becoming deterministic."
The technical foundation is Lean, the open-source programming language used to write machine-checked mathematical proofs. Pramaana points to Google DeepMind (搜索)'s AlphaProof, which generated formal Lean proofs for competition mathematics problems, as evidence that the proving step can be automated. The company also cites France's Catala project, which has formalized parts of the country's tax and benefit rules into executable code, as precedent for applying the method to regulation.
Drug Discovery and Medical Applications
Pramaana is building separate verification systems for each use case, each overseen by domain experts. For the drug discovery vertical, professors from IIT Delhi, IIT Madras, and UC Berkeley are supervising the development of the formal verification framework. The medical diagnosis system follows the same model, with clinical protocols serving as the rule base against which AI outputs are checked.
The company states it has yet to produce a confidently wrong verified answer—a claim with significant implications for pharmaceutical research, where computational predictions about drug-target interactions, toxicity, and clinical trial outcomes must be reliable to avoid costly failures.
"The world's hardest problems are not unsolvable. They are unformalized," said Rajagopalan. "Every domain where being wrong can cost someone their health, money, or freedom has rules."
Founding Team and Backers
Pramaana was founded by three IIT Madras alumni. Rajagopalan previously led moderation at Google Maps. Co-founder Krishnan worked on the Glean Assistant at Glean Technologies Inc., and co-founder Sanjay served as a staff research engineer at Google DeepMind (搜索), contributing to the Gemini models. The broader team includes researchers drawn from DeepMind, Meta Platforms Inc., Microsoft Corp., Uber Technologies Inc., and UC Berkeley.
The company's advisor roster includes Pushmeet Kohli, a vice president at Google DeepMind (搜索), and Sriram Rajamani, a corporate vice president at Microsoft Research. Former U.S. Internal Revenue Service Commissioner Danny Werfel is advising the tax effort.
The $27 million in seed funding will be directed toward training the company's formalization and prover models, hiring research engineers, and adding domain experts across its regulated verticals.