Formal Verification Wizard
Certora provides formal verification tools and smart contract audits to secure blockchain protocols. Their flagship product, the Certora Prover, uses formal verification to mathematically prove that smart contracts are secure against vulnerabilities by checking every possible contract state and path against predefined rules. They also offer security audits conducted by a team of formal verification experts. Certora engages with the community through audit contests to crowdsource security specifications.
About Certora
Certora Prover is the most advanced Formal Verification (FV) engine for Ethereum (EVM), Solana (sBPF), and Stellar (WASM), and is now free, transparent, and community-driven. It is a powerful tool that compares smart contract bytecode against rules detailing expected code behavior. This process, known as formal verification, checks every possible contract state and path to identify critical vulnerabilities. Certora offers solutions for teams to run the tools themselves or hire their team of experts to secure the code. They also work with their community to crowdsource custom formal specifications to find vulnerabilities in code, running frequent community audit contests.
Skills
About the Role
You will prove mathematical properties of complex financial systems implemented as smart contracts. You will analyze complex code, design modular proofs, and harness SMT solvers to locate critical bugs. You will collaborate with product definition to integrate formal verification capabilities into a prover and apply software development practices to DeFi protocols.
Requirements
- Academic graduate degree in Mathematics Physics or Computer Science or outstanding undergraduate equivalent
- Passion for applying cutting-edge technology to financial systems
- Software development background
- Background in code security (advantage)
- Understanding of DeFi and Fintech (advantage)
- Formal verification experience with tools such as Dafny Lean Coq or Isabelle (advantage)
Responsibilities
- Lead adoption of formal methods for financial systems
- Prove mathematical properties of smart contracts
- Analyze complex code and design modular proofs
- Use SMT solvers to find critical bugs
- Assist product definition to integrate formal verification into a prover
Benefits
- equity compensation
- remote work option
- hybrid work option