Formal Methods Researcher for ZK

Veridise is seeking a Formal Methods Researcher to join our team and help design and build new methodologies for verifying the security of ZK technologies.

As a ZK researcher at Veridise, you will be expected to conduct research and develop new techniques tailored to verifying the security of ZK circuits, proving systems, and ZKVMs. You would be expected to design new techniques to improve the performance and usability of Veridise’s core ZK tooling.

This role is ideal for a creative and independent thinker who can identify important security challenges and develop novel solutions.

Responsibilities

• Enhance and extend Veridise’s core ZK tooling, including Picus, ZK Vanguard, and the LLZK circuit IR.
• Develop novel methodologies to improve the usability and scalability of Veridise’s ZK tools for complex circuits.
• Design and implement generic circuit transformations, analyses, and optimizations within LLZK, along with formal verification methodologies to ensure their correctness.
• Work closely with the engineering and audit teams to integrate verification techniques into our security tooling.
• Conduct research, publish findings, and contribute to the academic and industry community on formal verification for cryptographic security.

Required Qualifications

• PhD or equivalent professional research experience in formal methods, programming languages (PL), computer security, or a related field.
• Publications in top PL, Verification, or Security conferences.
• Strong background in automated verification (e.g., SMT solvers, software model checking).
• Some experience with cryptographic security, ZK circuits, or blockchain security.
• Ability to independently identify and tackle important security challenges in ZK technologies.
• Strong communication skills, with a passion for both theoretical research and practical implementation.

Preferred Qualifications (Nice to Have)

• Experience designing formal verification infrastructure for large scale systems, languages, or security-critical systems.
• Proficiency using an interactive theorem prover such as Lean, Coq, or ACL2.
• Proficiency in C++ and Rust.
• Knowledge of ZK circuit languages, familiarity with existing formal methods for ZK.
• Familiarity with SMT solving techniques for cryptographic or security-related applications.
• Contributions to open-source projects in formal methods, theorem proving, or verification tooling.