Pramaana Labs raises $27M seed to bring formal verification to AI

Pramaana Labs announced $27 million in seed funding on Wednesday, a round led by Khosla Ventures with participation from Accel, BoldCap, Nexus Venture Partners, Premji Invest and Unbound. The startup plans to combine conventional large language models with deterministic, LEAN-style formal verification systems aimed at high-stakes verticals such as tax preparation, law and drug discovery.

What does Pramaana Labs plan to build?

Pramaana will build domain-specific formal verification systems using a LEAN-style approach, overseen by domain experts, for sensitive verticals including law, drug discovery and tax preparation. The company says each use case will have its own codified rule set; for tax law Pramaana is working with former IRS commissioner Danny Werfel, and professors from IIT Delhi, IIT Madras and UC Berkeley will oversee cybersecurity and drug discovery efforts.

Pramaana’s pitch is to make the decision layer around LLM outputs deterministic where stakes are high. The startup expects that codifying rules will allow reasoning above those rules to become predictable rather than purely probabilistic.

How does the LEAN-style verification layer work?

Pramaana pairs a conventional LLM engine with a deterministic verification layer built using tools derived from the open source LEAN programming language. The company runs the LLM to handle natural language queries and complex problem solving, then routes results through a formal verification layer that checks the LLM’s work against an executable, codified rule set.

Pramaana’s approach follows prior work in formalizing rules at scale; the company points to France’s CATALA project as precedent for turning tax and benefit rules into executable code. The startup says domain experts will oversee the construction of each formal system so the LEAN-style proofs and checks reflect legal, medical and technical constraints in each sector.

Why it matters

AI deployments in tax, law and drug discovery face much lower tolerance for error than consumer-facing applications. Enterprises struggle to move pilots into production partly because existing models can hallucinate or produce incorrect reasoning. Pramaana’s deterministic verification layer addresses that gap by ensuring LLM outputs conform to a formally codified rule set, turning some of the model’s reasoning into something checkable and predictable.

CEO Ranjan Rajagopalan framed the idea around rules and determinism: "It’s like math in the sense that you have a lot of rules that you need to abide by," he said, describing tax code as an example where codification could make reasoning deterministic. The company is positioning formal verification as a way to reduce costly errors where being wrong can affect health, money or liberty.

What to watch

Watch whether Pramaana moves from funding to demonstrable domain deployments, starting with the tax work led by Danny Werfel and the cybersecurity and drug discovery projects overseen by professors from IIT Delhi, IIT Madras and UC Berkeley. Adoption will hinge on whether LEAN-style formal systems can be built fast enough and kept up to date for regulatory and scientific domains that change frequently.

Pramaana’s seed round and its choice of investors give the company runway to prototype these systems. The next signals to look for are published case studies or pilots that show the verification layer catching or preventing errors an LLM alone would have missed.