Developers harness the power of the cloud to build innovative applications, websites, and businesses. Using proof-generating automated reasoning techniques, AWS enables customers to answer questions about security, availability, durability, and functional correctness. We call this provable security, absolute assurance in security of both cloud technology and of technology that uses the cloud. https://aws.amazon.com/security/provable-security/

We do proof at multiple levels of abstraction, ranging from high-level abstractions of highly distributed and concurrent protocols, covering manual and automated abstractions; software implementations in high-level implementation languages including Java and Rust; refining down to low-level implementations of x86/ARM hypervisor technology. We are looking for genuine PL-enthusiasts who appreciate the power of automated reasoning about program behavior to bring scale into software development and deliver profound impact with best-of-class tooling for the analysis of software that covers an exceptionally broad range of applications that are really fun!