Formal Methods Researcher for ZK
Veridise provides smart contract audits, blockchain security services, zero-knowledge audits, and in-house security tooling.
Maintainer signals as of 9/2/2026
Funding history
Projects
About Veridise
Veridise is a blockchain security company specializing in smart contract audits, zero-knowledge and zkVM audits, L1/L2 and DeFi security reviews, security proofs, architecture reviews, and security research. Its services combine manual auditing with formal methods and proprietary tools for vulnerability detection. Veridise also provides AuditHub and in-house tools including Vanguard, OrCa, ZK Vanguard, and Picus to support auditors and audit clients.
Skills
About the Role
Research and develop formal verification techniques for zero-knowledge circuits, proving systems, and ZKVMs. Design and implement circuit transformations, analyses, and optimizations within LLZK, extend core ZK tooling, integrate verification techniques with engineering and audit teams, and publish research findings on cryptographic security.
Requirements
- PhD or equivalent professional research experience in formal methods, programming languages, computer security, or a related field
- Publications in top programming languages, verification, or security conferences
- Strong background in automated verification such as SMT solvers and software model checking
- Experience with cryptographic security, zero-knowledge circuits, or blockchain security
- Ability to independently identify and tackle important security challenges in ZK technologies
- Strong communication skills and interest in both theoretical research and practical implementation
- Preferred: experience designing formal verification infrastructure for large-scale or security-critical systems
- Preferred: proficiency with interactive theorem provers such as Lean, Coq, or ACL2
- Preferred: proficiency in C++ and Rust
- Preferred: knowledge of ZK circuit languages and SMT solving techniques
- Preferred: contributions to open-source formal methods, theorem proving, or verification tooling
Responsibilities
- Enhance and extend core ZK tooling including Picus, ZK Vanguard, and the LLZK circuit IR
- Develop methodologies to improve the usability and scalability of ZK tools for complex circuits
- Design and implement generic circuit transformations, analyses, and optimizations within LLZK
- Design and implement formal verification methodologies to ensure correctness
- Integrate verification techniques with engineering and audit teams
- Conduct research and publish findings on formal verification for cryptographic security
Benefits
- Flexible work environment
- Opportunities to publish and contribute to academic and industry communities
- Competitive salary and benefits