Spark Program | CKB-VM Sail Formal Verification — Proving CKB-VM RISC-V Instruction Equivalence via Sail Specification and Coq Theorem Prover / CKB-VM Sail 形式化验证 — 基于 Sail 规范与 Coq 定理证明器的 CKB-VM RISC-V 指令等价性证明

[Ckroamer]

形式化验证这个方向很有意思，但感觉可能存在不小的技术障碍，而且项目在交付后的实际可用性是否能得到充分保证也值得进一步探讨，不过始终都值得一试。