Pramaana Labs raises $27 million to bring formal verification to AI

Pramaana Labs said Wednesday it raised a $27 million seed round as the startup builds AI systems for fields that punish errors with fines, lost time or harm to patients.

Khosla Ventures led the round. Accel, BoldCap, Nexus Venture Partners, Premji Invest and Unbound also invested.

Pramaana plans to use formal verification, a computer science method that proves software behavior with math, to check the work of large language models. The company will start with domains such as law, tax preparation, drug discovery and cybersecurity.

The pitch lands at a tense moment for enterprise AI. Companies have spent the past three years testing chatbots, coding assistants and document tools. Many pilots stall once teams ask the hard question: Can employees trust the output in work that carries legal, financial or medical risk?

Pramaana’s answer pairs a conventional LLM with a deterministic verification layer. The model handles language, ambiguity and broad reasoning. The verification system checks whether the output follows a formal set of rules.

That approach gives Pramaana a clearer lane than startups that promise better prompting or broader retrieval. The company wants domain experts to convert rules into executable systems, then use those systems to validate AI answers before customers act on them.

For tax, that means codifying rules from the tax code. For drug discovery, it means checking claims against defined scientific and computational constraints. For cybersecurity, it means asking whether an AI system’s conclusion follows from a model of the system under review.

Pramaana co-founder and CEO Ranjan Rajagopalan told TechCrunch that tax law fits the model because practitioners already work with strict rules. Once engineers encode those rules, the system can force the AI’s reasoning into a form that a verifier can check.

The company draws on ideas from Lean, an open-source theorem prover that mathematicians and computer scientists use to verify proofs. Lean has gained attention as researchers use it to formalize math and test whether AI systems can produce proof steps that machines can check.

Pramaana also points to Catala, a French project that turns legal rules into executable code. Catala shows the same core idea in public policy: Lawyers and programmers can translate statutes into systems that produce auditable results.

The market context helps explain the size of the seed round. AI spending has moved from experimentation budgets into operational plans, but many buyers still treat reliability as the gate. A hallucinated citation in a memo embarrasses a user. A bad tax position, a missed drug interaction or a flawed security conclusion can cost money or trigger liability.

Formal verification gives vendors a stronger answer than confidence scores. A model can sound certain and still fail. A verifier can reject an answer that violates encoded rules.

Pramaana still faces a hard build-out. Formal systems require specialists who understand both the domain and the proof machinery. Tax experts, lawyers, chemists and security researchers need to help engineers define the rules. Customers also need evidence that the system covers enough of a domain to matter in production.

That labor can slow growth. Each vertical demands its own rule base, expert review and test set. Pramaana has started adding that expertise: former IRS Commissioner Danny Werfel is advising on tax, while professors from IIT Delhi, IIT Madras and the University of California, Berkeley, are overseeing work tied to cybersecurity and drug discovery.

The broader AI market has split into two camps. One camp tries to make models more capable through scale, better data and tool use. The other tries to wrap models in systems that constrain behavior. Pramaana sits in the second camp, where buyers care less about open-ended fluency and more about whether a system can defend its answer.

That distinction matters for enterprise adoption. A lawyer, tax adviser or scientist does not need an AI system that sounds right. They need a system that shows its work in a format another expert, or another machine, can inspect.

Pramaana’s $27 million round gives the startup room to build those domain systems before larger AI platforms absorb the idea. Cloud providers and model labs already sell governance, retrieval and evaluation tools. Formal verification could become another layer in that stack if regulated customers demand stronger proof.

For now, Pramaana’s bet is narrower: AI will enter high-risk work only after teams can check its reasoning against rules they trust. The companies that solve that problem can sell into budgets that generic chatbots cannot reach.