Leo

ethereum_formal_verification_overview. Overview of the formal verification projects in the Ethereum ecosystem.

yools. Tools for Yul.

fusion. An experimental progressive and fast zkRollup written in Rust, focused on performance, modularity, and applying cutting-edge Verifiable Computation proof systems.

dl_symb_exec_sol. Symbolic execution engine written in Solidity, based on Difference Logic.

tinyzkevm. Python

sol-macros. Solidity

sol_generic_vector. Generic Vector library for Solidity

powdr-brainfuck. ZK proofs for Brainfuck execution using powdr

SolPrologV2. A Prolog engine written in Solidity.

evm. Simple EVM implementation in [no_std] Rust to be used in Powdr.

hevm_paper. TeX

pinballctf. Solidity

cav_2022_artifact. Solidity

text. Papers, talks, presentations

zokrates_nova. Examples of Nova recursive proofs for ZoKrates programs.

usc2022. My submission to Underhanded Solidity Contest 2022

baby_its_me. Solidity

chc_benchmarks_solidity. SMT

yultsur. Yultsur is a Rust implementation of Yul.

Nova. Nova: Recursive SNARKs without trusted setup

merkle-tree-powdr. Rust

swap.socks.sol. Swap socks.sol

problem_solving. Programming contests solutions

any-zkvm. A rust template that allows any rust dev to easily develop an app made for a zkVM, but abstracting which one to use

powdr-recursion-test. Rust

rust-smt-ir. SMT

seaport. Seaport is a marketplace protocol for safely and efficiently buying and selling NFTs.

InfiniTime. Firmware for Pinetime smartwatch written in C++ and based on FreeRTOS

bellperson. zk-SNARK library