以太坊EVM形式化验证

RecodeX 重构消息，以太坊基金会提出，机构在依据链上数据采取行动前应先完成核验，并将责任归属置于机构核查流程的核心位置。基金会另一项名为evm.fast的挑战项目则聚焦于验证者的执行证明。

RecodeX 重构消息，以太坊区块验证项目evm.fast的公开任务基准分截至3日仍为无穷大（∞），公开排行榜上尚无提交因给出有限上限而获得晋升。该任务要求计算固定Pancake EVM程序在64位RISC-V Flapjack模型上运行所需的步数上限K，程序初始启动步数也计入其中，适用输入为声明gas上限不超过2亿的情况，且程序须放入128MiB程序窗口。参与者需提交能产生对应结果的RISC-V字节码及Lean证明，仅通过执行测试并不满足提交要求。