I'd like to thank Lucas Vella, Georg Wiese and Thibaut Schaeffer for reviewing this post. We had a lot of fun last weekend hacking at EthBerlin4. Rodrigo Saramago and Moritz Hoffmann from the Solidity team joined Lucas Vella and me from powdr to hack on R55. We ended up winning the Infrastructure track and we're quite happy with what we managed to build, so I wanted to share some technical aspects of the project. This post explains how R55 works and our process for building the PoC in under 40h during the hackathon. Relevant links and stats R55: https://github.com/leonardoalt/r55, ~1000 new LoC rvemu-r55: https://github.com/lvella/rvemu, 48 LoC patch revm-r55: https://github.com/r0qs/revm, 241 LoC patch

Simplified Example field: 2**64 - 2**32 + 1 // The "@line" means that the register pc is matched with "line" in the lookup. // The "pc' = pc + 1" is the default assignment if it is not changed by an instruction. reg pc(@line): pc' = pc + 1 // If no default assignment is given, it is "A' = A" reg A[8] // default: : A' = A reg Z[8] //: Z' = Z reg B[8] //: B' = B

Ideas This is a random list of ideas that help designing the language. Most if this is heavily inspired by zkASM / PIL of the polygon/hermez team. Main goal: Everything is written in the same language, if possible not even spread across multiple files. Constant Definitions Define constants directly in the pil file: pol constant BYTE(i) { i % 0xff };

Tickets Sold-out, entry only with valid QR-code. When April 18th, 2022 Begin: 09:00 End: 17:00 Admission: 08:00 Where

Ethereum Foundation (remote) Formal Verification and Applied ZKP teams. About the role The candidate will be expected to research methods to formally verify ZK applications, potentially develop tools, and apply those to the verification of ZK programs developed by the EF Applied ZKP team. Some examples of such applications are Semaphore and other gadgets. The successful candidate will work closely with both the Formal Verification and Applied ZKP teams, but they should also be able to work independently and lead their own research. There is a lot of flexibility in the research itself, and the person should feel free to collaborate with folks outside the EF as well. We open source everything from the start. The position is remote, but they are welcome to join any of the EF offices if there is one close by. The position is permanent however the details of the contract will depend on the location and personal circumstances of the candidate. Requirements The candidate should be able to do research on Formal Verification, and be familiar with some of the topics/tools below: