Mistral 開源 Leanstral 1.5：讓形式驗證走入每個開發者的工作流——並找到 5 個真實漏洞

對大多數軟體開發者而言，「形式驗證」向來是航太產業、安全關鍵汽車系統，或從未在截止日期前出貨的學術研究人員才會碰的東西。Mistral 想改變這個現狀。2026 年 7 月 4 日，這家法國 AI 公司以 Apache 2.0 授權發布了 Leanstral 1.5——一個以 Lean 4 證明助理為核心、專為軟體數學驗證設計的開放權重模型。Lean 4 由微軟研究院開發，是當前最受矚目的形式化數學工具之一。

這次發布最引人注目的聲明是：在測試 57 個開源程式庫時，Leanstral 找到了 5 個此前未知的漏洞，其中一個在除錯模式下會導致崩潰，在正式發布模式下則會造成靜默的數據損毀。這正是傳統測試最容易漏掉的那類錯誤。

形式驗證究竟是什麼

傳統軟體測試的做法是：對一組輸入執行程式，確認輸出符合預期。這個方法本質上是不完整的——你可以測試一百萬種情況，卻仍可能在第一百萬零一種情況讓生產環境當機。形式驗證採取完全不同的路徑：不執行程式，而是用數學證明來建立程式碼滿足特定規格的保證——不是針對樣本輸入，而是針對所有可能的輸入。

問題在於，撰寫形式證明向來極為困難且耗時。Lean 4 是一個強大的工具，主要使用者是學術數學家和少數形式方法工程師，要應用於工業程式碼，需要同時精通程式語言和證明助理——這種複合能力稀有到足以讓形式驗證在大多數開發流程中缺席。

Leanstral 透過自動化「生成證明」這一步，重寫了這個方程式。

模型架構與效能

Leanstral 1.5 採用混合專家（MoE）架構，總計 1190 億參數，每個 token 激活約 65 億參數——這種設計以相對低廉的推論成本實現高效能。上下文視窗達 25.6 萬 token，足以對相當規模的程式碼庫進行推理。模型目前在 Hugging Face 開放下載，beta 期間亦可免費透過 Mistral Labs API 使用。

各項基準測試的表現令人印象深刻。在形式數學推理的標準測試 miniF2F 上，Leanstral 達到滿分 100%，全面飽和。在廣泛用於評估定理證明系統的 PutnamBench（來自 William Lowell Putnam 數學競賽的題庫）上，Leanstral 解決了 672 題中的 587 題，遠超此前任何開放模型。

成本優勢同樣顯著。在 PutnamBench 上，Leanstral 的成本約為每題 4 美元；同等性能的 Seed-Prover 1.5 需要 300 美元以上，Aleph Prover 則在 54 到 68 美元之間。對於沒有專屬研究預算的開發者，這讓形式驗證的實際嘗試成為可能。

在 57 個程式庫中找到 5 個真實漏洞

Leanstral 實用性最有力的證明，不在於 benchmark，而在於真實程式碼上的表現。Mistral 使用 Aeneas 工具將 Rust 程式碼轉譯為 Lean 4，再由 Leanstral 生成正確性條件並嘗試加以證明，測試了 57 個開源程式庫。

系統找到了 5 個此前未被回報的漏洞，最具代表性的是 Rust 函式庫 varinteger（用於讀寫可變長度整數）中 zigzag 解碼函式的整數溢位問題。這個溢位在除錯模式下（Rust 的邊界檢查會捕捉到算術錯誤的除錯建置）導致崩潰，在正式發布模式下（不進行邊界檢查）則造成靜默的數據損毀。這個漏洞讓 varinteger 的完整測試套件毫無察覺地通過了。

這正是形式驗證特別擅長發現的那類錯誤：只在特定邊界值輸入時才觸發的溢位，隨機或覆蓋率導向的測試套件幾乎不可能生成這樣的輸入。而對「所有輸入下函式均正確」的證明嘗試若失敗，本身就構成了對漏洞的偵測。

Lean 4 生態系的意義

選擇 Lean 4 作為目標證明助理是經過深思熟慮的。Lean 4 占有一個獨特的位置：它同時是一種函數式程式語言和一個證明助理，這意味著用 Lean 4 撰寫的程式本身可以攜帶正確性的數學證明。隨著 DeepMind 的 AlphaProof 採用 Lean 4，這個語言吸引了越來越多數學家的關注，微軟研究院也持續在其開發上投入資源。

Leanstral 與 Mistral 的代理編碼平台 Mistral Vibe 原生整合，讓形式驗證得以作為標準開發流程的一部分被調用，而非一個獨立的專業步驟。模型同時支援推論時算力擴展（test-time scaling）——在 PutnamBench 上，從 5 萬 token 擴展到 400 萬 token 的計算量，解題數量從 44 題增加到 587 題。

對軟體品質的意義

形式驗證向來遵循「反帕雷托法則」：驗證最後 20% 的程式碼，往往需要耗費 80% 的心力，讓大型系統的完整驗證在經濟上難以實現。Leanstral 近期最務實的應用場景，不是完整的程式驗證，而是針對高價值程式碼路徑的選擇性驗證——密碼學例程、解析器實作、對不受信任輸入的算術運算、協議狀態機。

這些恰好是測試覆蓋率與真實正確性之間的落差最致命、漏洞影響最深遠的程式碼區域。一個可變長度整數編解碼器中的整數溢位，往往會在兩年後演變成一個 CVE 漏洞通報。

對開源維護者而言，Leanstral 提供了一個將形式驗證加入 CI 流程的實際理由：beta 期間免費的 API、Apache 授權的模型權重，以及通過傳統測試後仍能找到漏洞的實績。障礙不再是成本或取用門檻，而是需要學習足夠的 Lean 4，寫出模型能夠嘗試證明的規格。

這最後一步依然不容小覷。Leanstral 自動化的是證明生成，但規格必須由人撰寫——而且必須準確描述程式碼應有的行為。如果規格有誤或不完整，再完美的證明也只是在錯誤的前提下成立。這是形式驗證的根本挑戰，任何模型都無法完全自動化：「正確」的定義，本身就需要人的智識判斷。

話雖如此，對於 Leanstral 實際找到的那類漏洞——算術溢位、邊界條件、偏移一位的錯誤——規格通常足夠直接，讓自動化確實有效。以每次 4 美元在 57 個程式庫中找到 5 個漏洞，這個成果足以吸引任何維護性能關鍵或安全敏感程式碼的團隊認真考慮。

開源即策略

Apache 2.0 授權值得深入思考。Mistral 一貫將開源作為商業策略，Leanstral 延續了這個路線。開放模型權重、採用寬鬆授權，意味著商業部署、企業微調和研究使用均無限制，與那些 API 呼叫更便宜但無法自行部署或客製化的閉源競品形成明確區隔。

在受監管行業——金融、醫療、航太——將驗證工作負載部署在自有基礎設施而非第三方 API 上，往往是決定性因素。Leanstral 的開放授權讓這成為可能，這是競品模型做不到的。

Leanstral 的發布恰好與 OpenAI GPT-5.6 Sol 宣稱以形式手段證明循環雙覆蓋猜想同在一週發生。近期記憶中最重要的兩個形式推理公告在數天之內相繼出現，是巧合，還是前沿正在加速轉向的訊號？無論如何，形式驗證——這個曾是少數專家才能觸碰的領域——正在以前所未有的速度向每一個開著終端機的開發者靠近。