Microsoft US Internship on math/crypto program verification

Stream: job postings

[Jonathan Protzenko]

This is a new internship posting, in the US this time. https://jobs.careers.microsoft.com/global/en/job/1791134/Research-Intern---Cryptography

Our ambition is to perform proofs of functional correctness for cryptography in Lean. There are two possible directions to this work:

• scaling up program verification using Lean by improving tactics, models and reasoning facilities -- this is the more language-oriented version of the internship
• using Lean to perform concrete program verification on real-world cryptographic implementations, e.g., proofs of functional correctness to show that this particular Montgomery or Barrett reduction in the implementation of ML-KEM is correct given range hypotheses for the inputs -- this is the more math-oriented version of the internship.

Concretely, the implementations will be written in the Rust programming language, and translated to Lean via the Aeneas toolchain for verification.

Both of these aspects would be an excellent fit for a proficient Lean user, either more on the PL side, or on the math-user side.

The internship is in the US, and Microsoft provides relocation assistance and visa support for international candidates. Any candidate must be currently enrolled in a PhD program.

[Jonathan Protzenko]

Oh and I forgot to mention: as with the previous job posting, please send me an email at protz@microsoft.com to notify me if you apply. Thanks!