We Raised $27M to Build a Compiler for Mission-Critical AI

AI can produce the answer. It cannot yet prove the answer is right.

In critical domains like tax, law, medicine, finance, and governance, that distinction decides everything. This distinction creates an accountability and trust gap. To be honest, a HOLE.

We started Pramaana to close this gap. 

Today, we're announcing $27 million in seed funding led by Khosla Ventures, with Accel, Nexus Venture Partners, Premji Invest and BoldCap, to take AI from probably right to provably right.

The idea is simple: AI should not just sound like an expert. It should be able to prove its work.

Jim Simons spent his career turning one messy human domain, the markets, into math. Renaissance Technologies didn't trade on hunches. It traded on math, and it became the most profitable fund in history. The lesson was clear: when math enters a particular domain, it solves it. 

A couple of years ago, AlphaProof showed the next step. Given some of the hardest problems in competition mathematics, a machine did not just find the answers. It wrote the formal, machine-checked proofs for them, in Lean. The proving itself was automated.

Lean proved theorems. We're building the infrastructure that lets it prove the real world.

That is the announcement. Here is the conviction behind it.

Chapter One: The Age of Creation

Every technology that reshaped civilization arrived in two waves. First creation, the messy, generative, world-making wave. Then proof is the slower wave that makes the new thing trustworthy enough for everyone to actually depend on it.

The first wave of AI was fluency and creation, and Transformers were the breakthrough. They gave us models that write, draw, code, and converse, and they rewarded one thing above all: speed. So the industry poured its capital into compute, the infrastructure to scale fluency. It worked. We got astonishing productivity and a real sense that the future had arrived early.

But fluency is not the same as truth.

While the world debates whether AI will take every job or launch every weapon, we still live in a world where ambulances sit in traffic, chronic disease goes undiagnosed, and an ordinary person cannot understand their own taxes in 2026. The bottleneck on solving these isn't imagination. It's the human expert, the doctor, the lawyer, the CPA, whose quality and quantity cannot scale to seven billion people.

Transformers can't break that bottleneck, because in high-stakes domains the architecture is probabilistic by design. It produces answers that are plausible, not answers that are proven. And in tax, law, healthcare, finance, and governance, plausible is the difference between a person keeping their health, their money, their freedom, and losing it.

This is the accountability gap. AI today has authority without accountability. It speaks like an expert and cannot be held to the standard of one. So a human stays in the loop, reading every diagnosis, checking every brief, signing every return, not as a decision-maker but as a liability shield. The most dangerous thing an AI can produce isn't a wrong answer. It's a confidently wrong answer that no one is accountable for.

Picture a CPA who reads every return her AI drafts, line by line, before she signs. Not because the AI is slow. It's faster than she'll ever be. She reads it because if it's confidently, invisibly wrong, the signature is hers, the liability is hers, and the machine that wrote it walks away clean. Multiply that one signature across every doctor, lawyer, and accountant alive, and you have the real ceiling on what AI can do for the world.

That ceiling is not a law of nature. It is an unsolved problem, and one of us had already spent three years learning exactly why.

Chapter Two: The Age of Proof

Krishnan spent three years at Glean building the first version of Glean Assistant, fighting hallucinations head-on. The harder he fought, the clearer it became: you cannot patch your way out of this. Reducing the error rate is not the same as eliminating the category of confident wrong answers. Hallucination in high-stakes domains isn't a product bug to be smoothed over. It's a research problem to be solved.

That realisation is what brought the three of us together.

A hundred years ago, a clerk in Madras filled notebooks with theorems he could see were true but could not get the world to accept, until he wrote to G.H. Hardy in Cambridge. Hardy recognised the work as world-class, brought Ramanujan to England, and spent much of his life proving what Ramanujan had intuited, long after Ramanujan was gone. Intuition created. Proof made it real. That pattern repeats through every great leap, from flight to the internet.

AI is at exactly that moment. The most important question of this decade isn't what AI can generate. It's what AI can prove. 

So we asked the question the first wave skipped: what is AI structurally not good at, and how do we solve precisely that?

Chapter Three: Lean for the Real World - The Compiler

A compiler takes something written in a language people can reason about and turns it into something a machine runs with total precision. It also does the thing that matters most here: it refuses to ship code that doesn't check out. We're building that for decisions instead of code. You bring a claim, a calculation, or an AI answer, and Pramaana compiles it against the rules that govern it. It either certifies the answer holds, or it tells you the exact rule that breaks. No probably. No, looks right. It compiles, or it doesn't.

Pramaana is the first company to apply formal verification to commercial, high-stakes domains at scale. We're building the auto-formalisation infrastructure and the prover that together deliver verifiably correct AI, where being wrong is not an option.

Simple to state, hard to do. Every regulated domain has rules: the US tax code, clinical protocols, and financial regulations. We encode those actual rules into a formal language a machine can reason over with mathematical certainty. When you ask a question, the system translates it into a formal statement, runs it through a proof engine, and does one of two things: it returns a machine-checkable proof that the answer is correct, or it tells you exactly which rule breaks and why.

It refuses to answer before it can prove. To date, it has never produced a confidently wrong verified answer.

That's the whole shift. When AI can prove its answers, the human in the loop stops being a liability shield. The doctor, the lawyer, the accountant stop being the review layer. And AI finally becomes what it was always supposed to be: the expert.

A claim that large is only as good as the people willing to stake their careers on it.

Who's building it

The three of us are IIT Madras alumni who spent years at the frontier of exactly this problem. Ranjan led Moderation at Google Maps, keeping a planetary-scale live database accurate. Krishnan built the first Glean Assistant and went to war with hallucinations. Sanjay was a Staff Research Engineer at Google DeepMind and a core contributor to the Gemini models, where he built the tool-use system and drove post-training for real-world tasks. Our team encompasses researchers from Deepmind, Meta, Microsoft, Uber and University of California, Berkley.

We left to build Pramaana around one conviction forged at the edge of frontier AI. The accountability gap is both the hardest unsolved problem in AI and its largest commercial opportunity.

We're not alone in that belief.

"I think this will turn out to be a very important area. Founders should work on things AI is not good at. Formalisation is exactly that. The hallucination problem is structural. Pramaana is building the infrastructure that lets us trust AI where being wrong is not an option." Vinod Khosla, Founder, Khosla Ventures.

"Autoformalization infrastructure is the unlock for superintelligence. Right now every high-stakes AI answer waits on a human to check it, so the system runs at the speed of that person. Once we formalize the rules of real-world domains, that bottleneck disappears. Done right, this doesn't just make AI better, it leads to abundance." Sathya Nellore Sampat, General Partner, BoldCap

"Pramaana's work is exciting because it builds on fundamental research to bring us closer to a future of seamless, trustworthy, and autonomous AI. Trustworthy AI should not require users to think like machines or become verification experts. As AI systems take on more complex tasks, trust should come from interpretable machine-checked guarantees built into the systems themselves." Prof. Gireeja Ranade, EECS, UC Berkeley

We're also partners with some of the world's leading minds in formal verification, including Pushmeet Kohli (VP, Google DeepMind) and Sriram Rajamani (Corporate VP, Microsoft Research), and by a frontier research lab spanning IIT Delhi, IIT Madras, and UC Berkeley, with our tax effort advised by former IRS Commissioner Danny Werfel.

What’s next

This funding goes toward training our formalisation and prover models, hiring research engineers, and scaling domain experts across regulated verticals, starting with tax, human diagnosis, cybersecurity, and financial compliance.

Go back to that CPA reading line by line. In the world we're building, she doesn't read it to catch the machine. She reads it because she wants to, and when she signs, a proof signs with her.

The world's hardest problems are not unsolvable. They are unformalised. We're here to change that, one provable domain at a time.

If that's your problem too, come build it with us.

— Ranjan, Krishnan & Sanjay