Formal Verification Researcher/Engineer - Zero Knowledge Applications

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:

• Theorem provers / SMT solvers / SAT solvers in general
• Coq / Isabelle
• Model checking
• Symbolic execution
• Abstract interpretation

The results of the research are expected to be implemented for production, so they should also be able to code. This may include learning/coding in languages/frameworks that create R1CS and PLONK circuits, such as Circom, ZoKrates, Dusk PLONK, as well as developing new tooling in their preferred language.

Plus

This FV position is focused on ZK applications, therefore experience with the following is an advantage but not required:

• zkSNARKs / zkSTARKS.
• Different arithmetization schemes, especially R1CS and PLONK.

Knowledge and experience on the topics above will also be gained at runtime.

Contact

Please email [e-mail] with a CV and any additional material you may want to present/discuss.