Verification Internships at Microsoft Azure Research

Stream: job postings

[Son Ho]

Azure Research in Cambridge (UK) is looking for PhD level interns to work on the formal verification of Rust programs. The internships will involve using and improving the Aeneas toolchain and Lean to develop a methodology which allows verifying production code at a fast pace. The potential topics include: the formal verification of cryptographic code, the development of automation in Lean to scale verification, and the development of a work in progress separation logic extension for Aeneas to reason about unsafe/concurrent code, with system verification as a first target.
If you're interested in seeing how Lean is used in the industry and are willing to contribute to scaling verification on production code which runs on billion of devices, we encourage you to apply here:
https://apply.careers.microsoft.com/careers/job/1970393556626892?domain=microsoft.com&hl=en