Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect unused gates, unconstrained cells, and unused columns. Using an SMT solver, we can detect under-constrained circuits (in the sense that for the same public input they have two efficiently computable satisfying assignments). This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.
Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using SAT and SMT solvers more than one billion times a day, both for “real-time” queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Supporting reasoning at this scale and volume requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will describe some lessons learned and offer some directions for the community that should allow us to scale further, increase trust, and solve the next billion queries a day.
Dolmen provides tools to parse, type, and validate input files used in automated deduction, and in particular problems from the SMT-LIB . We present here an extension of Dolmen which makes it capable of verifying ground models for quantifier-free SMT-LIB problems. While most of the extension was a straightforward implementation of an evaluator for ground expressions, there were some challenges, related to corner cases of the semantics (division by zero, partial functions, ...), as well as order of evaluation of statements, most of which could be solved by improvements to the SMT-LIB standard for models.
