# Pramaana Labs 获 2700 万美元种子轮融资，用形式化验证提升 AI 可靠性

- 来源：TechCrunch：AI（RSS）
- 作者：Russell Brandom
- 发布时间：2026-06-17 22:15
- AIHOT 分数：49
- AIHOT 链接：https://aihot.virxact.com/items/cmqi6614b05ytslf0wr9gvhdz
- 原文链接：https://techcrunch.com/2026/06/17/pramaana-labs-raises-27-million-seed-round-from-khosla-ventures-to-bring-formal-verification-to-ai

## AI 摘要

Pramaana Labs 宣布获得 2700 万美元种子轮融资，由 Khosla Ventures 领投，Accel、Boldcap 等跟投。该公司致力于将形式化验证引入 AI 系统，针对法律、药物发现和税务准备等高敏感领域，解决模型幻觉和错误问题。其系统在传统 LLM 之上叠加确定性验证层，利用开源 LEAN 编程语言确保输出正确。每个用例由领域专家监督构建专属形式化验证系统，团队已邀请前 IRS 委员及多所大学教授参与税务、网络安全和药物发现系统的开发。

## 正文

As enterprises struggle to turn AI pilot programs into functional parts of their business, reliability has taken center stage. A new startup is hoping to solve that problem by drawing on the tools of mathematical formalization, combining one of computer science’s most reliable systems with one of its most chaotic.

On Wednesday, Pramaana Labs announced $27 million in seed funding led by Khosla Ventures, with participation from Accel, Boldcap, Nexus Venture Partners, Premji Invest, and Unbound.

Pramaana will focus on highly sensitive verticals like law, drug discovery, and tax preparation — where errors can be costly and reliability is at a premium. Deploying AI in those systems will require stronger protections against hallucinations and errors than we currently have. But as Pramaana co-founder and CEO Ranjan Rajagopalan sees it, they’re also uniquely suited to formalization.

“It’s like math in the sense that you have a lot of rules that you need to abide by,” Rajagopalan told TechCrunch, describing the rules of the tax code. “Once you have a codified version of it, the reasoning on top of it starts becoming deterministic.”

Pramaana’s system still runs on a conventional LLM, giving it the flexibility to answer natural language questions and tackle complex problems that conventional computers can’t handle. But there’s a deterministic layer on top of that LLM ensuring the LLM’s work checks out.

This combination of an LLM engine with deterministic verification is a popular setup; Pramaana’s unique approach is to use the tools of formal verification — drawing on the open-source LEAN programming language used to verify mathematical proofs. There’s real precedent for much of this work; Rajagopalan points to France’s CATALA project, which formalizes much of the country’s tax and benefit system into executable code.

For each use case, Pramaana will build its own LEAN-style formal verification system, overseen by domain experts. For tax law, the company is working with former IRS commissioner Danny Werfel, while professors from IIT Delhi, IIT Madras, and UC Berkeley oversee the cybersecurity and drug discovery system.

“The world’s hardest problems are not unsolvable. They are unformalized,” says Rajagopalan. “Every domain where being wrong can cost someone their health, money, or freedom has rules.”

Now, those rules just need to be codified.