活動主題演講：以下是 @thejonanshow 在 ETHDenver 2025 演講中的 5 個主要見解。

1. 形式驗證的重要性
Jonan 強調，形式驗證提供了程式行為的數學證明，這對於複雜的系統至關重要。他指出，雖然它不能保證整個程式的正確性，但它允許開發人員在他們的系統中聲明某些不變量。例如，聲明銀行的集體餘額永遠不應低於零，這說明了如何驗證特定規則以維持系統的完整性。

2. Certora 的開源倡議
Jonan 分享了關於他所工作的公司 Certora 的令人興奮的消息，該公司最近將其形式驗證的驗證器開源。這項倡議旨在簡化形式驗證的過程，使該工具更容易被軟體開發人員使用。他鼓勵與會者嘗試一下，強調其易用性以及增強軟體可靠性的潛在好處。

3. 關於形式驗證的誤解
根據 Jonan 的說法，Web3 領域之外的許多人對形式驗證存在誤解，通常基於過時的觀點認為它是不切實際的。他強調，現代應用程式可以從形式方法中受益匪淺，並指出雖然證明複雜系統的每個方面可能並不總是可行的，但可以並且應該驗證基本的不變量，以避免重大的陷阱。

4. 轉向宣告式程式設計
Jonan 提倡從命令式程式設計轉向宣告式程式設計，強調軟體工程師通常以詳細的程序方式進行程式設計，而不是定義期望的結果。這種轉變可以使軟體能夠確定如何實現指定的結果，從而可能降低複雜性並促進與可能協助軟體開發的 AI 技術更好地整合。

5. AI 在軟體開發中的影響
Jonan 指出了 AI 越來越多地整合到軟體開發工作流程中。雖然他承認 AI 可以帶來的效率，但他對 AI 傾向於「產生幻覺」或產生意想不到的結果表示擔憂。他認為有必要採用強大的形式驗證方法來發現使用 AI 時可能出現的差異，並堅持認為明確的不變量可以防止此類陷阱。

您可以在此處查看我們的完整見解，100% 免費：https://t.co/bQ2B2KBeCc