摘要： Pramaana Labs 在 2026 年 6 月 17 日宣布完成 2,700 萬美元種子輪，由 Khosla Ventures 領投，要把 LEAN 形式化驗證層放在 LLM 輸出之上。這種設計瞄準法律、稅務和藥物發現等高風險場景，但每個領域都需要專家把規則形式化，工程既費工也耗時。
新創公司 Pramaana Labs 於 2026 年 6 月 17 日對外宣布，已完成 2,700 萬美元的種子輪募資；本輪由 Khosla Ventures 出任領投方，Accel、BoldCap、Nexus Venture Partners、Premji Invest 及 Unbound 也加入跟投行列。這家公司挑了一條業界少有人走的路：把「形式化驗證」這門數學證明領域的技術帶進 LLM 產品，在模型輸出之上加設一層確定性驗證器把關，專攻一出錯就可能賠上人命、虧掉大錢或失去自由的場景。
這個時間點格外值得留意——前一天（6 月 16 日），同樣以 LLM 可靠性為業的新創公司 Probably 才剛宣布募得 900 萬美元種子輪。短短兩天接連兩輪融資，意味著「LLM 輸出必須可驗證」已不只是研究圈口號，而是投資人買單的主題。
形式化驗證是什麼，憑什麼拿來約束 LLM
先把名詞講清楚：形式化驗證指的是以數學手段證明系統符合規格的技術，過去主要活躍於晶片設計與數學定理證明。而 Pramaana 的核心工具挑了開源證明語言 LEAN——數學界長年靠它核驗定理證明，Pramaana 則把同一套思路借過來，改為檢查 LLM 的推論結果。
「世界上最難的問題不是無解，而是未被形式化。」說這句話的，正是共同創辦人兼執行長 Ranjan Rajagopalan。他的主張是：任何「答錯會讓人損失健康、金錢或自由」的領域，背後必有明確規則，而規則有辦法寫成可供驗證的形式。
架構拆解：LLM 之上疊一層確定性驗證
這套系統以雙層方式運作：一層沿用傳統 LLM，扛起自然語言的理解與彈性；另一層是確定性的驗證層，逐筆核對 LLM 交出的輸出是否合乎規則。在這樣的分工下，LLM 不再充當「答案產生器」，改任「提案者」，對外的最終答案一律由驗證層背書。
Pramaana 為每一個應用場景，都在領域專家監督下量身打造一套 LEAN 式驗證系統——這份工作費工耗時，卻也是最難被抄走的護城河。法國的 CATALA 專案是現成先例：它把法國大多數稅制與福利制度寫成可執行的程式碼，在工程層面證實「把規則世界形式化」確實辦得到。
先攻最輸不起的市場：法律、稅務與藥物發現
法律、藥物發現與稅務，是 Pramaana 排在最前面的三個目標垂直領域。人事編制也與這盤布局呼應：稅法方向由前美國國稅局（IRS）局長 Danny Werfel 掌舵，監督網路安全與藥物發現兩套系統的教授，則來自 IIT Delhi、IIT Madras 與 UC Berkeley。
稅務把這套邏輯展示得最透徹。Rajagopalan 形容稅法「像數學一樣，有一大堆必須遵守的規則」，還說「一旦有了編碼化的版本，其上的推論就開始變成確定性的」。規則又多又不許出錯的確定性推理，向來是 LLM 最招架不住的一環，如今這塊缺口正好由驗證層直接補上。
Probably 同週登場：LLM 可靠性成了新戰場
搶在前一天發布融資消息的 Probably，可視為同一條路線的變體。創辦人是 Peter Elias，融資由 Andreessen Horowitz 出面領投，端出的第一款產品是資料科學工具：由 LLM 針對資料集作答，每個結果都掛上引用與稽核軌跡，底下撐著一套 harness，Elias 稱之為「資料科學動力裝」——凡與資料集對不上的輸出，確定性驗證器一律拒收，模型本身的訓練也以這個驗證器為準。
有兩個細節值得記下。第一，Probably 目前的模型「比前沿模型弱四個等級」，卻能在桌機等本地硬體上運轉，token 成本隨之大幅縮水——這正呼應 Elias 的原則：「harness 工程做得越好，模型就可以越弱。」第二，他把大實驗室遲遲不出手的原因講得毫無保留：「你修正模型的次數越多，他們賺得越多」。
給開發者的三個結論
歸納起來是三件事。第一，可靠性的戰場正從「prompt 技巧」層級往「架構」層級移動：由 LLM 出提案、交確定驗證器裁決的雙層設計，將成為高風險應用的標準配備。第二，有了驗證層，你能用更小、更便宜的模型，換到逼近確定系統等級的正確率，成本結構也就此翻新。第三，形式化規則庫（CATALA 之於法國稅法即是範例）是新的護城河——誰搶先把某領域的規則編碼化，誰就握有進駐該領域 AI 的入場券。