鲸鱼观察：Robinhood 首席执行官 Vlad Tenev 表示，所有代码将在两年内完成形式化验证。 这是一个雄心勃勃的说法。形式化验证适用于关键系统和航空航天加密协议，但要将其扩展到 Robinhood 这样规模的整个代码库，将是一项前所未有的工程壮举。如果他真的做到了，这将改变整个行业对软件可靠性的看法。 两年时间对于这项豪赌来说太短了。