Summary: Pramaana Labs announced a $27 million seed round on June 17, 2026, led by Khosla Ventures, to pair LLM proposals with LEAN-based deterministic verification in law, tax, and drug discovery. The approach targets high-stakes rule-bound work, but each domain requires expert formalization and slow, heavy engineering before the verifier can provide value.
Pramaana Labs, a startup, said on June 17, 2026 that it had closed a $27 million seed round: Khosla Ventures led, and Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound came in behind. Its product idea is rare in AI: formal verification — the discipline built on mathematical proof — carried into LLM products, with a deterministic checker set over model output, aimed at fields where one wrong call can cost a person their health, money, or freedom.
The timing deserves a second look. One day before, on June 16, Probably — another startup built around LLM reliability — unveiled a $9 million seed of its own. Two rounds in two days: verifiable LLM output is no longer just a research talking point; investors are paying for it.
Formal Verification, Briefly — and Why Point It at LLMs
The technique is formal verification: mathematics used to prove that a system meets its specification, a discipline long centered on chip design and theorem proving. Pramaana’s core tool, LEAN, is an open-source proof language — the very tool mathematicians trust to check proofs — repurposed to test what an LLM reasons.
“The world’s hardest problems are not unsolvable. They are unformalized.” That framing comes from co-founder and CEO Ranjan Rajagopalan, whose thesis runs: any domain where a wrong answer can cost someone their health, money, or freedom runs on rules, and rules can be recast in a form that can be verified.
The Setup: an LLM Topped by a Deterministic Verification Layer
The design stacks two tiers. One is a conventional LLM, contributing natural-language understanding and flexibility; the other is a deterministic verification layer that tests each thing the model emits against the rules. The LLM’s job shifts from answer machine to proposer, with the verifier’s stamp on the final answer.
Every use case gets a LEAN-style verification system of its own, assembled with domain experts supervising. The work is slow and heavy — exactly why it doubles as the moat. France’s CATALA project is the earlier proof of concept: it rendered much of the nation’s tax and benefit system as executable code, showing formalizing a rule-bound world can actually be engineered.
Starting Where Errors Hurt Most: Law, Tax, and Drug Discovery
Law, drug discovery, and tax preparation are the first three verticals, and the roster is built to match that bet. Tax law is the brief of Danny Werfel, previously commissioner of the IRS; the cybersecurity and drug-discovery systems are supervised by professors at IIT Delhi, IIT Madras, and UC Berkeley.
Tax lays the logic out most cleanly. In Rajagopalan’s telling, the tax code is “like math in the sense that you have a lot of rules that you need to abide by,” and “once you have a codified version of it, the reasoning on top of it starts becoming deterministic.” Rule-dense reasoning with zero error tolerance has always been the LLM’s weakest ground, and the verification layer is built to cover exactly that ground.
Probably Lands the Same Week: Reliability Turns into a Race
Probably, which unveiled its round one day earlier, plays its own variation of the theme. Peter Elias founded it, with Andreessen Horowitz backing it. Its opening product is a data-science tool: an LLM fields questions about complex datasets, each answer carries a citation and an audit trail, and under it all runs what Elias calls a “data science mech suit” — a harness whose deterministic validator throws out anything inconsistent with the dataset, and the LLM is trained against it.
Two details are worth holding on to. One: the model Probably runs today is “four classes weaker than the frontier models,” yet it operates on local hardware such as a desktop rather than a data center, which cuts token costs sharply — a working demonstration of Elias’s principle that “the better your harness engineering is, the weaker the model can be.” Two: on why the big labs have stayed away, he is unsparing — “they make money the more times you have to correct the model.”
What Builders Should Take Away
Three conclusions follow. First, reliability work is climbing from prompt tricks up to architecture: the two-tier design, with the LLM proposing and a deterministic verifier ruling, is on its way to becoming the norm for high-stakes applications. Second, with a verification layer you can trade down to smaller, cheaper models and still land near-deterministic accuracy — and the cost structure flips. Third, formalized rule bases — CATALA’s encoding of French tax law as the template — are the new moat: whoever codifies a domain’s rules first holds the ticket to AI in that domain.