Formal verification just left the lab. Why we invested in Pramaana Labs.

‍

A doctor still reads every AI diagnosis. A lawyer still checks every AI brief. A CPA still signs every AI return. Not because the AI is too slow. Because when it's wrong in a high stakes domain, it cant be held responsible.

‍

So we keep the human in the loop. But what if we didn't have to? What if you could guarantee, with mathematical certainty, that the AI's answer is correct — and let the human go work on something higher-order than babysitting it? That's the premise of formal verification, and it's what Pramaana is building.

What is formal verification?

Formal verification isn't a new term. It's a sixty-year-old discipline that has quietly underwritten the things you already trust. Every modern CPU is formally verified before it tapes out, fly-by-wire aircraft software is certified against standards built on formal methods, and AWS uses TLA+ to verify the protocols behind S3 and DynamoDB.

‍

The concept is simple. You define a system in mathematical terms and write down a property you want to be true. A prover — Lean, Coq, Isabelle — mathematically checks whether the property holds across every possible input. This is completely different from vanilla testing — the output is a guarantee.

‍

The reason this discipline has lived inside math, code, and hardware for sixty years and nowhere else is two things. First, those domains hand you ground truth for free. A proof is right if it type-checks. Code is right if it matches the spec. Everything else — tax, contracts, medical guidelines, regulated finance — is written in English, contradicts itself in places, gets reinterpreted by courts and committees, and exists in no machine-readable form anywhere. There is no answer key.

‍

Second, even where you knew what you wanted to prove, the act of formalizing it was prohibitively expensive. Translating English statute into formal logic required someone fluent in both formal verification and the target domain, working at roughly a page a week. The entire US tax code at that rate would have taken a small army a decade. So nobody bothered.

What changed?

Two things happened, together but on separate tracks.

‍

The first is that AI made the process of formalizing a domain a lot easier than before. Pre-AI, it used to require a PhD doing it by hand, one statute at a time. AI, given it is an anything-to-anything converter in its most basic sense, can theoretically take a messy real-world domain and formalize it, assuming some guardrails.

‍

The second is that the ability to prove something also got easier. Lean is the language used to prove correctness and it draws from a library of math proofs called Mathlib. Mathlib is a community effort that has now become a real ecosystem. AI-driven proof generation is no longer speculative — it's something a serious research lab like Pramaana can build on.

What's the catch?

If this were easy, the foundation labs would have done it. They won't, not because they don’t want to, but because the chain of problems is long and definitely not straightforward.

‍

First, LLMs are notoriously bad at formalizing axioms in Lean directly. The training data is too thin and the type checker is too unforgiving. So you can't just point Claude at the Internal Revenue Code (in the case for tax) and ask for a formal encoding. You need an intermediate domain-specific language designed to be LLM-friendly and prover-friendly at the same time.

‍

Second, even if you translate the real, messy world into formal code, how do you ensure the translation is faithful? If two encoded rules contradict each other, is that a bug in your encoding or a real ambiguity in the statute? Pramaana's stack handles this through back-translation and an extreme amount of human checking.

‍

Third, how do you know what to formalize in the first place? Lets take tax as a first use case - it is not a closed system. It's open-ended, with judgment calls and jurisdictional variance and constant updates. To make it tractable, you have to define what counts as in-scope, draw boundaries, and ensure every situation maps to at least one rule. That scoping methodology is its own piece of IP — process knowledge learned over hundreds of formalizations.

How Pramaana works in practice

Pramaana is first and foremost a formal verification platform. Its first use case is tax. The company has been formalizing chunks of the US tax code — encoding statutes, regulations, and case law into machine-checkable rules. Think of it as the Mathlib of tax law. Every section formalized is permanent infrastructure that compounds. The tax code has 35,000 sections; they've started with the highest-impact ones and are working outward. The same template already scales to accounting rules like GAAP, banking rules like FDIC for financial institutions, medical prognosis and even football rules!

‍

The corpus is the foundation. The real product is what happens when you run a query against it. Imagine a mid-market business that just restructured, acquired something new, changed its sales practices. KPMG and Deloitte don't want the account. The CPA is doing ad-hoc work, not audit-proof analysis. The CFO wants to know: am I following the law, and am I saving the tax I'm supposed to be saving? Pramaana formalizes the question, runs it against the encoded rules, and returns an answer with a machine-checkable proof — or tells you exactly which rule blocks it and why. No iterative chat. No 95%. A guarantee.

Our thesis

The consensus AI thesis in 2026 so far is that the app layer is dead. The foundation labs will eat everything. We disagree, and Pramaana is the cleanest expression of our counter-thesis.

‍

The pattern is older than AI. In 2008, every venture investor said the same thing about the cloud: AWS will eat the app layer, but it didn't. Salesforce, Workday, Coupa, Anaplan, ServiceNow — all got built on top of the same substrate that was supposed to eat them. The app layer didn't die, it figured out where to add value the substrate couldn't.

‍

The same thing happens with AI. The model layer is the substrate. The companies that win at the app layer are the ones that can build full-stack initially - own the model, data, application surface - to show the art of the possible, while giving them optionality to provide the infrastructure for others to build other apps on top.

‍

Formal verification is one of those gaps. It started as a niche academic topic and is becoming infrastructure as AI moves into the high-stakes, autonomous use cases where 99% is unusable.

The team, and the signal

This is one of the rare teams that breaks our prior assumptions about how companies get built. Ranjan Rajagopalan led Google Maps Moderation — keeping a planetary-scale live database accurate. Krishnan Raghavan spent three years at Glean building the first version of Glean Assistant and fighting hallucinations, until he realized solving them is a research problem, not a product problem. Sanjay Ganapathy was a Staff Research Engineer at Google DeepMind with a decade in AI research — a core contributor to the Gemini models, builder of its tool-use system. All three are IIT Madras batchmates.

‍

The market signal has been hard to ignore. In their first year, Pramaana pulled 1,500+ registrations to their inaugural Verification Summit with mostly word of mouth. They assembled a world-class investor syndicate while residing outside the country. They got major press coverage on just seed raise. That's a lot for a team that's been around a year.

The shape of the bet

For sixty years, formal verification was the unsexy plumbing behind everything we already trusted. Pramaana is turning it into the engine of everything we couldn't trust before. We're excited to invest in their $27M round with friends at Khosla Ventures, Accel, Nexus, Boldcap and Unbound. Onwards.