補齊算術電路約束，避免錯誤敘述通過證明驗證

值得記下的 5 件事

1. [13:40]
   電路外算出的提示值不能直接信任 提示值是協助產生見證資料、也就是用來滿足電路條件的數值，而非強制規則

   Sledd 說明，惡意證明者可以替換見證產生器，或自行指定提示值；只有電路實際檢查的約束，才能限制這些選擇。

2. [21:20]
   二選一電路必須明確限制選擇值 Sledd 示範，只有選擇公式，不能保證輸出來自兩個輸入之一

   在含十一個元素的有限體中，也就是加法與乘法都取除以十一餘數的運算環境，其他選擇值也可能通過等式。加入 s×(s−1)=0，才能強制 s 為零或一。

3. [31:20]
   不同模數的運算不能漏掉商的範圍檢查 電路若要檢查另一種模數下的運算，不能只靠一條表面相符的等式

   Sledd 以 gnark 漏洞說明，證明者若能任意選擇商，就可能讓錯誤結果通過；此外還須檢查曲線點是否屬於指定群組、必要數值是否非零，以及分解後各數值的範圍。

4. [40:20]
   測試應尋找能通過檢查的錯誤資料 Singh 指出，只測試依預期流程產生的見證資料，不足以揭露約束缺漏

   形式化驗證可將反例搜尋轉成檢查條件能否同時成立的問題；排除反例的結論只適用於所建模型，變數過多也可能使工具無法完成求解。

5. [47:00]
   人工智慧與證明工具仍需人工把關 Singh 介紹團隊結合人工智慧稽核、用來轉換電路表示方式的 LLZK，以及 Lean 證明工具的做法

   他說 Lean 主要用來檢查公式；公式正確不代表輸入已受妥善限制，這些機制單獨使用都不完整，仍需要人工稽核。