P3-FV

This project is an experimental devtool for more easily generating formal verification specs from existing Plonky3 circuits. First you extract the symbolic constraints from your Rust circuit and then pass it through a Python transpiler to output a Z3 Python program, which you use to run the Z3 solver.

This project uses the Z3 theorem prover and Polygon's Plonky3 ZK framework. The Plonky3 framework has nice abstractions around building AIRs which was very beneficial for extracting the constraints before passing them through the Z3 transpiling pipeline in Python (for which Z3 has a far more ergonomic library than in Rust).