1. 引言
主要见Daniel Luick等人2023年论文《ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge》。
程序安全性验证，通常可简化为在Satisfiability Modulo Theories (SMT)中证明某公式的unsatisfiability（即validity）：
- boolean logic ＋ 对任意first-order fragments公式化的理论。
ZKP支持，在不泄露底层共识的情况下，验证SMT公式。
本文设计的ZKSMT：
- 在ZK框架下，证明SMT公式的有效性。
- 所设计的定制虚拟机，可在ZK中表示SMT validity proof的验证流程。
- 在证明程序安全性时，在保证完备性和可靠性的同时，支持大多数主流理论。
形式化验证，为使用数学推理来证明程序正确性的流程。
形式化验证已用于验证大规模真实程序，如：
- compilers编译器
- operating systems操作系统
- Transport Layer Security (TLS)协议等。
为确认某程序具备某属性，需将该程序和属性均转换为某种数学形式，从而将程序的推理问题，reduce为，对数学对象的推理问题。