Microsoft internship on verification / crypto with Lean

Stream: job postings

[Jonathan Protzenko]

https://jobs.careers.microsoft.com/global/en/job/1782720/Internship-Opportunities--Azure-Research

Microsoft Azure Research is hiring for internships next summer. This is an opportunity to work on Aeneas, either on the theoretical side (how to verify Rust programs with Lean), or on the applicative side (verifying cryptographic algorithms such as AES-GCM, Kyber, whose proofs involve reasoning about the underlying mathematical structures such GCM, Ring Learning With Errors). So, either PL-focused on math-focused :-).

If you apply, please also email protz@microsoft.com to let me know about your application. Thanks!