VeriMan：用于Solidity智能合约的分析工具。 原型

威瑞曼 用于Solidity智能合约的分析工具。 原型。 使用VeriMan，您可以使用合同的变量以及Solidity的数字和布尔运算来定义时间属性。 然后，该工具对合同进行检测，以找到伪造至少一个属性或证明其持有的痕迹。 然后，您可以对照任何试图使断言失败的工具（例如Mythril）或也试图证明其成立的任何工具来检查已执行的合同。 例如，给定以下合同： contract Example { bool public a_called = false ; bool public b_called = false ; bool public c_called = false ; int public num_calls = 0 ; function a () public { a_called = true ; num_calls ++ ; } function b () public { require (a_called); b_called