Consultants to work on Aeneas verification tool

Stream: job postings

[Son Ho]

We may have fundings to hire people as independent consultants to work part time or full time on the Aeneas toolchain. Aeneas is a verification toolchain which aims at verifying programs, specifically written in Rust, at an industrial scale. It crucially leverages Lean for the proofs and is currently being used at Microsoft to verify SymCrypt (see this blog post), Microsoft's open source cryptographic library notably used in Windows and Azure Linux. One goal of the verification of SymCrypt is to develop a methodology by which a product team works hand in hand with proof engineers to verify programs as fast as they are being deployed in production.

If you are fluent in Lean, preferably (but not necessarily) with experience in meta-programming, and are interested in the project, please send me a DM!