Social
Automated reasoning

Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine

Isabelle/HOL's balance of expressiveness, automation, and scalability enabled the world's first formally verified cloud hypervisor.

By Larry Paulson
April 17, 2026
6 min read
Share
Key takeaways
  • Isabelle/HOL is a proof assistant used to formally verify the correctness and security of the Nitro Isolation Engine (NIE), the first formally verified cloud hypervisor, which provides resources to AWS clients while ensuring the security of customer data.
  • It balances expressiveness, automation, proof readability, and scalability, making it suitable for formal verification tasks.
  • Isabelle/HOL supports higher-order logic, allowing for the expression of complex mathematical statements and the verification of critical software.
  • It has been used in various projects, including the verification of the seL4 microkernel, WebAssembly semantics, and cryptographic protocols.
Was this answer helpful?

At Amazon’s 2025 re:Invent conference, Amazon Web Services (AWS) announced the Nitro Isolation Engine (NIE), a software module tasked with providing resources to AWS clients while ensuring the security of customer data. AWS also announced the formal verification of the isolation engine’s correctness and security guarantees, using a proof assistant called Isabelle/HOL. As the first formally verified cloud hypervisor, NIE sets a new standard for cloud security.

isabelle.png
Isabelle was originally developed at the University of Cambridge and Technische Universität München and includes numerous contributions from institutions and individuals worldwide.

A proof assistant is an automated tool that can help human users develop formal proofs — of mathematical theorems, the validity of hardware or software systems, or anything in-between. Several proof assistants are in common use, and we chose Isabelle/HOL because it struck the right balance among expressiveness, automation, proof readability, and scalability. So what do I mean by that?

Logical reasoning by computer

There is no fixed language of mathematics, but we can create languages for expressing mathematical reasoning, just as programming languages express computational tasks. And just as programming languages involve trade-offs between expressiveness and performance, mathematical languages involve trade-offs between expressiveness and ease of automation. Automation is vital because the construction of a formal proof is both time consuming and extremely tedious, analogous to constructing a ship in a bottle.

IsabelleHOL-01-16x9.png
Building a formal proof is like constructing a ship in a bottle: every piece must be assembled precisely within strict logical constraints. Isabelle/HOL provides the tools to make that painstaking process possible.

The most elementary mathematical language is Boolean logic, the world of the binary operators AND, OR, and NOT. Because this language is so simple, powerful automatic solvers exist for it. In 2016, Carnegie Mellon professor Marijn Heule — now an Amazon Scholar — and his colleagues encoded into Boolean logic an unsolved mathematical question, the Boolean Pythagorean Triples Problem, and used automatic solvers to help create the largest proof ever, 200 terabytes long.

A richer mathematical language called first-order logic allows us to talk about some domain of interest — the integers, say — and to define functions over that domain. And we can go beyond Boolean logic by including the quantifiers "for all" and "there exists" in assertions. In this sort of language, we can express statements such as "every prime number greater than two is odd". We can also prove the following theorem, due to Lewis Carroll: No ducks waltz; no officers ever decline to waltz; all my poultry are ducks. Hence, none of my poultry are officers.

However, most people prefer a still stronger mathematical language, where they can define types, as they do in programming. In higher-order logic, there are even function types, as found in functional programming languages such as Haskell. Higher-order logic is much richer than first-order logic, able to express statements such as Every set containing the number 1 and closed under addition contains all the positive integers. It appears to be rich enough to express most of mathematics.

The richest mathematical languages — called dependent-type theories — even allow types to take arbitrary values as parameters, e.g., T(i), where i is an integer. The best-known such languages are Lean and Rocq.

Powerful automatic theorem provers exist for first-order logic, but for higher-order logic and beyond, full automation is not available. This is the price of expressiveness. A proof assistant allows users to build proofs interactively, supported by partial automation and the possibility of coding their own proof searches. A proof assistant enforces strict compliance with the laws of logic, typically through a kernel architecture that gives only a limited portion of the code the right to create a theorem.

A proof assistant also supports the interactive development of a possibly huge formal-specification hierarchy. For example, verification of the Nitro Isolation Engine (NIE) rests on specifications of the architecture of the Graviton-5 processor, the Rust code of the hypercalls and their functional correctness, and the security properties that are to be proved. These take up much of the quarter of a million lines constituting the formal proof.

Higher-order logic is supported by HOL and HOL Light, two closely related proof assistants, and has been used to verify hardware designs, floating-point algorithms, and pure mathematics since the 1990s. AWS senior principal applied scientist John Harrison developed HOL Light, and he has used it to improve the performance of digital signatures on Amazon’s Graviton2 chip by up to 94%, by verifying an optimized version of the cryptographic algorithms. The code was delicate, and exhaustive testing is not feasible; only a formal verification of full functional correctness would do before the deployment of such critical software. But today we are interested in Isabelle/HOL.

Overview of Isabelle/HOL

The most visible difference between Isabelle/HOL and the other HOL systems — which are all based on higher-order logic — is its specification and proof language. With most proof assistants, users state what they want to prove, followed by lists of commands that replace the original goals with series of subgoals in a kind of whack-a-mole game. In Isabelle and to some extent Lean, the proof language allows desired intermediate goals to be written out explicitly, allowing a better controlled proof process and a more legible proof document. There are plenty of examples online.

Other notable features are as follows:

  • a user-configurable parser, which allowed us to embed a significant fragment of the Rust language into our specifications;
  • type classes for principled overloading, so that say + can be given its natural meaning, not just for a variety of numeric types but for machine words and in other appropriate contexts;
  • locales, a lightweight module system allowing a hierarchy of specifications to be defined and interpreted in various ways, even within a proof;
  • powerful built-in automation through simplification and backchaining proof search;
  • sledgehammer: one-click access to even more powerful external automation;
  • counterexample-finding tools, for identifying claims that are actually false;
  • code generation from executable higher-order specifications, which we used to test conformance.

For the verification of NIE, we began by implementing a specialized language called separation logic on top of Isabelle/HOL. Separation logic is designed for verifying program code operating on shared resources. We coded our own proof automation and also used what was built in. We therefore could use separation logic but also plain higher-order logic when we wanted to. Isabelle turned out to be resilient enough and efficient enough to cope with the truly gigantic subgoals. It could run that quarter-million-line proof in half an hour using an off-the-shelf laptop.

Some applications of Isabelle/HOL

The single most impressive application of Isabelle prior to NIE is probably the verification of seL4, a widely used microkernel. This proof was also about a quarter of a million lines when first announced, although it is now much longer. The seL4 developers proved that the microkernel’s C implementation refined the abstract specification, yielding full functional correctness of the core operations. And they have observed no bugs in the verified parts of the code, although testing still plays a role in covering unverified parts and certain assumptions that cannot be formalized.

Isabelle was also used in the following projects:

Isabelle is free, open source, and available to download. It runs on all the main operating systems on any machine that has enough memory.

Research areas
Tags
About the Author
Larry Paulson
Larry Paulson is an emeritus professor of computational logic at the University of Cambridge and an Amazon Scholar.

Related content

Work with us

See more jobs See more jobs
Applied Scientist, Neuron ARG, Annapurna ML
US, WA, Seattle
The Automated Reasoning Group in the Amazon Neuron team is looking for an Applied Scientist to work on the intersection of Artificial Intelligence and program analysis to raise the code quality bar in our state-of-the-art deep learning compiler stack. This stack is designed to optimize application models across diverse domains, including Large Language and Vision, originating from leading frameworks such as PyTorch and JAX. Your role will involve working closely with our custom-built Machine Learning accelerator, Trainium, which represents the forefront of innovation for advanced ML capabilities, and is the underpinning of Generative AI. In this role as an Applied Scientist, you'll be instrumental in designing, developing, and deploying analyzers for ML compiler stages and compiler IRs. You will architect and implement business-critical tooling, publish research, and mentor a brilliant team of experienced scientists and engineers. You will need to be technically capable, credible, and curious in your own right as a trusted AWS Neuron engineer, innovating on behalf of our customers. Your responsibilities will involve tackling crucial challenges alongside a talented engineering team, contributing to leading-edge design and research in compiler technology and deep-learning systems software. Strong experience in programming languages, compilers, program analyzers, theorem provers, and program synthesis engines will be a benefit in this role. A background in machine learning and AI accelerators is preferred but not required.
Member of Technical Staff, Frontier AI & Robotics (FAR)
US, CA, San Francisco
Join the next revolution in robotics at Amazon's Frontier AI & Robotics team, where you'll work alongside world-renowned AI pioneers to push the boundaries of what's possible in robotic intelligence. As a Member of Technical Staff, you'll be at the forefront of developing breakthrough foundation models that enable robots to perceive, understand, and interact with the world in unprecedented ways. You'll drive independent research initiatives in areas such as perception, manipulation, science understanding, locomotion, manipulation, sim2real transfer, multi-modal foundation models and multi-task robot learning, designing novel frameworks that bridge the gap between state-of-the-art research and real-world deployment at Amazon scale. In this role, you'll balance innovative technical exploration with practical implementation, collaborating with platform teams to ensure your models and algorithms perform robustly in dynamic real-world environments. You'll have access to Amazon's vast computational resources, enabling you to tackle ambitious problems in areas like very large multi-modal robotic foundation models and efficient, promptable model architectures that can scale across diverse robotic applications. Key job responsibilities - Drive independent research initiatives across the robotics stack, including robotics foundation models, focusing on breakthrough approaches in perception, and manipulation, for example open-vocabulary panoptic scene understanding, scaling up multi-modal LLMs, sim2real/real2sim techniques, end-to-end vision-language-action models, efficient model inference, video tokenization - Design and implement novel deep learning architectures that push the boundaries of what robots can understand and accomplish - Lead full-stack robotics projects from conceptualization through deployment, taking a system-level approach that integrates hardware considerations with algorithmic development, ensuring robust performance in production environments - Collaborate with platform and hardware teams to ensure seamless integration across the entire robotics stack, optimizing and scaling models for real-world applications - Contribute to the team's technical strategy and help shape our approach to next-generation robotics challenges A day in the life - Design and implement novel foundation model architectures and innovative systems and algorithms, leveraging our extensive infrastructure to prototype and evaluate at scale - Collaborate with our world-class research team to solve complex technical challenges - Lead technical initiatives from conception to deployment, working closely with robotics engineers to integrate your solutions into production systems - Participate in technical discussions and brainstorming sessions with team leaders and fellow scientists - Leverage our massive compute cluster and extensive robotics infrastructure to rapidly prototype and validate new ideas - Transform theoretical insights into practical solutions that can handle the complexities of real-world robotics applications About the team At Frontier AI & Robotics, we're not just advancing robotics – we're reimagining it from the ground up. Our team is building the future of intelligent robotics through innovative foundation models and end-to-end learned systems. We tackle some of the most challenging problems in AI and robotics, from developing sophisticated perception systems to creating adaptive manipulation strategies that work in complex, real-world scenarios. What sets us apart is our unique combination of ambitious research vision and practical impact. We leverage Amazon's massive computational infrastructure and rich real-world datasets to train and deploy state-of-the-art foundation models. Our work spans the full spectrum of robotics intelligence – from multimodal perception using images, videos, and sensor data, to sophisticated manipulation strategies that can handle diverse real-world scenarios. We're building systems that don't just work in the lab, but scale to meet the demands of Amazon's global operations. Join us if you're excited about pushing the boundaries of what's possible in robotics, working with world-class researchers, and seeing your innovations deployed at unprecedented scale.
Member of Technical Staff, Frontier AI & Robotics (FAR)
US, CA, San Francisco
Join the next revolution in robotics at Amazon's Frontier AI & Robotics team, where you'll work alongside world-renowned AI pioneers to push the boundaries of what's possible in robotic intelligence. As a Member of Technical Staff, you'll be at the forefront of developing breakthrough foundation models that enable robots to perceive, understand, and interact with the world in unprecedented ways. You'll drive independent research initiatives in areas such as perception, manipulation, science understanding, locomotion, manipulation, sim2real transfer, multi-modal foundation models and multi-task robot learning, designing novel frameworks that bridge the gap between state-of-the-art research and real-world deployment at Amazon scale. In this role, you'll balance innovative technical exploration with practical implementation, collaborating with platform teams to ensure your models and algorithms perform robustly in dynamic real-world environments. You'll have access to Amazon's vast computational resources, enabling you to tackle ambitious problems in areas like very large multi-modal robotic foundation models and efficient, promptable model architectures that can scale across diverse robotic applications. Key job responsibilities - Drive independent research initiatives across the robotics stack, including robotics foundation models, focusing on breakthrough approaches in perception, and manipulation, for example open-vocabulary panoptic scene understanding, scaling up multi-modal LLMs, sim2real/real2sim techniques, end-to-end vision-language-action models, efficient model inference, video tokenization - Design and implement novel deep learning architectures that push the boundaries of what robots can understand and accomplish - Lead full-stack robotics projects from conceptualization through deployment, taking a system-level approach that integrates hardware considerations with algorithmic development, ensuring robust performance in production environments - Collaborate with platform and hardware teams to ensure seamless integration across the entire robotics stack, optimizing and scaling models for real-world applications - Contribute to the team's technical strategy and help shape our approach to next-generation robotics challenges A day in the life - Design and implement novel foundation model architectures and innovative systems and algorithms, leveraging our extensive infrastructure to prototype and evaluate at scale - Collaborate with our world-class research team to solve complex technical challenges - Lead technical initiatives from conception to deployment, working closely with robotics engineers to integrate your solutions into production systems - Participate in technical discussions and brainstorming sessions with team leaders and fellow scientists - Leverage our massive compute cluster and extensive robotics infrastructure to rapidly prototype and validate new ideas - Transform theoretical insights into practical solutions that can handle the complexities of real-world robotics applications About the team At Frontier AI & Robotics, we're not just advancing robotics – we're reimagining it from the ground up. Our team is building the future of intelligent robotics through innovative foundation models and end-to-end learned systems. We tackle some of the most challenging problems in AI and robotics, from developing sophisticated perception systems to creating adaptive manipulation strategies that work in complex, real-world scenarios. What sets us apart is our unique combination of ambitious research vision and practical impact. We leverage Amazon's massive computational infrastructure and rich real-world datasets to train and deploy state-of-the-art foundation models. Our work spans the full spectrum of robotics intelligence – from multimodal perception using images, videos, and sensor data, to sophisticated manipulation strategies that can handle diverse real-world scenarios. We're building systems that don't just work in the lab, but scale to meet the demands of Amazon's global operations. Join us if you're excited about pushing the boundaries of what's possible in robotics, working with world-class researchers, and seeing your innovations deployed at unprecedented scale.
Applied Scientist II, Computational Modeling, OMHS SCS
US, MA, Boston
Are you excited about applying machine learning and applied mathematics to real-world systems at massive scale? As an Applied Scientist on this newly formed team, you will collaborate closely with scientists and engineers to bring research into production across a broad portfolio of problems — from computer vision perception platforms to building-wide optimization and orchestration. You will frame ambiguous business problems as tractable scientific challenges and implement novel machine learning (ML) systems, first-principles models, embedded systems prototypes, and performance optimizations in both prototype and production environments. This is a ground-floor opportunity to shape the scientific direction of a new organization, where your contributions will directly influence how Amazon's fulfillment network operates and evolves. Key job responsibilities - Design, develop, and deploy ML and scientific solutions spanning classical machine learning, statistical modeling, computer vision, optimization, and physics-informed modeling in production environments. - Rapidly ramp on unfamiliar problem domains, frame ambiguous business problems as tractable scientific challenges, and prototype solutions end to end. - Author or co-author research findings for internal or external peer-reviewed venues, and provide peer feedback on research procedures and results across teams. - Prototype and evaluate sensing hardware and lightweight, edge-deployable models that run on commodity compute under real-world constraints. - Collaborate across multiple science and engineering teams to integrate your solutions into deployment architecture, mentoring less experienced scientists along the way. A day in the life You might start your morning reviewing experiment results from an overnight model training run, then shift into a design discussion with engineers on how to deploy a new computer vision model to edge hardware in a fulfillment center. After lunch, you could be prototyping a physics-informed optimization approach, writing up findings for a research paper, or pairing with a teammate to debug a tricky data pipeline. As part of a new and growing organization, you will have a direct hand in shaping team practices, scientific roadmaps, and the tools you use every day. About the team Our team sits within Amazon's fulfillment technology organization and applies a range of scientific disciplines — including computer vision, optimization, reinforcement learning, and statistical modeling — to improve how goods move through Amazon's global fulfillment network. We build the models and systems that drive real-time orchestration, optimizing throughput, flow, and operational performance at scale. As a newly formed organization, we are building our culture and scientific agenda from the ground up. You will join a collaborative, inclusive group of scientists and engineers who value experimentation, rigorous research, and delivering measurable impact for customers.
Applied Scientist II, SSG Science
IN, KA, Bengaluru
Amazon Devices is an inventive research and development company that designs and engineer high-profile devices like the Kindle family of products, Fire Tablets, Fire TV, Health Wellness, Amazon Echo & Astro products. This is an exciting opportunity to join Amazon in developing state-of-the-art techniques that bring Gen AI on edge for our consumer products. We are looking for exceptional scientists to join our Applied Science team and help develop the next generation of edge models, and optimize them while doing co-designed with custom ML HW based on a revolutionary architecture. Work hard. Have Fun. Make History. Key job responsibilities What will you do? - Quantize, prune, distill, finetune Gen AI models to optimize for edge platforms - Fundamentally understand Amazon’s underlying Neural Edge Engine to invent optimization techniques - Analyze deep learning workloads and provide guidance to map them to Amazon’s Neural Edge Engine - Use first principles of Information Theory, Scientific Computing, Deep Learning Theory, Non Equilibrium Thermodynamics - Train custom Gen AI models that beat SOTA and paves path for developing production models - Collaborate closely with compiler engineers, fellow Applied Scientists, Hardware Architects and product teams to build the best ML-centric solutions for our devices - Publish in open source and present on Amazon's behalf at key ML conferences - NeurIPS, ICLR, MLSys.
Data Scientist, AI Program, CNGS NBS (New Business & New Seller) Amazon Business
CN, 31, Shanghai
Team & Project Overview The NBS Data Central team powers analytics, data science, and AI capabilities for Worldwide Global Selling (WWGS). We build scalable data products, and insight-generation systems that drive seller growth across 10+ marketplaces. Seller Intelligence is a P0 foundation theme at the Global Selling level, formed by merging "One Tagging" and "Good Contact" workstreams. It provides seller identity, segmentation, and contact-reach infrastructure that underpins all downstream seller-facing AI workflows — including intelligent outreach, personalized recommendations, and automated engagement. Scope of Impact Own the science pillar for Seller Intelligence within a cross-functional POD (PM + DE + DS + SDE) Directly impact seller engagement metrics across CN, IN, LATAM, and East-Asia expansion regions Models and data products consumed by 5+ downstream teams (ESM, NSR, MKT, NBS AI Ops, ROC) Influence $100M+ annual seller GMS through improved segmentation and contact optimization Key job responsibilities Design and deliver seller segmentation and propensity models at scale — incorporating GMS, category, growth trajectory, engagement signals, and lifecycle stage. Build contact quality scoring and lifecycle management systems (coverage optimization, dormancy detection, reactivation modeling). Define success metrics, experimentation frameworks (A/B, causal inference), and measurement methodology for seller engagement interventions. Productionize ML models and data products — partner with engineering to deploy seller scores, contact quality indices, and recommendation signals. Explore LLM/GenAI applications: automated insight generation from seller data, contact intent classification, and intelligent report synthesis. Serve as the science representative in bi-weekly NBS theme reviews; present findings and proposals to theme Bar Raisers and leadership. Collaborate with BIE team members to democratize analytical outputs via dashboards and self-serve tools. Contribute to cross-marketplace seller behavior analysis supporting Global Expansion strategy (IN, KR, VN, LATAM). Evaluate, integrate, and iterate on AI systems — assess new AI/ML tools, frameworks, and third-party models for applicability to seller intelligence use cases.
Applied Scientist, Prime Video Commerce Insights
GB, London
Come build the future of entertainment with us. Are you interested in shaping the future of movies and television? Do you want to define the next generation of how and what Amazon customers are watching? Prime Video is a premium streaming service that offers customers a vast collection of TV shows and movies — all with the ease of finding what they love to watch in one place. We offer customers thousands of popular movies and TV shows from Originals and Exclusive content to exciting live sports events. We also offer our members the opportunity to subscribe to add-on channels which they can cancel at anytime and to rent or buy new release movies and TV box sets on the Prime Video Store. Prime Video is a fast-paced, growth business — available in over 240 countries and territories worldwide. The team works in a dynamic environment where innovating on behalf of our customers is at the heart of everything we do. If this sounds exciting to you, please read on. Prime Video Commerce's mission is to present the right offer to the right customer at the right time — across subscriptions, channels, and transactional video, in every market and on every device. Our science team replaces static business rules with ML-driven decisions that personalise the entire commerce journey, from discovery through checkout and beyond. We operate at scale across hundreds of millions of customers, and we are expanding into new frontiers — combining the latest advances in agentic and generative AI, behavioural simulation, and causal inference to understand the impact of our decisions before they reach customers. We are looking for an Applied Scientist to join the Prime Video Commerce Insights team in London. You will develop and deploy customer-facing models, understand customer behaviour at scale, and explore emerging techniques that help us make better decisions faster. This is a delivery focused role within a high-visibility multidisciplinary group of engineers and scientists, focused on improving the customer experience for Prime Video. Key job responsibilities - Research, design, and implement machine learning approaches (e.g. reinforcement learning and recommendation systems) that personalise across different customer touch points. - Collaborate with engineers to deploy and integrate successful experiment results into large-scale, complex Amazon production systems with low latency. - Design and execute rigorous experiments to demonstrate the technical efficacy and business value of your methods. - Act as a subject-matter expert and help define the science roadmap and research agenda in line with organisational priorities and production constraints. - Provide machine learning thought leadership to technical and business leaders, thinking strategically about business, product, and technical challenges. - Work with technical product managers to work backwards from what matters to customers and deliver ML-backed solutions. - Share results with the team and wider scientific community through documents that are both statistically rigorous and compellingly relevant. A day in the life You will be a research leader and innovator within the Commerce Insights organisation. You will collaborate with talented engineers and senior leaders to solve problems that are uniquely challenging at Amazon's scale: personalising commerce decisions across multiple business lines, balancing competing objectives, and positively impacting hundreds of millions of customers worldwide. The problems here are technically deep — combining large-scale ML, causal reasoning, and behavioural modelling in a domain where every decision carries real revenue and customer-experience consequences. Your research will ship to production and move metrics that matter. About the team You will join a team of engineers and applied scientists with a proven track record of solving highly complex, ambiguous problems — work that has produced patents and publications at top-tier conferences. The team has direct visibility to senior Prime Video leadership and collaborates broadly across Commerce, Content, and Platform teams to shape how customers discover, subscribe to, and engage with video content. This is a team that operates at the intersection of rigorous research and real-world impact, where your ideas move from whiteboard to production for hundreds of millions of customers.
Sr. Applied Scientist, SSG Science
IN, KA, Bengaluru
Amazon Devices is an inventive research and development company that designs and engineer high-profile devices like the Kindle family of products, Fire Tablets, Fire TV, Health Wellness, Amazon Echo & Astro products. This is an exciting opportunity to join Amazon in developing state-of-the-art techniques that bring Gen AI on edge for our consumer products. We are looking for exceptional scientists to join our Applied Science team and help develop the next generation of edge models, and optimize them while doing co-designed with custom ML HW based on a revolutionary architecture. Work hard. Have Fun. Make History. Key job responsibilities What will you do? - Quantize, prune, distill, finetune Gen AI models to optimize for edge platforms - Fundamentally understand Amazon’s underlying Neural Edge Engine to invent optimization techniques - Analyze deep learning workloads and provide guidance to map them to Amazon’s Neural Edge Engine - Use first principles of Information Theory, Scientific Computing, Deep Learning Theory, Non Equilibrium Thermodynamics - Train custom Gen AI models that beat SOTA and paves path for developing production models - Collaborate closely with compiler engineers, fellow Applied Scientists, Hardware Architects and product teams to build the best ML-centric solutions for our devices - Publish in open source and present on Amazon's behalf at key ML conferences - NeurIPS, ICLR, MLSys.
Applied Scientist, SSG Science
IN, KA, Bengaluru
Amazon Devices is an inventive research and development company that designs and engineer high-profile devices like the Kindle family of products, Fire Tablets, Fire TV, Health Wellness, Amazon Echo & Astro products. This is an exciting opportunity to join Amazon in developing state-of-the-art techniques that bring Gen AI on edge for our consumer products. We are looking for exceptional scientists to join our Applied Science team and help develop the next generation of edge models, and optimize them while doing co-designed with custom ML HW based on a revolutionary architecture. Work hard. Have Fun. Make History. Key job responsibilities What will you do? - Quantize, prune, distill, finetune Gen AI models to optimize for edge platforms - Fundamentally understand Amazon’s underlying Neural Edge Engine to invent optimization techniques - Analyze deep learning workloads and provide guidance to map them to Amazon’s Neural Edge Engine - Use first principles of Information Theory, Scientific Computing, Deep Learning Theory, Non Equilibrium Thermodynamics - Train custom Gen AI models that beat SOTA and paves path for developing production models - Collaborate closely with compiler engineers, fellow Applied Scientists, Hardware Architects and product teams to build the best ML-centric solutions for our devices - Publish in open source and present on Amazon's behalf at key ML conferences - NeurIPS, ICLR, MLSys.
Research Software Engineer, Calibration, MQS Center for Quantum Computing
US, CA, San Francisco
The Models, Quantum, and Silicon (MQS) Center for Quantum Computing (CQC) is a multi-disciplinary team of scientists, engineers, and technicians, on a mission to develop a fault-tolerant quantum computer. We are looking to hire a Research Software Engineer to join our growing Software team. You will work closely with our experimental physics teams to enable their work characterizing, calibrating, and operating novel quantum devices. The ideal candidate should be able to translate high-level science requirements into software implementations (e.g. Python APIs/frameworks, data analysis pipelines, calibration nodes) that are performant, scalable, and intuitive. This requires someone who (1) has a strong desire to work within a team of scientists and engineers, and (2) demonstrates ownership in initiating and driving projects to completion. This role has a particular emphasis on working directly with experimental physicists to develop scientific software workflows that enable scaling to larger quantum devices. Inclusive Team Culture Here at Amazon, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon conferences, inspire us to never stop embracing our uniqueness. Diverse Experiences Amazon values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. Export Control Requirement Due to applicable export control laws and regulations, candidates must be either a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum, or be able to obtain a US export license. If you are unsure if you meet these requirements, please apply and Amazon will review your application for eligibility. Key job responsibilities - Architect extensible & intuitive frameworks for running quantum computing experiments and analyzing data. - Leverage the latest techniques in quantum calibration to enable scaling to larger devices. - Optimize the performance of experiment & analysis tools to enable faster experiment throughput. - Develop dashboards that allow experimentalists to inspect and control the state of quantum device calibration. - Deploy and maintain cloud infrastructure that supports increasingly-complex science workflows. - Empower scientists to actively contribute to the codebase through mentorship and documentation. We are looking for candidates with strong engineering principles, a bias for action, superior problem-solving, and excellent communication skills. Working effectively within a team environment is essential. As a Research Software Engineer embedded in a broader research science organization, you will have the opportunity to work on new ideas and stay abreast of the field of experimental quantum computation. A day in the life The majority of your time will be spent on projects that extend the functional capabilities or performance of our internal research software stack. This requires working backwards from the needs of our science staff in the context of our larger experimental roadmap. You will translate science and software requirements into design proposals balancing implementation complexity against time-to-delivery. Once a design proposal has been reviewed and accepted, you’ll drive implementation and coordinate with internal stakeholders to ensure a smooth roll out. Because many high-level experimental goals have cross-cutting requirements, you’ll often work closely with other engineers or scientists or on the team. About the team You will be joining the Software group within the MQS Center of Quantum Computing. Our team is comprised of scientists and software engineers who are building scalable software that enables quantum computing technologies.
See more jobs
View from space of a connected network around planet Earth representing the Internet of Things.
Get more from Amazon Science
Subscribe to our newsletter

Amazon.com | Conditions of Use | Privacy | © 1996-2026 Amazon.com, Inc. or its affiliates

Social