一种基于定理证明器的EVM实现层语义描述方法和装置

本申请涉及区块链技术领域，提出一种基于定理证明器的EVM实现层语义描述方法、装置、电子设备和计算机程序产品。该方法包括：获取待处理的EVM执行引擎代码；根据预定义的各种EVM指令的数据结构和指令行为，且基于定理证明器将EVM执行引擎代码的每条EVM指令的执行逻辑分别转换为对应的实现层语义描述。该方法根据定义好的各种EVM指令的数据结构和指令行为，在高可信度的定理证明器中对EVM执行引擎代码的实现层进行高保真的形式化建模，从而能够获得高准确度的实现层语义描述。