zkEVM Bootcamp

Formal Verification Today’s topic was about verifying the correctness of a proving system or a circuit with formal verification. This technique is increasingly popular and has stronger guarantees than static analysis or fuzzing. Projects and tools: Veridise is a company that maintains different security tools. Picus is one of them. It implements the &QED^2&, which checks the uniqueness property (under-constrained signals) of ZKP circuits. Aleo Vanguard, another tool by Veridise for Leo/Aleo programs....

Presentation by Iryna from RISC Zero RISC Zero is a zkVM system that can run general-purpose verifiable code. As any VM, it has a set of instructions: 32-bit RISC-V, an open standard instruction set architecture (ISA) based on established reduced instruction set computer (RISC) principles. For the zk part, it utilizes STARK. Read more in the official documentation. Two main parts from the developer’s perspective are: Host code, which the Prover or the Verifier will use....

Presentation by Ye from Scroll Scroll is one of the most popular zk-rollups on Ethereum. The team targets bytecode equivalence with EVM, which differs from, for example, zkSync because the latter has equivalence only on the language level and then compiles it to a different set of bytecode operations. The next level would be the consensus equivalence. From the developer’s perspective, Scroll is the same as EVM. You can use all the tooling (Foundry, ethers....