智能合約的形式化驗證仍然是一個未解決的巨大問題。首先，讓我們通過“形式化證明（formal proof）”來理解“形式化驗證（formally verify）”的意思。在數學上，“形式化證明”是一種數學證明，計算機可以通過基本的數學公里和推理規則（inference rules）來證明它。
在程序方面，形式化驗證是一種判斷程序是否能按預期運行的方法。具體的規約語言可以來描述輸入和輸出之間的函數關系。也就是說，如果在程序里聲明了一個不變量，則我們應該證明這個聲明的存在。
規范語言的一個例子是 Isabelle，它是一種通用證明輔助，可以在形式化語言里表達數學公式，還提供了工具在邏輯運算上來證明這些公式。另一種規范語言是 Coq，這是一種用來書寫數學定義、執行算法和定理的形式語言。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
