Pramaana Labs Raises $27M for Provably Correct AI
Pramaana Labs uses the LEAN proof language to attach a mathematical certificate to every AI answer in high-stakes domains like tax, law, and drug discovery.
7 min read
A tax attorney's AI assistant tells her client that a $12,000 home-office renovation is fully deductible. The client files. Two years later, an audit uncovers the deduction was invalid - a narrow carve-out in section 280A that the language model had never reliably encoded. The client owes back taxes, penalties, and interest.
That scenario isn't hypothetical in structure. It's the exact failure mode that AI hallucination creates in regulated industries: confident answers, no traceability, expensive consequences. Pramaana Labs, a startup founded in September 2025 by three IIT Madras alumni, raised $27 million in seed funding on June 17 to attack this problem from the bottom of the stack. The round was led by Khosla Ventures, with participation from Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound.
The pitch: attach a mathematical proof to every AI output, so an answer in law, tax, or drug discovery comes with a certificate rather than a confidence score.
TL;DR
- $27M seed led by Khosla Ventures, targeting regulated domains where AI errors carry legal consequences
- Core technology converts statutes and clinical protocols into LEAN code - the same proof language used by mathematicians to verify formal theorems
- Every answer ships with a machine-checkable proof, or the system refuses to respond rather than guess
- Query translation still uses an LLM, but the proof engine, not the language model, makes the correctness decision
- Target verticals: tax, law, drug discovery, cybersecurity - with domain advisors including former IRS Commissioner Danny Werfel
System layers (in order):
- Domain experts encode rules as LEAN predicates
- LLM translates natural language query to formal statement
- Proof engine assesses statement against encoded rules
- Returns proof + answer, or specific counterexample + refusal
How It Works Under the Hood
Layer 1 - Encoding the Domain
The foundation is a formal model of the domain's rules. Lawyers, physicians, and tax specialists work with Pramaana's team to encode statutes, regulations, and clinical protocols as executable LEAN code. Each rule becomes a verifiable predicate. CEO Ranjan Rajagopalan frames the starting insight this way:
"The world's hardest problems are not unsolvable. They are unformalized."
For a tax system, this means writing LEAN definitions for every relevant section of the code - including carve-outs, exceptions, and cross-references between clauses. The result is something like law that can be compiled.
Pramaana draws on France's CATALA project as a precedent. CATALA has been formalizing French tax and benefits law as executable code, demonstrating that the approach is technically viable for real-world regulatory complexity. Encoding is slow and expensive, but it produces something no LLM can: a ruleset that's auditable line by line.
Layer 2 - Translating the Query
When a user submits a question, an LLM converts it from natural language into a formal statement the proof engine can assess. This is a meaningful architectural choice. The LLM isn't generating the answer - it's only handling the translation. The language model's failure surface gets narrowed to one task: turning a question into a formal expression. If that expression isn't well-formed, the proof engine rejects it before any answer is produced.
This is structurally different from retrieval-augmented generation, where the language model synthesizes a final answer from retrieved documents. In Pramaana's system, the language model is middleware.
Layer 3 - Proof or Rejection
The LEAN proof engine evaluates the formal statement against the encoded rules. Three outcomes are possible. First: the rules support the query, and the system returns a proof - a machine-checkable certificate that traces back to the specific statutory language that justifies the answer. Second: the rules contradict the query, and the system returns a counterexample - the exact clause or precedent that blocks the claim. Third: the query touches a scenario the formal model doesn't cover, and the system refuses to answer rather than guess.
Rajagopalan described the output directly: "We turn statute and regulation into machine-verifiable code, so every output ships with mathematical proof of correctness."
Vinod Khosla framed the broader goal at the inaugural Verification Summit in San Francisco on June 10, 2026: "Auto formalization is a way to get at the things AI doesn't do well."
The domains Pramaana targets - tax, law, drug discovery - are defined by codified rules that can in principle be formalized. The challenge is doing that at the scale and accuracy real deployments require.
Source: pexels.com
A Minimal Example
A simplified version of what a rule and its proof look like in LEAN:
-- Home office deduction: requires exclusive, regular, and primary use
def homeOfficeDeductible (exclusiveUse : Bool) (regularUse : Bool) (primaryPlace : Bool) : Bool :=
exclusiveUse && regularUse && primaryPlace
-- Query verification: does this case satisfy the deduction rule?
theorem canDeductHomeOffice
(h1 : exclusiveUse = true) (h2 : regularUse = true) (h3 : primaryPlace = true) :
homeOfficeDeductible exclusiveUse regularUse primaryPlace = true := by
simp [homeOfficeDeductible, h1, h2, h3]
In a real deployment the encoded rules are vastly more complex - covering phase-outs, exceptions, and interactions between dozens of clauses. But the architecture is the same: formal definitions, formal queries, proof engine as the decision layer rather than a language model producing text.
This is related territory to Mistral's Leanstral formal code proof agent, which demonstrated that LEAN-based verification can be integrated into AI workflows at competitive cost. Pramaana is extending that logic from mathematical proofs into regulated domains.
Formal Verification vs Alternatives
| Approach | Accuracy guarantee | Explainability | Update cost | Primary failure mode |
|---|---|---|---|---|
| Formal verification (Pramaana) | Proof or refusal | Full trace to rule text | Re-encode changed clauses | Incorrect or missing formalization |
| RAG | None - retrieval can miss or misrank | Document citations | Add/update documents | Plausible but wrong synthesis |
| Fine-tuning | None - probabilistic | Post-hoc attention analysis | Retrain on new data | Confident hallucination |
RAG and fine-tuning produce answers. Formal verification produces answers with receipts - or doesn't answer at all.
Pramaana's public positioning leans hard on the proof metaphor - the startup's tagline is "AI That Proves Its Work."
Source: pramaanalabs.ai
When To Use It
Pramaana's approach makes sense for a specific class of problem:
- The domain has codifiable, explicit rules (statutory law, medical protocols, financial regulations)
- Errors carry legal, financial, or safety consequences
- Rules are stable enough to justify the formalization effort
- A refusal-to-answer is acceptable when a query falls outside the formal model
It's the wrong tool for:
- Creative or advisory tasks with no ground truth
- Domains that resist formalization - areas where judgment and context matter more than rules
- Fast-moving information that changes too frequently to re-encode
- Situations where users need a best-effort answer rather than proof-or-nothing
The coverage boundary matters. Terence Tao made a related point in a different context: verification remains hard even when generation becomes easy. Pramaana is betting that the hard part is formalization, not proof-checking, and that tooling and AI assistance can compress the encoding effort.
Known Gotchas
Encoding errors spread silently
If a rule is encoded incorrectly in LEAN, the system will prove wrong things with full mathematical confidence. The proofs are only as good as the formalization. A mis-encoded carve-out means every query that touches that carve-out gets a confident, certified, wrong answer. Domain expert review at the encoding stage is critical - and that review is expensive.
Hard failures at coverage boundaries
When a query touches a scenario outside the formal model, Pramaana's system refuses to answer. That's the correct safety behavior, but to a user expecting a response it looks like a broken product. Communicating coverage boundaries to end users is an UX problem the company hasn't publicly addressed.
Proof engine latency
LEAN proof checks for complex rule sets aren't instant. A multi-clause tax question evaluated against a large formal model can take seconds. For real-time conversational applications, this creates a ceiling on deployment contexts.
The bootstrapping cost
Building the initial formal model requires domain experts and formal methods engineers working closely together. Pramaana is using part of the $27M to train "formalization models" - AI systems that can translate domain text into LEAN with expert review rather than expert authorship. Whether that automation can meaningfully accelerate encoding is unproven.
The Verification Summit on June 10 drew formal methods researchers and domain experts to San Francisco. That Khosla himself headlined it signals conviction from the investor side. The model is early: no public customers or product demos were announced with the funding. What Pramaana has shipped is a thesis - that the formal verification toolchain built for mathematics can be adapted to the regulation-dense domains where AI reliability actually needs to be proven.
Sources:
