Email Gateway (May 04 2026 at 11:22): Email Gateway (May 04 2026 at 11:22):From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
The Automated Reasoning Group at AWS in Cambridge is seeking internship candidates to work on formal verification of low-level systems software. Among other things, the hosting team is responsible for the formal verification of the Nitro Isolation Engine, a new separation kernel for Graviton cloud instances. The ideal candidate is a student towards the end of their PhD with a strong background in interactive theorem proving, ideally but not necessarily Isabelle, and some familiarity with systems programming, ideally in Rust. Details are TBD, but potential topics include hands-on proof development, refining our large-scale separation logic proof automation, or improving AI / ITP integration.
If you are interested, please reach out to me directly.
Kind regards,
Hanno
Last updated: May 23 2026 at 03:31 UTC