In this blog post, we present a short example about how we define reasoning rules in Rocq to formally verify the safety of zero-knowledge circuits written in LLZK.
Follow-up
This blog post is a follow-up to:
The code we are referring to in this post is available in github.com/formal-land/garden/Garden/LLZK.