Formal verification startup Pramaana Labs Inc. today said it has raised $27 million in seed funding for a system it describes as a compiler for high-stakes artificial intelligence.

The product checks an AI model’s answer against the rules of a domain and will not return it unless it can be proved correct. Pramaana is going after regulated work where mistakes are expensive, starting with tax, medical diagnosis, cybersecurity and financial compliance.

Its founders argue today’s models have a gap they cannot close alone. A large language model can write an answer that sounds right. It cannot show the answer is right, and in fields run by strict rules, that is the part that matters.

A conventional large language model still does the heavy lifting, fielding questions in plain language. On top of it sits a deterministic layer that audits the output. Pramaana rewrites a field’s rules in a formal language a machine can reason over. The U.S. tax code is one target. Clinical protocols are another.

When a user asks a question, the system restates it as a formal claim and hands it to a proof engine. The engine returns a machine-checkable proof when the answer holds. When it does not, it points to the rule that breaks. The company says it has yet to produce a confidently wrong verified answer.

The technical foundation is Lean, the open-source 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 the proving step can be automated. It 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.

“It’s like math in the sense that you have a lot of rules that you need to abide by,” Chief Executive 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.”

Pramaana was founded by three Indian Institute of Technology 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 was a staff research engineer at Google DeepMind and a contributor to the Gemini models. The team includes researchers drawn from DeepMind, Meta Platforms Inc., Microsoft Corp., Uber Technologies Inc. and the University of California at Berkeley.

The company is building a separate verification system for each use case, overseen by domain experts. Former U.S. Internal Revenue Service Commissioner Danny Werfel is advising the tax effort, while professors from IIT Delhi, IIT Madras and UC Berkeley oversee the cybersecurity and drug discovery work. Pramaana also lists Pushmeet Kohli, a vice president at Google DeepMind and Sriram Rajamani, a corporate vice president at Microsoft Research, among its backers.

The funding will go toward training the company’s formalization and prover models, hiring research engineers and adding domain experts across the regulated verticals.

The seed round was led by Khosla Ventures, with participation from Accel, BoldCap, Nexus Venture Partners, Premji Invest and Unbound Capital Ltd.

Image: Pramaana Labs