In our previous blog post 🥷 Formal verification of an OpenVM chip, we have seen how to verify the determinism of the branch_eq chip of OpenVM. Now, we will see how to verify its completeness, meaning that it always accepts a valid witness for any possible input.
🥷 Verification of the completeness of an OpenVM chip
· 8 min read