合约的简单性使之成为创建形式规范并用这种规范进行形式验证的理想选择——数学上可以证明代码遵循了规范。对EVM（以太坊）编译也已经做过形式化验证了，需要形式化验证语言来重写合约。随着EVM形式化语义的发布，近来EVM的形式化验证得到了越来越多的关注。

下一步还要用低阶语言（LLL）或纯EVM字节代码来编写简单的多重签名合约，以便限制Solidity编译器的风险。

总结

本文探讨了一种更加简单的多重签名以太坊合约，在此合约下，用一个交易发送所有分离签名前，会先在链下汇总这些签名。这样做简化了链上智能合约代码，方便审查，且为将来进行形式化验证提供了可能性。