Research Software Engineer
Are you applying to the internship?
Job Description
About the Company:
CertiK, founded in 2018 by professors from Yale and Columbia Universities, is a leading blockchain security company. Their mission is to secure the cyber world by applying cutting-edge academic innovations to secure blockchain code and protocols. They focus on securing blockchain protocols and smart contracts, enabling the development of secure and reliable mission-critical applications.
Job Description: Research Software Engineer
CertiK is seeking a Research Software Engineer to contribute to their mission of securing blockchain technology. The role involves designing and developing automated tools to ensure the correctness of smart contracts and identify security vulnerabilities. The position is available at various seniority levels, with responsibilities and title matching experience.
Responsibilities:
• Extend and Develop Verification Tools: Expand the capabilities of existing automated program verification tools and design and implement new tools.
• Algorithm Adaptation and Improvement: Adapt and enhance algorithms for symbolic software model checking, including techniques like bounded model checking (BMC), counterexample-guided abstraction refinement (CEGAR), and property directed reachability (IC3/PDR).
• Language Translation and Optimization: Build and improve translators that convert various input languages into intermediate representations, optimized for automated analysis.
• Security Property Identification and Formalization: Identify new classes of smart contract security properties and formalize them for use in automated verification tools.
• Collaboration and Technical Direction: Closely collaborate with other software engineers, contributing to tool development and setting technical direction for problem-solving.
• Full Software Development Lifecycle: Participate in all aspects of software development, including analysis, design, testing, operations, CI/CD, result measurement, feedback incorporation, and support.
Required Qualifications:
• Master’s Degree in Computer Science or a related field, or 5 years of equivalent experience.
• Minimum 4 years of software development experience (including internships, research projects, and open-source contributions).
• Minimum 2 years of experience with at least one of the following: model checking, formal verification, SAT/SMT solving (Z3, CVC4, Yices, MathSAT, SMTInterpol), abstract interpretation, or related fields.
• Demonstrated knowledge of fundamental computer science concepts (data structures, algorithms, mathematical logic, automata theory).
Preferred Qualifications:
• PhD in automated reasoning or a related field.
• Publications in conferences such as POPL, CAV, TACAS, FMCAD, FM.
• Experience with functional programming (OCaml or Haskell).
• Strong problem-solving skills, willingness to learn, and collaborative spirit.
• Prior professional software development experience.
