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.
Skills Required
- PhD or equivalent professional research experience in formal methods, programming languages, computer security, or related field
- Publications in top PL, Verification, or Security conferences
- Strong background in automated verification
- Some experience with cryptographic security, ZK circuits, or blockchain security
- Ability to independently identify and tackle important security challenges
- Strong communication skills
What We Do
Veridise is an innovative blockchain security company, founded in 2021 by a team of world-class academics. The birthplace of Veridise is the UToPiA research group. Our co-founder and UT Austin professor, Isil Dillig, leads the UToPiA research group, which focuses on program analysis, verification, and synthesis—an area of Computer Science that has profound implications for software security. Veridise provides industry-leading blockchain security audits for all verticals of the Web3 ecosystem, including smart contracts, zero-knowledge circuits, blockchain implementations, and more. We have a track record of identifying critical vulnerabilities in protocols and projects that other security companies and auditors missed. So far, we’ve identified more than 100 high-severity vulnerabilities.
Why Work With Us
At Veridise, we leverage our cutting edge research in program analysis and formal methods to improve blockchain security. Perks of working for Veridise Fully remote work and flexible working hours Attending industry conferences Multiple opportunities for professional growth Industry-leading security professionals as colleagues
