Zero Knowledge

Using Formal Verification on ZK Systems with Jon Stephens

Jul 12, 2023
Ask episode
Chapters
Transcript
Episode notes
1
Introduction
00:00 • 3min
2
Veridice: A Blockchain Auditing Firm That Is Increasingly Specializing in ZK Systems
03:19 • 3min
3
Formal Verification of Solidity Code
05:54 • 2min
4
How to Use Formal Verification to Validate a Program
08:04 • 4min
5
The Flexibility of Verifiers
11:49 • 2min
6
How Verdes Got Started
13:30 • 4min
7
The Different Types of Static Analyzers
17:16 • 2min
8
The Importance of a Formal Verifier
19:06 • 2min
9
The Struggle of My Life Is Translating Based on Boogie Programs
21:30 • 2min
10
The History of the Move to Zk
23:28 • 2min
11
The Differences Between Formal and Formal Verification in Zk
25:00 • 2min
12
The Formal Verification of a Program in Circum
27:09 • 2min
13
The Problem With Over Constrained Circuits
29:06 • 3min
14
The Risks of Under Constrained Circuits
32:16 • 3min
15
The Importance of Having Additional Validation in ZK Circuits
35:22 • 2min
16
How to Check for Under-Constraintness in ZK Circuits
37:40 • 2min
17
The Importance of Formal Verification in ZK Circuits
39:25 • 3min
18
How to Run a Formal Verification Tool for ZK
41:56 • 2min
19
How to Conduct an Audit on Fixed Versions of Code
44:08 • 2min
20
How Long Does It Take to Run a Formal Verifier?
46:07 • 3min
21
CIRCOM vs. Nova: A Comparison of Proving Systems
48:52 • 2min
22
The Role of Languages in Auditing
50:38 • 4min
23
The Language of Halo 2
54:20 • 2min
24
Rust's Borrow Checker for Formal Verification
55:56 • 3min
25
ZK: A Language for Formal Verification
58:40 • 3min
26
Security in the Ecosystem
01:01:15 • 2min
27
How to Disclose a Bug in Solidity
01:03:28 • 3min
28
The Importance of Reporting Bugs
01:06:43 • 2min
29
The Counterpoint to Security Reactions
01:08:15 • 2min
30
How to Motivate a Black Hat Hacker
01:10:43 • 4min
31
ZK Systems: How Optimistic Are We?
01:14:41 • 3min
32
Verdiocese and ZK Security Disclosures
01:17:46 • 2min