A：是人为的熵，大家写程序的时候犯的错。本来写一个程序倒无所谓，但现在跟很多货币有关的话，是非常非常危险的，当然慢慢也会产生一些市场，自动地去堵这个风险。Formal verification 能够自动检测智能合约是不是你想描写的那样，这里面的数学是非常奇妙的，就是我刚才讲的数学逻辑。