Role summary As a member of the Protocol Snarkification team, you will work towards snarkifying Ethereum by working to specify and verify the core cryptographic components of proof systems and their implementation in the Ethereum ecosystem. About the Ethereum Foundation The Ethereum Foundation (EF) is a global non-profit organization dedicated to assisting the Ethereum ecosystem in realizing the potential of Ethereum as an open, neutral infrastructure for the world. In practice, we dynamically allocate resources to critical projects when needed and step back when others can take the lead. About the team The Protocol Snarkification team's mission is to help integrate cryptographic proof systems into the core of Ethereum, with a particular focus on specifying and verifying the cryptographic protocols and their implementation. This is a research-oriented team that sits alongside other Protocols teams (particularly the Cryptography and zkEVM teams), working towards Ethereum’s snarkification, and which is intended to remain flexible to the needs of Ethereum’s development whilst improving the way that high assurance cryptography is delivered in the Ethereum ecosystem. The team currently oversees the zkEVM formal verification project, which includes the formal verification of zkVM circuits, the development of formally verified executable specifications of proof systems, and the verification of implementations against these specifications. Many aspects of this work are representative of this team’s interests; for example, formalization of cryptography in Lean and (Lean-)MLIR for cryptography. Key responsibilities Key responsibilities would include a subset of the following, depending on your specific interests and expertise. - Formalize cryptography that is used in Ethereum. This includes developing new specifications, maintaining libraries such as ArkLib , and working with external collaborators to verify optimizations and other implementation details which are used in practice. - Investigate the development and verification of MLIR dialects for cryptography and zkVMs. - Improvements to tooling and the use of AI for the above. - Assist the zkEVM Formal Verification effort . - Collaborate with other teams at the EF (e.g. Cryptography, zkEVM). - Stay at the forefront of relevant developments in cryptography, implementations, and formal verification. - Document and communicate your work, and contribute to the broader high assurance cryptography ecosystem.