Prompts Aren’t (Good) Specs: Correctness in the LLM Era

這場演講的起點是講者看到 OpenAI 某演講提出「英文 spec 將成為新程式碼」的概念後感到不安。她的核心疑慮在於：自然語言本質上是模糊的，你無法執行它、無法確認 AI 是否真的理解了你的意圖、也無法保證所有 edge case 都被涵蓋。更重要的是，如果真的把靜態分析器、編譯器這些幾十年積累的工具全丟掉，換來的只是更難讀的 AI 生成 diff，那對安全性的威脅將無從管控。她觀察到整個行業對 AI 既興奮又疲憊——興奮於生產力提升，疲憊於閱讀大量 AI 輸出的 code 卻又感到與它完全脫節。

她的答案是反過來：不是把工具丟給 AI，而是把更好的工具給 AI。她與團隊開發的 Quint 是一種可執行規格語言，定位在英文（無法執行）與程式碼（難以判斷正確性）之間。Quint 的關鍵能力是讓你用問題的形式查詢規格——「這個狀態可以被達到嗎？」「這個行為在任何情況下都成立嗎？」——從而在真正動 code 之前，先建立對協議設計的信心。這對去中心化系統、共識引擎這類高複雜度協議尤其重要，因為 LLM 在沒有足夠護欄的情況下極容易偏離預期行為。

具體工作流程分三段：首先讓 AI 根據需求修改 Quint spec；接著開發者親自用 Quint 驗證這份 spec，確認行為符合預期；只有在對 spec 有信心後，才將它作為 context 輸入，讓 AI 去修改實際程式碼，並同步用 model-based testing（類似 differential fuzzing）驗證 code 行為與 spec 是否一致。這個流程的核心價值是「讓驗證前移」——開發者重新建立與協議的連結，而不是盲目信任 AI 的大量輸出。

這套方法並非玩具案例，而是直接應用在 Malikite 這個生產級區塊鏈協議上。Malikite 從設計階段就全程使用 Quint，今年更被 Circle（USDC 發行方）收購，成為其新區塊鏈 Arc 的核心。講者團隊用這套 AI + Quint 工作流程完成了一個複雜的協議變更，而工程師原本的預估是兩個月——實際不到一週完成。這個結果讓她確信：AI 時代工程師的核心工作已經轉移，從「寫 code」變成「定義正確性並驗證 AI 輸出」，而 prompt 本身並不是合格的驗證工具。