合約的簡單性使之成為創建形式規范并用這種規范進行形式驗證的理想選擇——數學上可以證明代碼遵循了規范。對EVM(
以太坊)編譯也已經做過形式化驗證了,需要形式化驗證語言來重寫合約。隨著EVM形式化語義的發布,近來EVM的形式化驗證得到了越來越多的關注。
下一步還要用低階語言(LLL)或純EVM字節代碼來編寫簡單的多重簽名合約,以便限制Solidity編譯器的風險。
總結
本文探討了一種更加簡單的多重簽名以太坊合約,在此合約下,用一個交易發送所有分離簽名前,會先在鏈下匯總這些簽名。這樣做簡化了鏈上智能合約代碼,方便審查,且為將來進行形式化驗證提供了可能性。