Software Formal Verification Engineer
Munich, Bavaria-Bayern, Germany
Join the team delivering high-level guarantees of Apple’s most critical systems through state-of-the-art formal verification methodology! Apple’s formal verification team is looking for software verification engineers that are passionate about driving high-quality software within Apple’s kernel and security systems. Apple devices are at the center of the daily lives of over a billion customers. We rely on them to handle our private data carefully and securely. Our team delivers on this promise of quality by deriving formal guarantees about the systems that countless of users rely upon. As part of the formal verification team, you will work alongside kernel, security, and other formal experts in the field to develop formal proofs of key software systems. Dynamic, smart people and inspiring, innovative technologies are the norm here. Your work will drive quality by providing formal guarantees to ensure that customers can continue to rely upon the security of Apple products. Join our team of formal experts and make a real difference to Apple’s devices and to the state-of-the-art of software formal verification.
- Advanced working knowledge of formal logic and automated reasoning.
- Proven proficiency in developing theories using interactive theorem provers.
- Deep understanding of computer architecture.
- Experience formally modeling real-world systems.
- Proficiency in C, C++, or similar language with excellent debugging skills.
- Extraordinary teammate with excellent interpersonal and communication skills.
- Must be passionate about developing world-class/innovative formal verification solutions.
As a software formal verification engineer, you will be responsible for: - Deriving full formal proofs over Apple’s critical software systems. - Flushing out bugs and security issues within these systems before they ever hit production. - Collaborating with Apple’s world-class software teams to improve the quality of software architecture. - Clearly communicating formal specifications to non-formal engineers - Crafting novel and creative improvements that continuously improve our software formal verification methodology. - Developing and implementing re-usable and optimized formal models and verification code base
Education & Experience
Graduate degree in Electrical Engineering, Computer Science or relevant discipline is required (or B.S. plus equivalent industry experience)
- - Experience with Isabelle and AutoCorres is a plus.
- - Experience designing, verifying, or modeling cryptography or computer security systems is a plus.
- - Experience with ML or other functional programming languages is a plus.