Zero Knowledge cover image

Using Formal Verification on ZK Systems with Jon Stephens

Zero Knowledge

00:00

The Flexibility of Verifiers

It depends on how you perform formal verification and exactly how much you kind of constrain the problem. The verifier that I created was actually very flexible in that it used a specification class called temporal specifications which basically state properties over time. And because we were using this very I guess flexible but particular specification language it was able to find attacks that required a series of transactions or that even would require fallback functions to be synthesized. It's always gotten this impression that it was a very precise testing tool but a very limited one. This is sort of surprising that it sort of can find things past what it's been specked for.

Transcript
Play full episode

The AI-powered Podcast Player

Save insights by tapping your headphones, chat with episodes, discover the best highlights - and more!
App store bannerPlay store banner
Get the app