From warehouse automation to surgical assistance, many real-world applications depend on robots performing delicate, contact-intensive tasks. Often missing in these situations is the sense of touch: robots need to feel the forces on their fingertips to manipulate objects effectively. Despite years of effort, robust and scalable solutions to this problem remain out of reach, especially in industrial settings. One approach has been to use vision-based tactile sensors, in which cameras embedded in soft fingertips capture contact geometry. Researchers have used this approach to estimate object shape and pose, but computing the forces that correlate most with manipulation capabilities remains a challenge. Modeling tactile shear — the forces that arise when an object slides or rotates against a sensor — is crucial for building robots that can grasp objects, use tools, and perform complex manipulation skills. Our solution, HydroShear, gives simulators the ability to accurately model tactile forces, enabling robots to learn dexterous, contact-rich manipulation policies entirely in simulation. These policies transfer seamlessly to the real world with no modification, achieving a 93 percent average success rate across four challenging tasks. Bridging the tactile reality gap Simulators for robot locomotion have found success in real-world applications because physics engines model rigid body dynamics and proprioceptive sensing well. But subtle tactile forces and shear feedback are notoriously difficult to simulate accurately. This has made it nearly impossible for tactile sensors trained on simulators through reinforcement learning to succeed when deployed on real robots. Existing tactile simulators face a fundamental trade-off. Physics-based methods like finite-element methods accurately model contact forces but are too slow for training reinforcement learning policies at scale. Faster approximations, on the other hand, oversimplify how forces build up and change during contact. They miss critical events like the moment a gripped object begins to slide or the way a soft sensor deforms over time. Modeling touch with fidelity and speed HydroShear’s key innovation is to add new capabilities to an existing physics simulation technique known as hydroelastic contact models. Called path-dependent force tracking, this approach accurately tracks how forces accumulate over a soft sensor membrane during a physical interaction. Rather than computing forces based only on instantaneous contact, HydroShear remembers the motion history of the object as it moves across the sensor. More concretely, when a robot grasps an object and moves it, different points on the object's surface come into contact with the sensor at different times. HydroShear tracks each of these contact points individually, computing how the soft elastomer deforms as the object moves. It then converts these deformations into realistic force fields, accounting for friction, slipping, and the elastomer's material properties. The simulator handles full 3-D motion — tilting and rolling as well as in-plane sliding — which is essential for dexterous manipulation. It's also GPU parallelizable, enabling efficient large-scale policy training. We calibrate HydroShear by collecting controlled real-world data with a robot arm and vision-based GelSight Mini tactile sensors. The calibration isolates four key parameters: how forces dissipate across the sensor surface, how tangential and normal forces build up, and the friction coefficient between the object and the elastomer. This systematic approach ensures that the simulator accurately reproduces real tactile feedback. Validation: From simulation to real robots We evaluated HydroShear on four contact-rich manipulation tasks, each highlighting different challenges. In all tasks, the robot perceives touch and proprioception (joint positions and gripper state) and has no access to object poses. Peg insertion: The robot grasps a cylindrical peg at an unknown orientation and must insert it into a tight socket. Because the grasp pose varies with each trial, the robot must use tactile feedback alone to detect and correct alignment errors during insertion. Bin packing: The robot inserts a cube into a target slot within a crowded bin. Neighboring cubes partially block the slot, so the robot must push through multiobject contact while sensing forces from multiple directions simultaneously. Book shelving: The robot inserts a book laterally into a shelf, with gravity pulling perpendicular to the insertion direction. The book is larger than the fingertip, producing broad contact patches that make it difficult to localize the object from touch alone. Drawer pulling: The robot pulls open a drawer while external-force perturbations are applied at random times. The robot must detect when the handle begins to slip and tighten its grip just enough to maintain hold without crushing it. We trained reinforcement learning policies entirely in simulation using HydroShear, then deployed them on a real Franka robot with GelSight Mini sensors without any modification or fine tuning. HydroShear achieved a 93% average success rate across all four tasks. We compared against two strong baselines: TacSL, which uses simplified force approximations, and FOTS, a recent learning-based method. TacSL achieved only 34% success, while FOTS reached 58 to 61%. The performance gap underscores the importance of accurate tactile shear simulation. Interestingly, the performance difference correlates directly with simulation fidelity. On tasks like peg insertion, where precise force feedback is critical, HydroShear's advantage is most pronounced. On drawer pulling, which requires detecting and reacting to slippage, HydroShear's path-dependent force tracking proves essential. Faster and less expensive Accurate tactile simulation unlocks a powerful recipe for robot learning: train policies entirely in simulation, then deploy them on real robots. This approach is dramatically faster and cheaper than learning from real-world interactions, which can damage sensors and require extensive trial and error. For warehouse automation, the approach is particularly valuable. Tasks like bin packing, sorting, and careful handling require robots to feel their way through complex interactions. HydroShear enables robots to learn such skills without extensive real-world data collection. While HydroShear yields strong results when coupled with vision-based tactile sensors like GelSight, the underlying principles could extend to other tactile modalities. We're also exploring how higher-resolution sensor simulations and more-complex object geometries could further improve performance.

Reinforcement learning (RL) is one of the techniques we use to make language models better at sustained, multistep tasks like writing code, navigating a website, or carrying out a research workflow. The model doesn't act alone in those settings; it's wrapped in a piece of software we call a harness, which lets it call tools, observe the results of using them, and decide what to do next. To improve such a model with RL, we let it attempt many tasks inside the harness, score how well each attempt went, and use the score to nudge the model's parameters toward the choices that worked. The hard part turns out to be the bookkeeping. To turn a scored attempt into a parameter update, the trainer needs an exact record of what the model produced — not a summary, and not a transcript that looks as though it captures a complete exchange but drops vital information. Internally, models see text as a sequence of numbered units called tokens; an English sentence might have 10 or 20 tokens, each assigned an integer ID by a piece of software called a tokenizer. Two strings that look identical in a transcript can map to different token IDs after a small change of formatting, and that gap, however small, is enough to make the trainer optimize against a slightly different past than the one the model actually experienced. Today we're releasing Turnstile, a small proxy written in the Rust programming language that sits between any agent harness and the backend system that runs the model. Turnstile records the exact token-level history of every request as it happens, at the only point where that history is unambiguously correct: the moment of generation. It then exports a generic, framework-neutral trajectory that can feed into whichever RL training stack you already use. We use Turnstile to drive real RL training runs. In the validations we report here, two different agents — a text-only coding agent and a multimodal computer-use agent — improved steadily over the course of their RL runs. In both cases the agent harness was left unchanged, and the data Turnstile records flowed directly into the training stack and produced the expected learning signal end to end. Tokens, rollouts, and why agent transcripts can lie Three pieces of vocabulary do most of the work in the rest of this post, so it's worth grounding them up front. A tokenizer is a deterministic function that turns text into a list of integer token IDs and token IDs back into text. Each model is paired with a specific tokenizer; you can't substitute one for another. The tokenizer is unforgiving: a stray space, a different way of writing a tool call as JSON, or a slightly different chat template (the format string a serving system uses to wrap roles and messages into a single text input the model can read) can change the token IDs even when the rendered text looks the same to a human. We'll call this kind of mismatch retokenization drift when it comes from rerunning a tokenizer over text we’ve already seen and chat template drift when it comes from the surrounding format changing under us. A rollout is one recorded attempt at a task: the prompt, every tool call, tool feedback, the model’s responses, and the final outcome. The version of the model that produced the rollout is called the behavior policy. The mathematics of policy-gradient RL works cleanly only when the trainer optimizes the model's behavior against the context the behavior policy actually saw. If we rerender the prompt and end up with a slightly different token sequence, we're now training the model against a context unfamiliar to the behavior policy. The training signal degrades, sometimes invisibly, since the model still appears to be learning. That is why agent harnesses make the problem worse rather than better. A harness is not a static prompt; during a single rollout it may compact older messages to save context, retry a malformed tool call, branch into subagents, merge their results back, or summarize history. All of that is normal, useful agent behavior. But each rewrite is another chance for the next request's token sequence to drift away from what the model actually generated last turn. The transcript a harness produces is a faithful record of the conversation; it is not, in general, a faithful record of the tokens, and it is the tokens the trainer needs. Capturing tokens at the proxy boundary Turnstile's central design choice is to stop trying to reconstruct token-level state from text after the rollout is over. We capture it at the moment of generation, where it is already correct, and we do that without changing the harness. The proxy speaks the same HTTP API every modern agent harness already speaks: the OpenAI Chat Completions API, which has become the de facto standard for "send a list of messages, get back a response." The harness creates a rollout group with Turnstile, points its Chat Completions client at Turnstile's address instead of the real backend, and runs unchanged. Behind the scenes, every request flows through Turnstile to the inference backend (today SGLang, with vLLM planned). Turnstile records the exact token IDs the model sampled, the per-token log probabilities (the model's own confidence values for each token, expressed as logarithms; the trainer needs these to compute its update), and a loss mask that marks which tokens were generated by the model and should contribute to training versus which came from the user, tools, or the system prompt and should not. When the rollout is finished, the harness asks Turnstile for the recorded trajectories. Each trajectory is a TrainingSequence object containing the token IDs, log probabilities, the loss masks for the full sequence, and a record of which version of the model's weights was active during which spans of the sequence. (The trainer needs these weight version boundaries to know if the model parameters changed mid-rollout because of an asynchronous update.) Turning that into the specific batch shape your trainer wants is straightforward adapter work: attach the reward, expand the mask, and hand it off. Existing harnesses can stay black boxes There are a number of agent harnesses, such as OpenHands, Codex, and Terminus, that are already useful but were not designed as training runtimes. Without Turnstile, using one of these to drive an RL training run requires it to record token IDs, log probabilities, masks, and routing traces; in practice, that work often falls to a separate harness-shaped component built inside the training system. Either way, a harness ends up acting as a token-level RL data pipeline, and that is the wrong abstraction. The harness knows the information it intended to send to the model, but it does not, in general, know the exact token sequence, cache state, routing trace, or processed multimodal inputs the model actually used. Those live in the backend. With Turnstile, the production harness doesn't have to log training data. It points its Chat Completions client at Turnstile instead of the inference backend and otherwise runs unchanged. Turnstile records the model-facing rollout state: it does not need to understand the harness's private control flow or the semantic reason a context changed. If the next request is a faithful token-level extension of an earlier one, Turnstile merges it into the same trajectory. If the harness compressed memory, rewrote history, merged a subagent result, or otherwise changed the prefix in a way that cannot be proven equivalent, Turnstile starts a new sequence and keeps the trainable suffix honest. All this applies in the strict black-box case: a proprietary harness whose internals are closed to the training system can still drive an RL training run, with no source-level integration at all. Below are two examples of using Turnstile with open-source harnesses in a black-box fashion. Multiturn agents and prefix-aware trajectories A naïve way to store these recordings would be to treat every request as an independent training example. That’s wasteful, because each new request includes the whole conversation so far, so the same token strings would end up being duplicated over and over. It’s also subtly wrong, because it loses the relationship between turns. Instead, Turnstile stores a multiturn rollout as a single growing token path — so long as the path is faithful to what the model actually saw. When a later request to the model is just the previous request plus a few new tokens at the end (the new user message, a tool result, an LLM response), Turnstile recognizes the overlap at the token level — not by comparing rendered strings but by checking that the previously captured token IDs really do appear unchanged at the start of the new request. If they do, the two turns become one continuous trainable sequence with the loss mask correctly identifying which spans were the model's outputs. When the next request cannot be safely extended from a previous one — because the harness rewrote earlier messages, or the tokens drifted for some reason — Turnstile does not pretend otherwise. It starts a new training sequence. We call this "exploding the trajectory". It costs more training tokens than the optimistic alternative, but it ensures that every token string used for RL training is one the behavior policy actually saw. The point is not to maximize compactness; the point is never to lie to the trainer about what happened. Mixture-of-experts routing adds a hidden dimension Some modern models use a mixture-of-experts (MoE) architecture, in which only a small subset of the model's parameters — called experts — are activated for any given input token. The choice of experts is itself part of the computation, made by a small router network at every layer. The routing decision depends on the activations at each layer, and tiny differences in how the previous tokens were processed can change which experts are picked. This matters for RL because, even if two requests have the same token IDs, the tokens might get routed to different experts on different runs. Last fall, researchers at Peking University and their colleagues characterized this discrepancy and proposed recording the MoE model’s routing decisions so the trainer can replay them. We adopt the same principle. When MoE capture is enabled, Turnstile asks the inference backend for the routing trace and records it alongside the tokens. Every time it extends the token path, it checks that the routing for the shared prefix matches what was recorded last turn. If it doesn't — for example, because a key-value cache miss forced the backend to recompute the prefix and pick different experts — Turnstile splits the trajectory rather than train under the wrong routing. Multimodal rollouts When the model also takes images as input — a vision-language model — the rollout has another piece of state to keep track of. The model doesn't see the raw bytes of the uploaded image; it sees the output of an image processor, a fixed pipeline that resizes and crops the image, converts it into a tensor of pixel values, and inserts placeholder tokens into the text to mark where the image goes. The same image bytes can produce different tensors as the result of a different processor version, a different resize policy, or a different patch geometry, and the placeholder count can change with the input dimensions. If the RL trainer has to reprocess the image from scratch, the visual prefix it trains under may not be the visual prefix the behavior policy saw. Turnstile treats image processing as part of the rollout. When a request includes an image, Turnstile decodes it, hashes and stores the original bytes for audit, runs the model's configured processor, and records the processed pixel features in the same trajectory as the token IDs, in the order in which the placeholders appear. The exported sequence carries both the raw and processed visual data, so the trainer can use whichever it needs. Where this is going Turnstile is early. The current implementation has a Rust core, an SGLang backend, Python bindings for in-process training scripts, prefix-aware multiturn capture, optional MoE routing capture, and multimodal support. Near-term work is broader: a vLLM backend, more training-framework adapters, and more multimodal-model coverage. The long-term shape is unchanged from the design we started with: agent harnesses should not have to become RL data pipelines, and trainers should not have to guess what happened from rendered text. The model sampled the tokens. We record them. Additional references Turnstile is now available on Github OSWorld and its open-source agent harness OpenHands THUDM/slime Prime Intellect renderers blog Prime Intellect renderers GitHub prime-rl algorithms (extension property, multi-turn trajectory merging) prime-rl inference (router replay) Polar: Agentic RL on Any Harness at Scale NVIDIA-NeMo/ProRL-Agent-Server Stabilizing MoE Reinforcement Learning by Aligning Training and Inference Routers rLLM Agent Lightning Strands Agents SGLang provider AcknowledgementsSpecial thanks to Keagan Long, Daisy Lin, Changlong Yu, and Yifei Wang for their contributions to this work.

At Amazon, we believe that as our strategy to reach net-zero by 2040 evolves, we need to continue to raise the bar on what and how we measure. Measuring carbon emissions across our entire business is complex, and the tools and methodologies available are continuously improving. Each year, we report on our carbon intensity, absolute emissions, and sustainability progress in our Sustainability Report, and we continue to adopt more-precise tools and methodologies to ensure our data is as meaningful and as representative of our decarbonization journey as possible. Carbon intensity — the amount of emissions per unit of activity or production — is one of the most important tools for tracking decarbonization progress. But not all activities are the same. Across industries, some of the most meaningful intensity metrics are sector specific, tied to the actual activity being decarbonized, across buildings, energy, transportation, and products and beyond. Examples of metrics used by companies include carbon dioxide equivalent per megawatt-hour for electricity, per square foot for building decarbonization, and per kilometer for transport. At Amazon, we apply the same principle: we are developing intensity metrics tailored to specific business activities, so we can measure what matters most. Emissions per unit shipped For Amazon's retail operations, we track carbon emissions per unit shipped. This metric matters because it directly reflects the efficiency of our delivery operations at scale. We’ve reduced emissions per unit shipped every year since 2019, resulting in a carbon intensity reduction of 39% at the end of 2025, relative to 2019. As we ship more packages, we're doing so with less carbon per unit, and our investments in carbon-free energy, smarter routing, lighter packaging, low-carbon fuels, alternative transportation methods (like rail versus road or air), and electric vehicles are all translating into real per-unit reductions. We also track carbon intensity at the regional and country level to understand geographic variation and target interventions accordingly. It's the clearest measure of whether we're decoupling delivery growth from emissions growth. Why this is unique to Amazon Amazon is more than a traditional logistics company: we're also a pharmacy, a grocery store, a cloud services company, a movie studio, a device manufacturer, a satellite business, and much more. As a result, our emissions span the entire value chain — from the manufacture of goods, long-haul shipping, and air freight to warehousing and distribution and middle-mile and last-mile delivery. Amazon’s decarbonization efforts require strategies that can address significant portions of global transportation and supply chains simultaneously. That breadth creates complexity — and opportunity. Solutions that we develop together with our suppliers and partners don’t only stay within the four walls of Amazon; they have the potential to drive decarbonization across multiple industries at once. This is a responsibility we take seriously: we’re proud of our progress and want to share what we are learning along the way. Simplifying our economic intensity metric Part of sharing what we learn is being transparent about how we measure and what we change. One change that we’ve made recently is in our economic carbon intensity indicator. In our 2025 reporting, we updated this from grams of carbon dioxide equivalent per dollar of gross merchandise sales (gCO2e/$GMS) to grams of carbon dioxide equivalent per dollar of revenue (gCO2e/$Revenue). Revenue is publicly reported, widely understood, and aligns with how most companies disclose the carbon intensity of their operations— making our progress easier to compare with the rest of the industry’s. This update does not change our year-over-year trajectory. Looking ahead Climate science and carbon accounting are not static, and as the science and our own operations evolve, we'll continue to refine how we track and report our progress. We’re proud of our Climate Pledge goal to reach net-zero carbon by 2040. We’ll continue updating how we measure, so our data always reflects the most precise and meaningful picture of where we are and where we’re headed. To learn more about Amazon's carbon methodology, visit our Sustainability reporting website.

Amazon is investing in next-generation nuclear technology to meet the rising energy demands of AI infrastructure and cloud computing, and at the heart of that technology are tristructural isotropic (TRISO) fuel particles. This is not your grandparents’ nuclear-reactor fuel. These tiny, robust TRISO particles represent a step forward in the design, performance, and inherent safety of reactor fuel. TRISO: A materials science breakthrough in every particle To understand why TRISO-based fuel is exceptional, consider what reactor fuel must do. In addition to sustaining a controlled fission reaction, it must contain the radioactive byproducts of that reaction, known as fission products. These include noble gases, volatile metals, and long-lived isotopes. Fuel must reliably isolate them throughout operation and into long-term storage, protecting both plant personnel and the public. At less than a millimeter in diameter, each TRISO particle is about the size of a poppy seed, but it acts as a miniature containment system. At its center is a kernel of enriched uranium, surrounded by an inner buffer of porous carbon. Then comes a ceramic shell with three layers (hence the word “tristructural” in the particles’ name): a dense pyrolytic-carbon layer, a silicon carbide (SiC) layer, and an outer pyrolytic-carbon layer. The ceramic shell ensures containment. The silicon carbide layer acts as a pressure vessel and chemical barrier. SiC's hardness, corrosion resistance, and melting point above 2700°C give TRISO particles exceptional mechanical integrity and thermal resilience. Those properties persist even in conditions commensurate with the worst hypothetical criticality accident. Data from the U.S. Department of Energy's Advanced Gas Reactor Fuel Qualification Program (AGR) show that irradiated TRISO particles, subjected to 1600°C for 300 hours, exhibited no detectable failures, with an upper-bound failure fraction of ≤ 6.6 × 10⁻⁵. At 1800°C, failure rates remained well below conservative design limits. These findings were based on the fabrication, irradiation, and testing of more than 500,000 TRISO particles since 2002. The proven durability of these TRISO coatings also preserves long-term stability in spent fuel better than today’s fuel, potentially for as long as 100,000 years. Fuel form flexibility and operational efficiency For decades, commercial light-water reactors have relied on uranium oxide fuel pellets clad in zirconium alloy tubes. This well-established combination has delivered stable, reliable power with a strong safety record in the global reactor fleet. TRISO-based fuels build on this foundation and offer engineers greater flexibility in fuel form and reactor design. Because each TRISO particle contains its own fission-product barriers, nuclear fuel designers can explore novel configurations that enable new operational modes. In pebble-bed reactors like the X-energy Xe-100, in which Amazon is investing, TRISO particles are embedded in tennis-ball-sized graphite spheres that circulate continuously through the core. This motion allows operators to refuel without shutting down the reactor, monitor fuel consumption in real time, and minimize the amount of unburnt uranium in spent fuel. These efficiencies support both resource conservation and waste reduction. TRISO-based fuels can also accommodate different core geometries, so they’re compatible with a range of newer reactor designs focused on safety. Cylindrical compacts are well suited for prismatic cores, for instance, while spherical pebbles enable pebble-bed configurations. This geometric flexibility also allows for the integration of advanced coolants. Unlike conventional light-water reactors, many TRISO-fueled designs — such as the Xe-100 — use high-temperature helium as the primary coolant. Others explore the use of clean molten salt. These alternatives improve thermal efficiency, enable passive heat removal, and further expand the potential applications for advanced reactors. Enrichment and the supply chain TRISO particles are manufactured using high-assay low-enriched uranium (HALEU), enriched to between 10% and 20% ²³⁵U. HALEU offers higher energy density than traditional low-enriched uranium while remaining below the threshold for highly enriched uranium. The use of HALEU in TRISO-based fuels supports compact, high-output designs like the Xe-100 by enabling higher fuel loading and energy density. Each unit produces 80 megawatts of electricity, and up to 12 can be collocated. This modular approach allows right-sized deployment and operational flexibility. HALEU production requires dedicated infrastructure. As enrichment levels increase, separative work becomes more demanding. Centrus Energy operates a U.S.-based HALEU cascade, and the Department of Energy has launched programs to accelerate commercial access. Fuel fabrication has also progressed. TRISO-X, a public-private venture at Oak Ridge National Laboratory, produces TRISO fuel at kilogram scale and is expanding commercial capacity. Standard Nuclear continues developing sol-gel processing, which yields spherical uranium oxide microspheres for TRISO kernels. Amazon's role in deployment Amazon has invested in the Cascade Energy Center, a project to deploy TRISO-fueled Xe-100 reactors in central Washington. With participants such as X-energy, Energy Northwest, Korea Hydro and Nuclear Power, and Doosan Enerbility, the project plans to bring as many as 12 Xe-100 units online to power data centers and cloud infrastructure. The Xe-100 is licensed for construction, TRISO fuel production is active, and project sites are under development. The time is now As a nuclear-engineering professor and researcher focused on advanced reactor technologies and fuel development, I can say with confidence that TRISO particle fuel is the most robust nuclear fuel we have ever developed. Its resilience has been confirmed through rigorous experimentation, and its readiness is evident in a growing manufacturing base and commercial momentum. TRISO-based fuels support reactors that build on decades of engineering progress and deliver clean energy with new capabilities. These systems operate flexibly, scale efficiently, and meet the demands of today’s evolving energy landscape. The future of nuclear fuel is not hypothetical. We are building it now — particle by particle.

Today we announced the general availability of the new M9g and M9gd instances of Amazon Web Services’ (AWS’s) Elastic Compute Cloud (EC2), the first instance types powered by Graviton5, the latest generation of our general-purpose CPU. Graviton5 doubles the number of cores from the previous generation, from 96 to 192. They’re also the first instance types to use the new Nitro Isolation Engine, a component of the Nitro Hypervisor whose sole job is isolating virtual machines (VMs) from each other. In this post, we explain how we used the Isabelle/HOL (higher-order logic) proof assistant — software that mechanically checks reasoning steps for adherence to the laws of logic — to prove that the Nitro Isolation Engine behaves correctly and enforces isolation between virtual machines. The Nitro Isolation Engine is the critical component of the first formally verified hypervisor to be deployed in a commercial cloud environment. Our Isabelle/HOL model and proof comprise 330,000 lines of machine-checked mathematics. It’s comparable in scale to seL4, the landmark project that first demonstrated that realistic operating-system verification was feasible and was an inspiration for our own work. However, unlike seL4, the Nitro Isolation Engine is designed for a commercial cloud environment and ships on production hardware as an always-on feature for Graviton5 users. Our talk at Amazon’s 2025 re:Invent conference introduces our formal-verification methodology, and our white paper is a more detailed discussion covering important aspects of the results, such as scope and assumptions. This blog post gives an informal overview of the main aspects of our formal-verification work and how they fit together. What is a separation kernel? John Rushby coined the term “separation kernel” in 1981 to describe a minimal OS component that partitions a system into isolated compartments. The key idea: separate policy from mechanism. A separation kernel does not decide what to isolate, how to allocate resources, or which VMs to schedule: those decisions are made elsewhere. Instead, it focuses solely on enforcing isolation, and this clarity of purpose makes separation kernels much simpler to implement than full OS kernels. Since its introduction in 2017, the Nitro Hypervisor has been responsible for enforcing isolation in EC2, but it also handles business logic, device drivers, and AWS-specific features. That complexity makes proving correctness much more difficult. Moreover, the Nitro Hypervisor was not designed for verification from the start. Distilling the hypervisor’s critical isolation logic into a minimal component, the Nitro Isolation Engine, makes it small enough to verify and audit, giving customers unprecedented visibility into how isolation is enforced. We also wrote the Nitro Isolation Engine in Rust, a language that lends itself more naturally to formal verification. The Nitro Hypervisor still handles policy — VM creation, resource allocation, migration, scheduling — but it is now deprivileged and must ask the Nitro Isolation Engine to perform any operation touching guest state. The Nitro Isolation Engine checks every request before acting. Specifications and proofs The two key parts of our work are specifications and proofs. Formal specifications precisely capture the expected behavior of the system, and proofs establish that the implementation meets those specifications. Our theorems about the Nitro Isolation Engine address four types of properties: Confidentiality and integrity. Only authorized information flows can occur. For example, guest memory allocations are always scrubbed before reuse. Functional correctness. The implementation behaves exactly as specified. Absence of runtime errors. There are no runtime errors such as unwraps of None option values in Rust — an erroneous command invocation that will stop program execution. Memory safety. There are no issues such as buffer overflows and NULL pointer dereferences. In practice, we handle the last three properties collectively, as a functional-verification result, with confidentiality and integrity treated separately, because we use different proof techniques for each. Functional verification For functional verification, the key parts are a formalization of a core subset of the Rust language, called μRust (“micro Rust”); an expressive specification language using Separation Logic for precisely capturing specifications; and a verification technique, weakest-precondition calculus, with custom proof automation for proving a program correct with respect to its specification. Each of these is part of a general-purpose proof infrastructure that we open-sourced in 2025 as the AutoCorrode library. In more detail, μRust is a restricted subset of the Rust programming language that is expressive enough to write the Nitro Isolation Engine but amenable to formal reasoning because we deliberately excluded advanced Rust features, such as traits and dynamic dispatch. The formal semantics of μRust is defined as a shallow embedding in Isabelle/HOL, which means that the meaning of μRust is defined in terms of higher-order logic, the “host language” of Isabelle/HOL. The specification for a μRust program is defined as a contract with pre- and postconditions, which are assertions about the system state before and after executing the program. Our contracts specify “total correctness”, which means that in all states that satisfy the precondition, the program always terminates, and the resulting state satisfies the postcondition. This total-correctness condition also means the program is memory safe and free of runtime errors. Our specifications are written using Separation Logic, a logic designed to reason about low-level pointer-manipulating programs. Despite the relative simplicity of separation kernels, with the verification of the Nitro Isolation Engine we are still operating on the edge of what is possible with formal verification, and both our specifications and proofs grow very large. For example, the following specification captures what happens when an executing guest virtual CPU tries to turn itself on (an erroneous request): While the specification above is complex, what it captures is intuitively straightforward: in this circumstance, the Nitro Isolation Engine sees that, to act as the caller, the virtual CPU must be turned on already, and it therefore returns a defined error code, AlreadyOn. Everything else about the system state remains unchanged. The complexity in the specification is a reflection of the depth of our modeling and the fact that several other error checks must already have been performed for us to have reached this point in the implementation of the Nitro Isolation Engine. To prove a μRust program correct with respect to its specification, we use a standard weakest-precondition calculus. A weakest-precondition calculus is a systematic way to identify the least restrictive constraint that can ensure that the state of a program after a particular operation is not outside some specified range of states. For example, the weakest precondition of the expression "x + y" is the state in which the values of x and y cannot overflow the addition. The proof obligation then is to show that the contract’s precondition entails the computed weakest precondition. Confidentiality and integrity For confidentiality and integrity, the first key part is a high-level specification that captures the behavior of the Nitro Isolation Engine as a transition relation, where each “high-level” step of the system (e.g., hypercall) is an atomic transition. This specification is rigorously connected to the more concrete Separation Logic specification used in our functional-verification results, which uses another proof idea called Refinement. The second key part is the idea of noninterference. Noninterference is the idea of indistinguishability preservation that we use to make confidentiality and integrity mathematically precise. The idea is that if two states are indistinguishable to an observer before a step, they must remain indistinguishable afterward. The intuitive reason why this captures confidentiality is that the observer has learned nothing new because of the step. Understanding why indistinguishability preservation guarantees confidentiality is subtle. Consider two simple machines, A and B, each with one public and one private register. An observer considers them indistinguishable if their public registers match: the private register is hidden. In the following diagram, A and B are indistinguishable: Now consider what happens if we execute a program that branches on the private register to assign 1 to the public register. The resulting machines A' and B' now have different public registers — they're distinguishable! A clever observer could use this to deduce the original private values, and this failure to preserve indistinguishability corresponds to illicit information flow to the observers. And more to come We hope you’ve enjoyed this overview of the main pieces of our verification work. There are many other aspects to our work, such as conformance testing and how we handle reasoning about concurrent code, that we’re excited to share in future posts.

AWS Graviton processors have improved steadily across generations, with each iteration delivering advances in computational performance, price performance, energy efficiency, and memory capacity. Today, Amazon announced the general availability of the new M9g and M9gd instances of its Elastic Compute Cloud (EC2), for general-purpose workloads. These are the first Amazon products powered by Graviton5, the latest generation of Amazon’s CPU. After five generations of custom silicon and eight years of continuous investment, Graviton powers over 350 instance types that are suitable for workloads including web applications, microservices, analytics, databases, machine learning inference, electronic design automation, gaming, video encoding, and agentic AI. Graviton5 doubles the number of cores from Graviton4, from 96 to 192, and it supports DDR5-8800 memory and the latest PCIe gen6 interconnects. We’ve worked closely with leading DRAM manufactures to meet the DDR5-8800 level of performance, and AWS Graviton instances deliver the fastest memory of any processor instances in the cloud. With Graviton5, Amazon also moved to a three-nanometer process, enabling greater circuit density and faster on-chip communication. Not only does Graviton5 pack in more cores than Graviton4, but each of those cores offers 25% better performance. We've talked for a while about how micro benchmarks are very different from big, real-life workloads, and we design for our customers’ actual workloads — not small loops but all the code and complexity of a real application like a database. To execute code quickly, modern processors predict branches that come from control flow in programs and speculatively execute the predicted paths. The Neoverse V3 core used in Graviton5, codefined by Arm and Amazon’s Annapurna Labs, substantially improves the branch prediction capability of the CPU, and that in turn makes it able to execute real applications like databases up to 30% better. The DRAM of a CPU can be about 100 nanoseconds away. That doesn’t sound like a lot, but for a CPU that runs at 3.3 gigahertz, one memory access takes 330 cycles. CPUs use caches to bring data closer to the CPU, and when a request can be fulfilled from one of these caches, the CPU doesn’t have to wait for the full DRAM latency. Graviton5 has 64-kilobyte first-level caches, two-megabyte second-level caches, and 192 megabytes of level-three cache — more than five times as much as the previous generation of Graviton. Graviton3 was the first Graviton CPU to adopt a chiplet architecture, using seven dies across cores, DRAM controllers, and PCIe controllers. Graviton4 followed the same architecture as Graviton3, with a few refinements. However, in Graviton5, we’ve changed it substantially: the 192 cores in Graviton5 are split across four chiplets, with each chiplet containing DRAM controllers, PCIe controllers, and 48 cores, with custom die-to-die connectivity that provides up to 420 gigabytes per second of bandwidth between chiplets, minimizing latencies between cores in the mesh. There is no longer a separate I/O die nor a separate DRAM controller die. This organization allows us to configure two or four nonuniform-memory-access (NUMA) regions per chip and partition the size of the L3 cache to the size of the virtual machines (VMs) running on the CPU while reducing memory latency for VMs that are 48 cores or smaller. With these enhancements, Graviton5 offers up to 25% better computational performance than Graviton4-based instances, with up to 35% faster performance for web applications, up to 35% for machine learning inference, and up to 30% for databases. The M9g and M9gd instances that are powered by Graviton5 are also raising the bar on security even further with the introduction of the Nitro Isolation Engine. The Nitro Isolation Engine is an enhancement to the Nitro System, which enforces isolation of instances and harnesses formal verification to provide assurances of isolation with mathematical precision. The Nitro Isolation Engine is a purpose-built component that is responsible for enforcing isolation between VMs, including mediation of all access to VM memory, CPU register state, and I/O devices through a minimal set of APIs. The Nitro Isolation Engine leverages formal verification, a technique for mathematically demonstrating that hardware or software behaves as intended, and not just in specific test cases. This intensive verification establishes Nitro as the first formally verified cloud hypervisor, pioneering a new standard for mathematically proven cloud security. To learn more about the Nitro Isolation Engine, read the Amazon Science blog post or our technical white paper.

The year 2026 marks a definitive shift in the AI landscape: we have moved from models that simply know to agents that do. Foundation models (FMs) — large Transformer models pretrained with massive datasets and fine-tuned for diverse downstream tasks — have moved far beyond chatbots, coding, and other digital applications. They are now used as the cognitive engines for AI agents in the physical world, where they plan, use tools, and execute multistep tasks across complex, digitally integrated environments, from warehouses and factories to transportation systems and hospitals. At Amazon, you can see the transition to this new era of "physical AI" in the debut of Project Eluna, an agentic AI model designed to transform how Amazon fulfillment centers operate. To be useful in a high-stakes physical environment, however, an agent needs to be more than fluent in natural language; it needs to be grounded in physical laws and operational constraints. In particular, we must overcome the challenge of hallucination, which, in virtual environments, takes the form of fabricated information — made-up citations, factual inaccuracies, and logical fallacies, all output with high levels of certainty. In a physical system, such hallucinations can lead to violations of reality, with detrimental consequences. For example, if an agent suggests a robotic path that ignores the momentum and mass of the items being moved, its output could be potentially dangerous to people or result in damage to products or equipment. In this article, I propose four approaches to grounding AI agents in the physical world, where "grounding" is defined as the integration of external information, including domain-specific datasets, physical principles, and numerical simulations, to contextualize a model's reasoning. All four approaches can be used separately or in combination, depending on the specific application. Practical implementation of these approaches will not only accelerate the safe and productive use of AI agents but could allow for their further expansion into new domains. Four pillars of grounding Project Eluna is an agentic AI model that lives in the cloud and assists operators who manage operations within fulfillment centers via digital dashboards. It’s designed to act with a degree of autonomy, reasoning through complex operational situations and recommending actions to operation managers. It pulls in historical and real-time data — such as the states of conveyor belts or robots — to anticipate bottlenecks and keep operations running smoothly. The four approaches to grounding AI agents that I describe here grew out of my research at the University of California, San Diego, and with the Amazon Fulfillment Technology (AFT) team, and they help ensure that agents like Eluna are physically consistent and operationally reliable. 1. Physics-guided deep learning. Traditional foundation models can learn to mimic statistical patterns in data but often fail to respect the hard constraints of the physical universe, such as the conservation of mass, energy, or momentum. In physics-guided deep learning (PGDL), we integrate first-principle physical knowledge into the foundation model in pretraining. First principles include symmetries, such as inductive biases like rotations and other transformations, and differential equations that could be used, for instance, in a robot’s motion and control. Not only does this ensure that predictions obey governing physical laws, but grounding a model in physics allows it to learn from significantly smaller datasets. If the model already "knows" the fundamental principles of dynamics, it requires less data to achieve satisfactory accuracy. 2. Uncertainty-aware reasoning. LLMs often exhibit overconfidence in uncertain predictions, which can lead to the assertion of misinformation with high certainty. For an AI agent to be trustworthy in a mission-critical setting, it must know when it does not know. Using our framework (UQ4CT), we produce calibrated uncertainty over the space of functions that map input prompts to outputs. The framework uses an approach called mixture of experts, in which the model is divided into smaller “subnetworks”, each with specific expertise. Our UQ4CT framework allows the model to dynamically align its confidence estimates with predictive correctness. Practically speaking, an agent grounded using calibrated uncertainty can halt or request human intervention when its internal uncertainty exceeds a safety threshold, ensuring reliability even when a model has been fine-tuned with relatively small datasets such as epidemiological forecasts or rare weather events. UQ4CT preserves high accuracy across five benchmarks while demonstrating over 25% reduction in expected calibration error (ECE), a measure of how well a model's estimated "probabilities" match the true, observed probabilities. Even under distribution shift, UQ4CT maintains superior ECE performance with high accuracy, showcasing improved generalizability. 3. Bridging the text-to-numerical gap. While foundation models are masters of natural language, the laws of the physical world are written in the language of mathematics and high-dimensional data, the kind used in fields like robotics, supply chain management, and finance. A trustworthy agent must translate human intent, expressed through language, into precise numerical execution without losing accuracy. Our group developed the adapting-while-learning (AWL) framework, which relies on two key mechanisms. The first is called world-knowledge distillation, where AI agents interact with simulators of the physical world to gather a range of information about what’s physically possible. This knowledge is internalized through supervised fine tuning, effectively grounding the agents’ future outputs. The second mechanism is dynamic tool adaptation, in which a foundation model calls a specialized numerical simulator when it recognizes that its original training is insufficient for the complexity of the current task. This approach is particularly useful in climate science or epidemiology. For instance, if scientists need to plan for vaccine distribution, their original model would call on outside datasets representing disease dissemination. Compared to original models without AWL, those post-trained with AWL achieved 29 percent higher answer accuracy and 12 percent better usage of simulator tools, even surpassing state-of-the-art models including GPT4o and Claude-3.5 on physical-science datasets. 4. Verifier-augmented grounding. Verifiers are software external to LLMs that can be used to ensure that the models work within the bounds of logic and reality. Our weather AI agent, Zephyrus, uses verifiers to refine the reasoning of foundation models in weather science. Zephyrus works in a “reflective” interactive loop, where the agent writes code to query outside weather datasets, observes physical results, and revises its reasoning if the output is flagged by a verifier as scientifically implausible. Another verifier, Hilbert, is used specifically for mathematical reasoning. LLMs, in general, can already generate mathematical proofs, but they need humans to verify whether these proofs are correct. However, there exist so-called proving systems, such as Lean 4, that can offer automatic verification. This has prompted efforts to build specialized prover LLMs that can generate proofs in formal mathematical language. So far, however, these provers solve substantially fewer problems than general-purpose LLMs operating in natural language. Hilbert bridges this gap by breaking complex mathematical problems into subgoals and using feedback from a separate formal verifier to validate them recursively. This process ensures that the agent’s outputs are provably correct. We’ve shown an impressive 422 percent performance improvement over the best publicly available prover LLM. Looking ahead We believe these four pillars lay a solid foundation for grounding LLMs in reality. Meanwhile, several research directions stand to deepen the connection between AI agents and the physical world. First, foundation models can be fine-tuned to interact with more complex, multifidelity numerical simulations, moving beyond function calls to agentic tools and toward an internalized sense for when and at what fidelity to invoke a simulator during reasoning. Second, uncertainty can serve not only as a hallucination detector but also as an intrinsic reward signal, training agents to explore areas of the environment where they have low confidence, high surprise, or incomplete knowledge. Third, physical laws and domain constraints can be embedded as formal verifiers during process planning. They can check every proposed action against conservation principles, kinematic limits, and safety envelopes before execution. As these techniques mature, they will increasingly work in concert: an agent that couples physics-guided learning with calibrated uncertainty and formal verification will be far more robust than one relying on any single pillar alone. Ultimately, as AI agents expand into increasingly complex physical domains, faithful reasoning and effective grounding will be the guiding principles to ensure that agentic AI operates safely, reliably, and at scale across the physical world.

AI agent performance is not just a modeling problem; it is fundamentally a systems problem. A modern agent combines an LLM with a harness, software that mediates the LLM’s interaction with tools and manages the cycle of reasoning and feedback: you can think of the harness as the operating system around the model. As models improve, the performance bottleneck shifts from the model’s ability to reason to the harness’s ability to translate model intent into actions and reflect execution outcomes back to the model. In a paper we just published on arXiv, "Dissecting model behavior through agent trajectories", we formalize this bottleneck as the intent-execution gap: the mismatch between what the model intends and what the harness executes, and vice versa. For example, in trying to revise code, a model may intend to edit a single instance of a function, while the harness accidentally modifies multiple instances. We show that minimizing this bidirectional gap — without any task-specific tuning — is sufficient to achieve state-of-the-art performance across diverse agentic benchmarks, including datasets that test real-world repository patching (SWE-Pro, SWE-Verified) and interactive terminal environments (Terminal-Bench2). While the most visible components of the harness — such as the execution graph, which controls iterations over the thought-action-observation process, and tools — are natural candidates for improvement, we highlight that seemingly trivial implementation details lead to nontrivial fluctuations in performance. Factors such as environment interaction timeouts, infrastructure stability, and resource constraints also materially affect performance. Thus, benchmaxing, or reporting higher numbers on benchmarks, may not necessarily quantify underlying model/harness capability, as it is additionally influenced by the basic infrastructure parameters used during evaluations. We also introduce Simple Strands Agent (SSA), a lightweight and customizable single-agent harness designed to close the gap between the performance reported in agent documentation and the performance seen in open-source implementations. SSA achieves consistent gains in performance across multiple models and benchmarks. Finally, we show that effective agent design is not entirely model agnostic. While many principles generalize, model families differ in tool use preferences, feedback interpretation, and context sensitivity, making model-harness codesign a critical factor in achieving optimal performance. Motivations It is well established that problem-specific customizations such as tuned prompts, tailored tools, and specialized execution graphs can improve AI models’ performance in a controlled setting (fixing all other factors, such as evaluation infrastructure). However, we observed that many such optimizations fail to transfer between models. Improvements that work for one model or version often degrade, disappear, or even regress with newer models. This lack of transferability exposes a deeper issue: many optimizations implicitly overfit the behavior of a specific model. As models improve, these behaviors change, making such gains brittle and noncompounding. In the context of agents, this suggests a shift in focus: rather than optimizing for current model behavior, we should identify invariant components — design principles that remain effective across model upgrades, benchmarks, and environments. To identify such invariants, we focus on the model-harness interface — the boundary where model outputs are interpreted and executed and where execution outcomes are communicated back to the model. This interface is the primary locus of failure when agent performance degrades across settings. From this perspective, two fundamental questions emerge: Does the harness understand what the model intends to do? Is the model clear about how the harness interpreted its actions? These questions define the core alignment problem between model and harness and characterize the failure modes we analyze in the following sections. Tool-interface failures We consider the case in which the agent’s goal is code generation. Our agent primarily uses a bash tool, which provides access to the computer terminal (for example, to execute code), and a file editor to revise code. The bash tool is extremely powerful and can consume all the atomic operations of reading, searching, and editing. We make a simple enhancement to manage its outputs when they get too long. Naïvely truncating the output does not work well because the end of a command execution confirmation carries useful information such as job status and command success/failure. Instead, we contain the response length by condensing content in the middle and keeping only a limited number of lines at the beginning and the end. For reasons of efficiency and better corner-case handling in editing, we use file-editing tools in addition to bash. Our file editor is based on a string-replace mechanism that replaces existing file content with new (model-provided) content to produce edits. While string-replace works well in many cases, we repeatedly observed failure modes that expose the intent-execution gap: the model may have a clear intention, but the harness may not have enough information to execute that intention safely. In these cases, a naïve editor does not merely underperform; it can actively damage the working state by applying the wrong edit with high confidence. The first failure mode arises when the context of the model’s proposed edit appears at multiple locations in the codebase. From the model’s perspective, the requested edit may be unambiguous, because it is reasoning about a specific function, block, or error location. But if the harness receives only a raw “replace old text with new text” request, and the old text occurs several times, it cannot reliably infer which occurrence was intended. Naïvely replacing all matches is dangerous. In practice, the safer behavior is for the harness to alert the model of the ambiguity and request clarification — for example, by asking it to expand the current context such that the text to be replaced is unique. This is a small implementation detail, but it sharply improves faithfulness between intended and executed edits. A second failure mode appears when the model proposes only partial lines or short fragments for replacement. Partial-text matching is attractive because it is flexible, but it is also brittle: the same fragment may appear inside comments, string literals, neighboring expressions, or unrelated code paths. Even when the fragment is unique, replacing text that does not constitute a full logical unit — a complete line or well-bounded span — can produce malformed edits. These may be syntactically correct from the editor’s point of view but semantically unintended from the model’s point of view. We found that requiring stronger text anchors — such as exact line spans, richer surrounding context, or line-aware matching — substantially reduces these accidental edits. Put differently, the harness should not execute underspecified edit requests by guessing. Third, even when an edit is applied successfully, simply returning “edit succeeded” leaves the model underinformed about what the harness changed. This weakens the reverse side of the interaction loop: not only should the model express intent clearly, but it should also be able to verify how that intent was interpreted. To close this loop, we found it useful, after every successful edit, to supply the model with a diff file — a text file indicating what additions and deletions had been made and what text stayed the same. A diff serves as an immediate confirmation channel: the model can inspect whether the replacement landed in the correct location, whether collateral lines changed, and whether follow-up edits are needed. This seemingly minor feedback mechanism improves reliability because it converts editing from a fire-and-forget action into an observable state transition. A natural question arises: if the diff is provided after a successful edit, why do the first two failure modes require special handling? While the diff does expose unintended changes, it does so after the mistake has already been applied. At that point, the model must decide whether to roll back, repair the unintended edits, or continue execution with a potentially corrupted state. This introduces additional branching in the agent’s trajectory and forces it to spend tokens and reasoning effort correcting avoidable errors, rather than progressing toward the solution. In other words, every correction step injects additional information into the model’s context window. Note that every piece of information competes for the agent’s attention for next-action generation. Unrelated or unintended edits do not just waste tokens; they actively degrade performance by introducing spurious patterns and relationships, increasing the likelihood that the model forms incorrect associations and drifts away from the original goal. In contrast, addressing ambiguity and weak anchoring before execution ensures that edits are applied correctly in the first place. This reduces unnecessary exploration, prevents cascading errors, and keeps the context focused on task-relevant signals. In effect, the first two failure modes improve correctness at the point of action, while diff feedback improves observability after action. Both are necessary, but they operate at fundamentally different stages of the interaction loop. Reasoning A less obvious but equally important design consideration is how agents balance internal reasoning with external interactions. Chain-of-thought reasoning is clearly valuable. It allows the model to decompose a problem, plan next steps, and decide which tool to invoke. Without sufficient reasoning, tool usage becomes reactive, leading to shallow exploration, redundant calls, or poor sequencing of actions. However, excessive thinking introduces its own failure mode. When the model spends too long reasoning internally, it begins to form assumptions about the environment rather than verifying them. These assumptions may appear coherent within the model’s internal state, but they are often misaligned with the actual system state. As a result, the agent may issue poorly grounded tool calls or skip necessary validation steps altogether, creating a fundamental tension. Effective agents must continuously reconcile these two demands, and we refer to this balance as tool calling with a reasoning nudge. The idea is to encourage the model to perform just enough reasoning to decide the next action and then prioritize evidence-gathering interactions with the environment over further reasoning. Rather than extending internal chains of thought, the agent is nudged toward validating its hypotheses through tool outputs. In practice, we did not find a single “golden prompt” that reliably balances reasoning and tool interaction across all model families. For the Claude variants, we found that introducing quantitative guidance — e.g., “make 50+ tool calls” or “ideal tool call count is 100” — helps break long reasoning chains and pushes the model toward interacting with the environment. While the exact number of target tool calls is not important, it serves as a useful north star that biases the model toward action. However, in our experiments, this strong nudge was ineffective for other families, such as Gemini and Grok, which often interpret such instructions literally and make empty tool calls in order to meet the target. Such behavior reduces agent quality. Here, we find that using a flexible nudge like “You should use tools as much as possible” works just fine. The principle remains the same: we need to nudge the model to proactively use tools along with right amount of reasoning. Tool use preferences Across agents, tools function in exactly the same way, but models tend to exhibit distinct preferences in how they invoke them. For example, GPT models prefer to update code by using an apply_patch command to splice in text from a separate file, formatted in a particular way; denying them their formatting preferences hurts performance. Similarly, for Grok-4.20, a single monolithic tool for editing and viewing creates confusion, which leads to incorrect tool calls. Splitting functionality into atomic operations yields better results — even when the functionality remains unchanged. Additionally, viewing line numbers in a file helps most models, but Grok’s tokenizer and attention mechanism appeared less robust at separating prefixes from line numbers, and disabling this feature helps the view tool. These preferences are a by-product of training. This reinforces a broader design principle: agent performance is a function of not only what tools are available but how naturally those tools align with the model’s learned behaviors. A well-designed harness meets the model where it is, adapting interfaces, feedback, and interaction patterns to its strengths while still enforcing the invariants needed for reliable execution. Benchmarking study SSA is a simple harness that implements many of the principles we describe above. We evaluated it on three agentic benchmarks — SWE-Bench-Verified (n = 500), SWE-Bench-Pro (public set, n = 731) and Terminal-Bench-2 (n = 89). Each example in SWE-Bench-Verified and SWE-Bench-Pro is an open-source code repository and an “issue” to be fixed by making a code change. Terminal-Bench-2 tackles a range of programming tasks (software engineering, machine learning, security, etc.) but is not tied to a code repository. All three benchmarks have individual, static, prewritten tests for evaluating generated code. In SWE-Bench-Verified and SWE-Bench-Pro, the runs and evaluations occur in separate container images, meaning changes must be transferred into a different evaluation environment; in Terminal-Bench-2, the evaluation happens in the same container. Therefore, in SWE problems, it may be necessary to exclude irrelevant artifacts to not overly bloat the diff patch. Additionally, Terminal-Bench-2 imposes computational and agent-runtime limits that the SWE benchmarks do not. We evaluate our SSA agents using metrics standard in the field. Note that the mini-swe-agent results reported above in the SWE-Bench-Verified graph and the Terminus results reported in the Terminal-Bench-2 graph correspond to a fixed agent configuration per benchmark — the exact same prompts, tool specifications, and structural output instructions. As we discuss above, however, different model families require different reasoning nudges and exhibit distinct preferences for tool use. As a result, while SSA’s core harness remains identical, there are minimal but nonzero differences in prompts and tool specifications across model families (e.g., Claude, Gemini, GPT, Grok). Our goal in building SSA was not to optimize separate agents per model but to identify minimal, orthogonal adaptations that allow different model families to express their strongest capabilities within a shared harness framework. Terminal-Bench-2 Unlike SWE-Bench-Verified and SWE-Bench-Pro, the Terminal-Bench-2 dataset restricts the agent’s environment by limiting computational capacity (memory, storage, number of CPUs) and time (both agent and verifier run times) per project. While this is effective in limiting disproportionate use of computational resources to boost benchmark scores, it does have the unintended side effect of making the benchmark more sensitive to infrastructure choices. We observed that, given those restrictions, the following system characteristics have the most impact: Reliability of the inference backend. The inference backend’s capacity (tokens per minute and requests per minute) should be able to support all concurrently run projects for the full duration of the evaluation. High variance in invoker latency, frequent API timeouts, and retries eat into the allowed time budget, leading to more timeouts and a lower resolution rate. The number of concurrent projects run on a single node. This affects the network bandwidth available to each project. One of the first steps for an agent in Terminal-Bench-2 is to install dependencies (popular libraries like pip, torch, transformers, etc.). If the evaluation infrastructure is set up in such a way that multiple projects are run on a single node (e.g., Harbor with n_concurrent > 1), the available network bandwidth for each node is shared across all the concurrent projects. This increases the download times for dependencies, leaving the agent with less time for problem solving and a higher risk of getting interrupted before it’s done. Since the majority of tool calls involve command-line instructions, a natural way to address timeouts is to introduce a batch interface, allowing the agent to execute multiple commands in a single turn, rather than executing them sequentially. In our experiments, however, the results of this approach were mixed and correspond to one of the failure modes we describe above — the balance between reasoning and tool interaction. While batching reduces interaction overhead, it also requires the model to maintain a coherent terminal state across multiple steps, which increases reasoning complexity. For Claude models, the time taken by additional autoregressive reasoning tends to offset the gains from batching. In contrast, for other model families (such as Gemini and Grok), batch execution was beneficial, as it did not trigger additional reasoning. Overall, under constrained settings, batching commands does not consistently improve performance across all models. Given that evaluations are sensitive to such confounding factors, we next assess the upper-bound potential of the agent-model combination by relaxing time constraints. Specifically, we compare SSA’s performance on Terminal-Bench-2 under constrained settings (as shown above) and unconstrained settings, where memory and agent timeouts are removed. The unconstrained setup serves as an estimate of the achievable performance ceiling. The gap in accuracy between the constrained and unconstrained evaluations is typically 5-10%. We note that in our experiments, out of the 89 total projects in Terminal-Bench-2, a few consistently have a high timeout rate in the constrained evaluation but a high solve rate in the unconstrained setting. Those projects are make-doom-for-mips, torch-pipeline-parallelism, gpt2-codegolf, caffe-cifar-10, and train-fasttext. Experimental methodology We evaluate SSA across multiple agent benchmarks under a controlled and reproducible setup. All experiments were conducted on an AWS PCS cluster using c7.48xlarge instances, with maximum concurrency set to 10 to balance throughput and system stability. For model access, Claude models were served via Amazon Bedrock (production capacity), while OpenAI, Gemini, and Grok models were accessed through their respective commercial APIs. We enforced strict evaluation hygiene. Internet access was disabled for SWE-Bench-Verified and SWE-Bench-Pro runs, while it was enabled for Terminal-Bench 2 due to its benchmark design. For SWE-Bench-Verified and SWE-Bench-Pro, we used the standard benchmarking Docker environments, which include repository state up to the point of the current code revision. This allows agents access to the relevant history of the codebase while ensuring no access to future revisions. Evaluation-specific issues In SWE-Bench-Verified, instances such as astropy-8872 and astropy-8707 fail even with flawless code patches due to setup inconsistencies and require fixes in the evaluation environment. Additionally, some psf_requests instances can fail intermittently due to external test dependencies (e.g., nonresponsive URLs), requiring manual patching for reliable evaluation. For SWE-Bench-Pro, evaluations were executed on Amazon ECS. Due to environment-specific assumptions, a small subset of tests — 3 out of 731 instances — consistently fail when run on AWS infrastructure, resulting in an approximate 0.41% ceiling loss across all SSA evaluations. Finally, to minimize information leakage during agent runs in Terminal-Bench-2, hidden tests are introduced into the Docker environment only after the agent has completed its execution, ensuring that the agent has no direct access to them during problem solving. Note that internet access in Terminal-Bench 2 does introduce a possibility of solution leakage, but a manual review of trajectories didn’t reveal any instances of the model trying to copy solutions. Model configs To ensure reproducibility, we used public documented configurations from release/model cards wherever available. Specifically, Claude Opus 4.6 and Claude Sonnet 4.6 were used with adaptive thinking and max effort across all benchmarks (except when Sonnet 4.6 was tested on Terminal-Bench-2 with thinking disabled). Opus 4.5 used high effort and no thinking across all benchmark runs (except in Terminal-Bench-2, where Opus 4.5 has thinking enabled with 128k budget tokens). Sonnet 4.5 was used with an interleaved-thinking budget of 200k, Haiku 4.5 with a 128k budget, and Sonnet 4.0 with a 200k budget across all runs. Both Gemini 3.0 Flash and Gemini 3.1 Pro used thinking_level high and temperature 1.0 across all runs. Every GPT model used reasoning effort xhigh for all benchmarking runs. With Grok, we used the grok-4.20 reasoning variant for all runs with default configs. Detailed config files for every experiment are included in the SSA package. Conclusion We show that bridging the intent and execution gap in agent harnesses is critical to extracting state-of-the-art performance out of frontier models. Well-chosen editing tools, feedback from tool application, and management of tool-output lengths improve performance across all model families. On the other hand, models exhibit distinct preferences for different tool interfaces, and an effective harness should leverage them instead of trying to uniformly impose the same interfaces across all model families. We open-source all elements of our harness — the agent logic, tools, and prompts, as well as model configs, for easy reproducibility in the SSA package. Acknowledgments: Luke Huan and Anoop Deoras

Today, the key challenge in AI isn’t only how to build better models; it’s how to build evaluation systems that can keep up. Search-augmented AI systems can now produce deep research reports — long, polished syntheses of many sources that increasingly resemble expert analysis. But those reports are useful only if their claims are supported by the underlying literature. Most existing fact-checking tools work best when a claim can be matched to a short quote or a single document. But in AI-generated research reports, a single sentence may combine evidence from several sources. It can depend on the surrounding report for context, and it might compare assertions in a way that no single source does on its own. When Amazon’s Artificial General Intelligence (AGI) group started working on the problem of evaluating AI-generated research reports, we thought that the main technical challenge would be building a stronger AI fact checker. But before you can evaluate an AI fact checker, you need a benchmark, a standardized test set used to measure performance. And in this setting, building the benchmark turned out to be at least as hard as building the model. Traditionally, we view the ground truth for a problem as a fixed dataset. But we discovered that to evaluate complex AI properly, ground truth has to become a process. We call that process audit-then-score, and we present it, together with two accompanying datasets, in a paper we recently published to arXiv. When static datasets break down In the standard method for measuring AI performance, human experts label examples, those labels become the “ground truth” (the undisputed correct answers), and models are scored against them. To test this approach with AI-generated research reports, we recruited PhD-level specialists from fields such as computer science, control theory, education, public health, and environmental engineering. We asked them to verify claims from reports in their own specialties, mixing in a hidden set of claims whose answers we already knew. The result was sobering. In a controlled study, unassisted experts achieved only 60.8% accuracy on the hidden set of known answers. The issue was not a lack of expertise. It was that assessing deep-research factuality is an unusually demanding task. Verifying a single claim can require long-context reading, cross-document synthesis, and sustained attention. Normally, in machine learning, when a model disagrees with a benchmark, we assume the model made a mistake. But we realized that, in cognitively demanding tasks like deep research, disagreement should not automatically be treated as a model failure. Sometimes, a model’s “error” is actually a signal that the benchmark itself is ambiguous, incomplete, or wrong. Audit, then score Instead of treating the initial expert labels as unquestionable ground truth, we decided to use the models to actively scrutinize the benchmark. This is the core idea behind the audit-then-score protocol. Our paper introduces the protocol alongside DeepFact-Bench, a shared test set for comparing systems, and DeepFact-Eval, a system that checks whether literature supports report claims. Here is how the protocol works: When our AI fact checker disagrees with the current benchmark answer, it is not simply penalized. Instead, it acts as a challenger and must submit concrete evidence and a written rationale for why it thinks the original human answer is wrong. An auditor — which can be a human expert — then steps in. Crucially, auditors do not start from scratch; they compare the challenger’s new evidence directly against the benchmark’s original rationale. If the challenger makes the stronger case, we revise the benchmark before we score the model. DeepFact-Eval reads the full report context, plans searches to cover the relevant literature, summarizes retrieved documents, and asks follow-up questions when key details are missing. It then produces both a verdict and a written explanation. This fundamentally changes what a benchmark is. A new role for human expertise One of the most striking things we found is that the same experts who were unreliable as one-shot labelers became far more reliable when placed in the role of auditor. Across four rounds of audit-then-score, accuracy on our hidden test set rose from 60.8% to 90.9%. When experts start from a blank page, they have to find the evidence, interpret it, and make a judgment on their own; when they audit a disputed claim, they can focus on comparing two concrete cases. This shift had significant impact. On DeepFact-Bench, DeepFact-Eval reached 83.4% accuracy when we used GPT-4.1 as the underlying model. That was higher than the 58.5% of the best traditional fact-checking system we tested and the 69.1% of a strong prior deep-research system. Evaluation as an evolving infrastructure This shift has implications beyond one paper or one task. If AI systems continue improving, to the point that they exhibit humanlike expertise, the community will increasingly run into settings where evaluation based on one-time human answers is not enough. In those settings, sustaining benchmark quality may require auditing, revision, calibration, and periodic revalidation. Evaluation will become an ongoing collaboration among humans, models, and the evidence they surface together. Acknowledgments: Yukun Huang, Leonardo F. R. Ribeiro, Momchil Hardalov, Markus Dreyer

Routing in today’s data centers is usually governed by a data structure called a “fat tree”, which is similar to a corporate organizational chart, with nodes in each layer connecting to multiple nodes in the layer below. Here, however, the nodes of the bottom layer represent routers that want to send messages to each other, and the layers above them contain extra routers that simplify the routing procedure. A message sent by one bottom-layer router climbs the tree until it reaches the branch that leads to the destination router, and then it is sent down. This design is easy to implement but inefficient: the extra layers of routers add overhead, and routers at the top of the tree are prone to congestion. The fat-tree structure is also fragile, since the loss of a single router can cut off large regions of the tree. Theoretically, the best alternative is a “flat” network, in which the routers connect directly to each other. Ideally, one should connect the routers randomly, to maximize the diversity of routes through the network. But this is impractical, because calculating ad hoc paths through a random network is computationally intensive, and randomly connecting routers leads to data centers criss-crossed with wires. In a paper we recently posted to arXiv, we describe the first ever scalable flat-network datacenter. We introduce a “quasi-random” network topology that preserves many of the benefits of random connection and a passive optical component we call a ShuffleBox, which makes it practical to cable a flat network. The resulting network design — which we call RNG, for resilient network graphs — is now used in AWS data centers and is the default for most new builds globally. It uses 69% fewer routers, delivers up to 33% better throughput, and projects a 40% reduction in network equipment electricity consumption. The secret of randomness In the early 1990s, mathematicians showed that the optimal network for routing has a random topology, in which each router simply connects randomly to a few others. This is quite counterintuitive, but the overall network ends up having lots of different paths between all pairs of routers. Random networks also demonstrate excellent resilience, since no single router is more important than any other. The loss of 1% of routers results in a roughly 1% capacity loss. Degradation is proportional and predictable rather than catastrophic and concentrated. Networking researchers have also validated these results through simulations, showing that random, flat topologies achieve better performance than the corresponding fat trees. But these results couldn’t make it in the real world. Any network design comes with a “routing protocol” that decides how packets reach their destinations. In a random network, computing and implementing the right set of routing paths can take a lot of hardware resources — well beyond what is present in commodity routers. On the other hand, using dedicated hardware for routing would be cost prohibitive. An even bigger problem is that cabling routers randomly in a datacenter is completely infeasible. Our solution is to build a “quasi-random” network topology that has exactly the right mix of random and deterministic components. Routing without structure In a fat tree, the hierarchy itself tells packets where to go. And the paths generated are guaranteed to be the shortest possible. In a quasi-random graph, there is no obvious structure to exploit. Standard approaches to multipath routing in flat topologies typically require 20 to 80 times more memory than commodity hardware is equipped with. Our key insight is that we can exploit the random structure of the topology to open up a wide range of path options in a lightweight manner. Our routing algorithm, Spraypoint, has two components. The source router “sprays” its traffic randomly to all of its neighbors. Every (destination) router has some designated “waypoints” that feed traffic to it. The main scheme is that each data packet sent from the source goes to a random neighbor, after which the classic shortest-path algorithm routes it to a waypoint, and the waypoints feed it to the destination. The utility of spraying is that traffic can take a wide variety of paths to the destination, while the waypoints prevent traffic from congesting near the destination. In the implementation, we create various “rings” around each destination, and traffic is guided from each ring to a closer ring. By spraying to neighbors, Spraypoint provides nearly twice as many independent paths between routers as standard shortest-path routing techniques. This improves the likelihood that traffic will be routed around congested pathways or failed routers. Making quasi-random cabling practical A random graph connects arbitrary pairs of routers that may sit in different rooms, hundreds of meters apart. This is the strength of the topology, since it allows for fast communication between routers. But that is also its drawback, since cabling such a structure is extremely complicated. This is where our quasi-random solution comes in. Instead of all connections being random, we fix specific parts of the network topology. Our central innovation is a passive optical device called a ShuffleBox. It has router-facing ports on one side and connects to other ShuffleBoxes on the other side. The internal wires are shuffled according to a special pattern, so that random connections between the ShuffleBoxes lead to an overall quasi-random topology. When a new rack arrives, a technician plugs its router into an available port on the local ShuffleBox. No rewiring elsewhere. The physical-cabling complexity, the number of cable runs, and the installation process are on par with those of a fat tree, even though the logical topology is quasi-random. Predicting performance before construction With any new network topology, operators need confidence that it will meet capacity and performance requirements before they commit to construction. Fat-tree topologies come with simple, well-defined models that predict performance and capacity constraints. No equivalent existed for quasi-random graphs. We developed new mathematical models for various network statistics, such as path lengths, the number of routes, and how much traffic will end up on a particular link. These models give precise formulas that network operators can use to choose design parameters. We validated those models extensively, using 530 processor-years of simulation, the equivalent of running a single CPU for half a millennium, executed on Amazon EC2. An operator can now specify a server count and a target performance level, compute the cheapest compliant topology, and be confident that it will work. From theory to production The first quasi-random network went live near Dublin, Ireland, at the end of 2024, carrying real production traffic. We validated performance against the mathematical predictions, identified operational refinements, and applied them in two additional deployments. In end-to-end benchmarks across these production fabrics, our flat topology matched fat-tree performance for multipath-transport workloads and latency-sensitive storage operations. No customer workload changes were required, and the network operates transparently beneath existing applications. By April 2026, quasi-random wiring became the default architecture for most new AWS data centers globally. The 69% reduction in the number of routers translates directly into reduced power, cooling, and operational overhead at every site. For customers, it means more resilient infrastructure behind every API call, database query, and machine learning training job, without changing a single line of code.

Amazon Research Awards (ARA) provides unrestricted funds and AWS Promotional Credits to academic researchers investigating various research topics in multiple disciplines. This cycle, ARA received many excellent research proposals from across the world and today is publicly announcing 70 award recipients who represent 49 universities in 11 countries. This announcement includes awards funded under 6 calls for proposals during the fall 2025 cycle: AI for Information Security, Agentic AI , Automated Reasoning, AWS Cryptography, Cybersecurity and Anti-Abuse Technologies, and Sustainability Proposals were reviewed for the quality of their scientific content and their potential to impact both the research community and society. Additionally, Amazon encourages the publication of research results, presentations of research at Amazon offices worldwide, and the release of related code under open-source licenses. Recipients have access to more than 700 Amazon public datasets and can utilize AWS AI/ML services and tools through their AWS Promotional Credits. Recipients also are assigned an Amazon research contact who offers consultation and advice, along with opportunities to participate in Amazon events and training sessions. "Fraud and abuse evolve at the speed of the technologies that bad actors exploit. Since we can only defend against what we can measure, the science of studying those technologies has to keep pace," said Dhruv Kuchhal, Applied Scientist, Special Projects & Invest-Fixed. "Through ARA, we bring together experts across industry and academia to tackle these problems upstream and publish defenses that systematically raise bad actors' operating costs and erode their ROI as they spread across the ecosystem. This not only strengthens Amazon, but the broader Web, including online shopping customers, sellers and brands who build businesses online, and the platforms and payment rails that tie them together. We were impressed by the quality and volume of proposals we received — a strong signal that the field is raising the bar for Web users everywhere — and we look forward to working with the new recipients to turn this research into lasting, ecosystem-wide improvements in fraud and abuse prevention." “AI is reshaping cybersecurity faster than ever in advancing how we detect threats and defend systems, ”said Wei Ding, Applied Science Manager, GuardDuty, AWS. “At the same time, agentic AI requires stronger guarantees of safety, robustness, and trust worthiness. Since 2020, our team has funded security research that solves some of the biggest challenges for the industry. We’re pleased to continue our tradition of fostering innovation through these latest research projects addressing agentic AI security, AI-powered incident response, and threat detection in agentic AI systems and cloud environments, among other exciting areas.” ARA funds proposals throughout the year in a variety of research areas. Applicants are encouraged to visit our call for proposals page for more information or send an email to be notified of future open calls. The tables below list, in alphabetical order by last name, fall 2025 cycle call-for-proposal recipients, sorted by research AI for Information Security RecipientUniversityResearch titlePeng GaoVirginia Polytechnic Institute and State UniversityCortexCTI: A Unified Threat Intelligence Engine for Knowledge-Driven Cloud Threat Detection and ResponseGuofei GuTexas A&M UniversityNew Benchmark and Defense on Prompt Injection in Agentic AI SystemsXiyang HuArizona State UniversitySecuring Agentic AI: From Local Detection to Global AssuranceAdriana SejfiaThe University of EdinburghExploit-driven AI Agents for vulnerability detection verificationYue ZhaoUniversity of Southern CaliforniaSecuring Agentic AI: From Local Detection to Global Assurance Automated Reasoning RecipientUniversityResearch titleJonathan AldrichCarnegie Mellon UniversityA Visual Debugger for Program VerificationDalal AlrajehImperial College LondonSOLAR: Symbolic Learning for Automated Requirements ConsistencyMaria Paola BonacinaUniversity of VeronaNew Data Structure Theories and Quantifiers in CDSATJason CongUniversity of California Los AngelesBreaking the Parallelism Limit with SAT-solving AcceleratorsLucas CordeiroThe University of ManchesterCombining Formal Methods with Large Language Models in ESBMC: Enabling Automated Program Verification through AI/MLWerner DietlUniversity of WaterlooStrata-Sphere: Expressive Type Systems and Language FormalizationsKatalin FazekasTU WienPASSAT: Improved Passing of Assertion Stacks to SAT in Incremental SMT SolversSicun GaoUniversity of California San DiegoEvaluating and Improving Quantitative Reasoning in LLM Agents Using Sandbox Coding Tasks and Formal ToolsMilos GligoricThe University of Texas at AustinDocumenting and Recommending Tactics in HOL LightRonghui GuColumbia University in the City of New YorkScaling Formal Verification of Security Properties for Unmodified System SoftwareTyler JosephsonUniversity of Maryland Baltimore CountyAutoformalization for Scientific Computing in LeanJunyi Jessy LiThe University of Texas at AustinDocumenting and Recommending Tactics in HOL LightXiaorui LiuNorth Carolina State UniversityNeurosymbolic LLM Reasoning with Symbolical Soundness and Logical ConsistencyAzalea RaadImperial College LondonSoteria in Lean: Mechanising the Next Generation of Symbolic Execution ToolsDominik SchreiberKarlsruhe Institute of TechnologyResource-Efficient Flexible SAT Solving in HPC and Cloud EnvironmentsIlya SergeyNational University of SingaporeLinear Types for a Foundational Multi-Modal Program VerifierPeter SewellUniversity of CambridgeGradual Lightweight Methods for High-Assurance Cloud InfrastructurePaulo ShakarianSyracuse UniversityNon-Markovian Agentic Meta-ReasoningArmando Solar-LezamaMassachusetts Institute of TechnologySynthesizing Library Models for Static Analysis via LLMs and Conformance TestingSalil VadhanHarvard UniversityTranslating Formal Proofs of Differential Privacy via LLMsNickolai ZeldovichMassachusetts Institute of TechnologyVerifying Rust distributed system implementations using monotonic ownership state machines in VerusXuezhou ZhangBoston UniversityAuto-Formalization and Informalization through Two-Stage Reinforcement LearningTianyi ZhangPurdue UniversityScaling Interprocedural Data-Flow Analysis with LLMs AWS Agentic AI RecipientUniversityResearch titleRaman AroraJohns Hopkins University Multi-Party Differential Privacy: Unlocking Enterprise Agentic AI Fanglin CheWorcester Polytechnic InstituteAutonomous Catalyst Design with Agentic AI for Hydrogen ProductionMuhao ChenUniversity of California DavisFlowGuard: Evolutionary Red-Teaming for Safe Multimodal Web AgentsIoannis DemertzisUniversity of California Santa CruzCAMEO: Confidential Agentic Multi-component Enclave OrchestrationCaiwen DingUniversity of Minnesota Twin CitiesEnd-to-End Agentic AI for Scalable Chiplet Design with Extreme Parallelism and HeterogeneityAriel FelnerBen-Gurion University of the NegevMulti-Agent Pathfinding with Unassigned AgentsZhaomiao GuoThe University of Texas at AustinFrom Observation to Intervention: Counterfactual Multi-Agent World Models for Autonomous DrivingJiangen HeThe University of Tennessee-KnoxvilleBeyond Walls of Text: Building UI-Native LLM Agents as the Next Gateway to the InternetFan LaiUniversity of Illinois at Urbana-ChampaignReinforcing Coordination: Streaming, Exploration, and Distillation for Long-Horizon Agent LearningZiyang LiJohns Hopkins UniversityA Protocol Stack for Resource-Bound Multi-Agent AIHenry LiuUniversity of MichiganAutomating Large Scale Deployment of Infrastructure-based Safety Critical Event Detection with Agentic AIBryan Low Kian HsangNational University of SingaporeSelf-Configurable Agentic Learning via Co-optimizationChinmay MaheshwariJohns Hopkins UniversityMarkov Near-Potential Function Based MARL Training for Mixed Cooperative–Competitive Agentic AIArash NoshadravanTexas A&M UniversityA Retrieval-Augmented Dual-Attention Vision Framework for Standards-Aligned Infrastructure InspectionMuhammad ShafiqueNew York University Abu DhabiAVAAS – Automated Vulnerability Analysis Through Advanced Agentic SystemsRoni SternBen-Gurion University of the NegevMulti-Agent Pathfinding with Unassigned Agents Zhengzhong TuTexas A&M UniversityFlowGuard: Evolutionary Red-Teaming for Safe Multimodal Web AgentsLu WangUniversity of MichiganBenchmarking and Monitoring Multi-Agent SchemingYuke WangRice UniversityEmpowering Multimodal AI Agents with Continuous LearningHamed ZamaniUniversity of Massachusetts AmherstA Framework for Proactive and Collaborative AI AgentsYang ZhaoUniversity of Minnesota Twin CitiesEnd-to-End Agentic AI for Scalable Chiplet Design with Extreme Parallelism and HeterogeneityVictor ZhongUniversity of WaterlooKNOWLEDGESTORE: A Dynamic Hierarchical Memory for Scalable, Enterprise-Ready AI Agents on AWS AWS Cryptography RecipientUniversityResearch titleSri AravindaKrishnan ThyagarajanThe University of SydneyEfficient Robust Post-Quantum Distributed Key Generation and Threshold SignaturesDaniel J. BernsteinUniversity of Illinois at ChicagoFormally verified symmetric cryptographyJeremiah BlockiPurdue UniversityStronger Memory Hard Functions to Protect Passwords against Brute Force AttacksGeoffroy CouteauParis Cité UniversityPseudorandom Correlations for Threshold CryptographyYevgeniy DodisNew York UniversityMachine Unlearning and Computational Assumptions for AIZhengzhong JinNortheastern University - United States of AmericaPractical Watermarking for LLMs via Pseduorandom CodesYael KalaiMassachusetts Institute of TechnologyEnhancing AI Safety Using CryptographyJohn LiagourisBoston UniversityPushing secure MPC beyond niche applicationsRafail OstrovskyUniversity of California Los AngelesTowards Low-Latency Maliciously Secure MPC for LLMsRachel PlayerRoyal Holloway - University of LondonNew Approaches for the Linear Transform in BFV/BGVElaine ShiCarnegie Mellon UniversityPractical Secure Computation At ScaleAkshayaram SrinivasanUniversity of TorontoSimultaneous-Message and Succinct Secure ComputationDouglas StebilaUniversity of WaterlooFantASM: Fast, Auditable, and Neat AssemblyNi TrieuArizona State UniversityFuzzy Secure Computation for Real-World Noisy DataXiao WangNorthwestern University - United States of AmericaFrom Signing to Garbling: Exploring the Spectrum of Post-Quantum PrimitivesMark ZhandryStanford UniversityAlgorithms for Post-Quantum CryptographyJiaheng ZhangNational University of SingaporePractical Watermarking for LLMs via Pseduorandom CodesVassilis ZikasGeorgia Institute of TechnologyFuzzy Secure Computation for Real-World Noisy Data Cybersecurity and Anti-Abuse Technologies RecipientUniversityResearch titleGeoffrey VoelkerUniversity of California San DiegoDetecting Anti-detect Browsers at Scale Devices Sustainability RecipientUniversityResearch titleUdit GuptaCornell UniversityAgent-Driven Life Cycle Carbon Optimization for Sustainable Edge DevicesAdriana SchulzBrown UniversityIntegrating Sustainability Reasoning into Early-Stage Electronics Design

Large language models (LLMs) are pretrained on huge volumes of unlabeled data, but afterward, they’re typically post-trained on specific tasks such as instruction following, avoiding harmful outputs, and reasoning, or providing justifications for the outputs they generate. Parallel reasoning — in which multiple, diverse reasoning paths are generated and compared for the same problem — is emerging as a key tool for understanding the limits of LLMs’ reasoning capability. It also underpins techniques for testing LLMs such as self-consistency, where multiple reasoning paths are aggregated to improve accuracy. LLMs are generally optimized for reasoning through supervised fine-tuning (SFT), in which each training example is labeled with a single, human-verified reasoning trace. Given the usefulness of parallel reasoning for evaluation, the question naturally arises, Can we expand the limits of LLMs’ reasoning capacities by training them on diverse reasoning traces for each question? In a paper we presented at this year’s International Conference on Learning Representations (ICLR), we propose a method for doing just that, which avoids some previously identified pitfalls of parallel reasoning. To prompt a single LLM to adopt different reasoning strategies, we introduce a set of global forking tokens (such as s). The model then produces an answer conditioned on the sampled token, and the output is verified to obtain a reward signal (e.g., correct or incorrect). These rewards are converted into advantages, which are used to update the policy over forking tokens. Importantly, the generated reasoning traces are treated as rollouts: their gradients are detached and used only for computing rewards, not for direct optimization. By focusing optimization on the forking-token distribution, GFPO avoids the complexity of token-level reinforcement learning while still capturing the key decision — selecting the right reasoning mode upfront. This makes training both efficient and stable, while directly improving end-to-end performance. Together, SSFT and GFPO enable models to both learn diverse reasoning strategies and select the right one at inference time. Evaluation We evaluate SSFT+GFPO on both reasoning and coding benchmarks along two axes: (i) accuracy and (ii) diversity of reasoning. Across all settings, SSFT+GFPO consistently outperforms standard pipelines, such as SFT+GRPO. 58.80%64.22%52.07%AIME 2025 (Pass@1)AIME 2024 (Pass@1)LiveCodeBench-v5 (Pass@1)+6.84 vs. SFT+GRPO+5.37 vs. SFT+GRPO+4.94 vs. SFTBeyond accuracy, a key goal of SSFT is to address mode collapse. SSFT explicitly encourages specialization, allowing different tokens to represent distinct reasoning strategies. This leads to two important effects. First, each global forking token consistently triggers a distinct reasoning pattern. Second, this diversity improves pass@k without compromising pass@1. This contrasts with temperature-based sampling, where increasing diversity typically comes at the cost of accuracy. Below, we present a qualitative example illustrating our approach on a representative problem from the AIME 2025 benchmark, a challenging math reasoning dataset. The same question is solved using multiple qualitatively distinct strategies — such as algebraic manipulation, geometric reasoning, and case-based analysis — depending on the selected global forking token.), where each token indicates a different reasoning mode. During training, a bipartite matching step assigns traces to tokens for each question, encouraging the model to learn distinct behaviors rather than collapsing to a single pattern. The training objective sums the next-token prediction (NTP) losses across all matched pairs, evaluating each reasoning trace conditioned on its assigned control token. As a result, each forking token is specialized to a distinct reasoning strategy, and the model produces more diverse solutions — measured by pass@k, the probability that at least one of k generated answers is correct — while maintaining strong single-shot accuracy ( pass@1). Reinforcement learning While supervised training encourages the model to learn diverse reasoning strategies, it does not explicitly teach the model which strategy to use for a given question. Choosing the right reasoning mode is inherently a decision problem, making it a natural fit for reinforcement learning. We address this with global forking policy optimization (GFPO), a lightweight reinforcement learning approach that learns to select the most effective reasoning mode for each input. For a given question x, the model samples a global forking token from a distribution over control tokens (the through in the figure below) in the post-training phase, each intended to elicit a distinct reasoning mode. These tokens enable the model to generate diverse, high-quality reasoning paths for the same problem. However, naïve post-training strategies such as SFT can lead to mode collapse, where different reasoning tokens produce nearly identical behaviors. To address this, we propose set-supervised fine tuning (SSFT) — a simple and principled training approach that enables models to learn multiple distinct reasoning strategies from diverse supervision. Instead of representing reasoning with a single trace, SSFT models it as a set of complete solution paths, which arrive at the same answer through different strategies. To further teach the model which reasoning strategy to adopt in what contexts, we introduce a reinforcement learning paradigm we call global forking policy optimization. Between these two techniques, we observe gains of 5% to 7% in single-shot accuracy on standard benchmarks, indicating that improved reasoning-mode selection directly translates to better end-to-end performance. Supervised fine tuning In practice, multiple reasoning traces for the same question can be obtained by prompting multiple teacher models, sampling alternative reasoning paths from a single model, or aggregating solutions from heterogeneous sources. SSFT pairs each such trace with a dedicated forking token (e.g., through

Large language models (LLMs) keep getting bigger and better. But the cost of running them — generating text, answering questions, powering real-time applications — is scaling up, too. Obviously, model accuracy is important, but for real-time AI-based web applications, it can’t come at the expense of efficiency. In a paper we presented at the International Conference on Learning Representations (ICLR), we provide a framework for navigating this accuracy-versus-efficiency tradeoff, by connecting scaling laws directly to architectural-design decisions. The gap in current scaling laws In 2022, Google DeepMind announced the results of a study involving an experimental LLM called Chinchilla. The DeepMind researchers demonstrated a scaling law that enabled joint optimization of model size and training data to achieve a desired loss level, given a particular computational budget. More precisely, the law relates the model loss (L) to the number of model parameters (N) and the number of tokens in the training dataset: The other variables in this equation — E, A, B, α, and β — are all learnable coefficients. The DeepMind researchers did extensive experimentation to tune those coefficients. This "Chinchilla law" doesn't specify architectural choices, such as the size of the model's internal representations — the "hidden size" — or the relative number of parameters allocated to attention layers and multilayer perceptron (MLP) layers. However, two models, each with the same billion-parameter count, trained on the same data, with the same accuracy, can differ by up to 40% in inference-time throughput, depending on additional architectural choices. We set out to deduce scaling laws that can help predict those choices. The Transformer architecture The Transformer architecture — which lies at the heart of all LLMs — consists largely of stacked attention and MLP blocks. Attention blocks determine how much weight to give each prior token (word or word part) when updating the current token's representation; MLP blocks transform that representation further and are where much of the model's learned knowledge is stored. A separate output layer at the end of the stack converts the final representation into a probability distribution over the next token. The attention mechanism uses three matrices, with names borrowed from information retrieval: the query matrix encodes what each token is looking for in the rest of the sequence; the key matrix encodes what each token has to offer; and the value matrix holds the content each token can contribute when it's attended to. Comparing queries against keys tells the model how relevant each token is to each other token. Most LLMs use multihead attention: several attention computations run in parallel, each with its own query, key, and value projections. Different heads tend to specialize in different aspects of the input, letting the model capture a richer set of relationships than a single head would. Our approach: Architecture as a first-class variable In our ICLR paper, we introduce a scaling law that augments the Chinchilla framework with three architectural factors: the hidden size (the dimension of the vectors that flow through the embedding, attention, and MLP blocks); the ratio of the number of MLP parameters to the number of attention parameters; and grouped-query attention (GQA), in which groups of attention heads, while preserving distinct query matrices, share key and value matrices. Each factor has a direct impact on inference throughput: Hidden size (d_model): Under a fixed parameter budget, larger hidden sizes reduce total inference FLOPs and shrink the key-value cache, improving throughput. MLP-to-attention ratio (r_mlp/attn): A higher ratio allocates more parameters to the MLP and fewer to attention, shrinking the key-value cache and reducing memory-bandwidth bottlenecks. Grouped-query attention (GQA): Compressing key-value heads further cuts input/output costs during generation. Adjusting these factors purely for higher throughput comes at a cost of accuracy. Both hidden size and MLP-to-attention ratio exhibit U-shaped loss curves: there is an optimal point for each, and pushing too far in either direction has a negative effect on model accuracy. GQA has a more erratic effect on loss, so we treat it as a discrete hyperparameter tuned through local search. We deduce our scaling law in two stages. First, we fit the standard Chinchilla law to the model under investigation, calculating values for the coefficients E, A, B, α, and β. This establishes an optimal reference loss. Then we calibrate how each architectural choice — differences in the three factors we consider — affects that loss. Effectively, we learn a correction surface over the design space. Because the effects of hidden size and MLP-to-attention ratio on loss turn out to be separable, each factor can be optimized independently. Two model families: Panda and Surefire This scaling law enabled us to develop a search framework that identifies Pareto-optimal architectures for any given accuracy target. The result of that search was two model families: Panda (which maximizes accuracy) and Surefire (which is Pareto optimal on the accuracy–efficiency frontier). To validate the framework and identify our families of optimal models, we trained more than 200 models with varying architectures (80 million to three billion parameters, eight billion to 100 billion tokens). The results of our experiments are below (throughput measured on H200 GPU with batchsize-128-4096-input-1024-output tokens): Modeld_modelGQAr_mlp/attnLossAvg. accuracyThroughput vs. LLaMA-3.2-vLLMThroughput vs. LLaMA-3.2-SGLangLLaMA-3.2-1B204844.802.80354.9%baselinebaselinePanda-1B256041.072.78257.0%-33%-Surefire-1B256093.602.80455.4%+21%+47%LLaMA-3.2-3B307234.802.62561.9%baselinebaselinePanda-3B409631.002.61962.5%-23%-Surefire-3B409671.002.62062.6%+12%+17% The billion-parameter Panda model gains 2.1% over LLaMA-3.2-1B, and the three-billion parameter model gains 0.6% over LLaMA-3.2-3B — at the cost of lower throughput. Surefire models match or exceed LLaMA-3.2 accuracy while improving throughput by 12-47%, with gains reaching up to 42% on A100 (vLLM) and 47% on H200 (SGLang) under different model size and batch size configurations. Key takeaways Architecture is not an afterthought. The optimal MLP-to-attention ratio of LLaMA-3.2-style models is around 1.0, far lower than that of existing open-weight versions (e.g., 4.8 for LLaMA-3.2-1B). Current models overallocate to MLP layers. The right configurations of hidden size, MLP-to-attention ratio, and GQA configuration can unlock large efficiency gains with no accuracy cost. Small-scale experiments predict large-scale outcomes. The conditional scaling law, calibrated on models with as few as 80 million to 297 million parameters, reliably predicts the best architecture at one billion and three billion parameters, enabling low-cost exploration before expensive full-scale training. The framework generalizes across hardware and serving systems. Efficiency gains are consistent across A100/H200 GPUs and vLLM/SGLang, making the results directly actionable.

Large language models (LLMs) have become integral to enterprise applications across industries. Under the hood, customers’ inputs to the models are usually augmented with prompts that encode intricate business logic, regulatory requirements, and domain expertise: a healthcare system must use language compliant with the Health Insurance Portability and Accountability Act, for instance, and a financial trading system must follow risk tolerance rules. These prompts are typically crafted by domain experts over weeks or months. Yet business demands continue to push for further performance gains. The challenge, therefore, is not engineering prompts from scratch but rather elevating already strong performance by discovering nuanced, task-specific refinements — without compromising domain requirements. In this post, we present Promptimus, a method for automatically optimizing well-developed prompts that has several advantages over its predecessors: It's model agnostic: It takes a prompt already optimized for a source model, rapidly reoptimizes it for a target model, and compares the optimized prompts across models. It's driven by performance criteria: It takes the existing prompt template, task-specific data samples, and user-defined performance metrics and generates targeted improvement strategies, iterating repeatedly to achieve domain-specific optimization objectives. It focuses on exploits: It uses a metric-analyzer AI agent to identify failure points and a debugging helper agent to identify root causes, and it surgically refines prompts relative to failures (rather than along random dimensions) for targeted performance improvement. It’s fully automated: It analyzes user-defined metrics and uses a code sanitization AI agent to generate debugging checkpoints automatically. Metric functions can be imported as Python code, and performance criteria can be added or modified at any time. It has an edit mode: For large, carefully structured prompts with complex business logic, the edit mode makes surgical, targeted modifications instead of rewriting the entire prompt — preserving the parts that already work while fixing exactly what’s broken. Promptimus supports a wide range of textual and multimodal LLM tasks, including classification, extraction, generation, summarization, code generation, and tool use. In the following sections, we’ll present our methodology, the system architecture, and experimental results on multiple enterprise tasks. Why good prompts are hard to improve Attempts to automate prompt optimization are as old as prompt engineering itself, but approaches that work well when generating prompts from scratch struggle to improve well-engineered prompts. Random exploration strategies using generic directions like "be more creative" or "add examples" are ineffective, because the remaining improvements lie in very specific strategic directions. Sparse feedback in the form of scalar scores provides no guidance on why instances fail or how to improve. On top of growing complexity from business domain demands, rapid model evolution further compounds the challenge of prompt optimization. As providers like Anthropic, OpenAI, Google, Meta, and Alibaba release new models, enterprises face recurring prompt migration challenges. Prompts optimized for one model often underperform on another due to different instruction-following characteristics. Manual reoptimization is costly and time consuming, and regression risks delay adoption of better models. Methodology and system design Promptimus addresses these challenges with a methodology built around a four-step iteration loop, with the following inputs: the LLM you aim to use for inference the initial prompt template a small JSONL dataset (typically 20–50 samples) with corresponding variables for prompt templates, split into a development set (for prompt tuning) and a held-out test set (for validation); it is not mandatory for the samples to contain the ground truth a user-defined performance-evaluation metric function (you can bring your own Python code) The four-step iteration loop Step 1 — evaluation: During initialization, the original prompt is executed on the target LLM using the development set (dev set) to establish baseline evaluation scores. Additionally, the metric-analyzer agent performs analysis of the user-defined metric function, generating checkpoint functions that decompose the evaluation into intermediate validation steps. These checkpoints enable fine-grained failure diagnosis throughout the optimization process. For example, when the checkpoints reveal that 98% of outputs have the correct JSON format, and 95% have valid schemas, but only 88% have valid values, the cause of underperformance is localized to value validation. After the initial evaluation, Promptimus branches into either standard mode, where it conducts full prompt rewrites, or edit mode, where it modifies prompts with structured find-and-replace edits. Standard modeEdit modeStep 2Feedback generation: The LLM-driven feedback generator uses the metric checkpoints precomputed by the metric analyzer to diagnose failure patterns in the current-prompt results. It identifies the bottleneck checkpoint (the one with the lowest pass rate) and collects representative instances — including both failing and passing examples, to provide contrast — then analyzes root causes and common failure modes. Finally, it provides actionable suggestions for fixing the prompt (such as "model outputs descriptive text instead of enum codes, suggest adding explicit constraint").Analysis + strategy + edit generation: After performing the same failure analysis as in the standard mode, the feedback generator proposes targeted find-and-replace edits, pinning changes to the exact locations responsible for specific failures. Step 3Strategy + full rewrite: Based on the feedback from the previous step, along with the metrics and data samples, the metaoptimizer analyzes task characteristics and generates task-specific exploration strategies, while maintaining all domain-specific requirements encoded in the original prompt. Then, for each strategy, the instruction optimizer proposes an improved prompt candidate that addresses the identified weaknesses and specific error patterns. This one-to-one coupling between strategies and candidates ensures diverse exploration of the optimization landscape. Programmatic edit application: For each proposed edit in step 2, Promptimus deterministically matches the edit to the identified failure with three match levels: exact match, whitespace-normalized fuzzy match, and similarity match near line reference. This process has a 97.3% success rate with zero LLM calls.Step 4Candidate evaluation: Each candidate is executed using the dev set, and the best candidate is selected by running the user-defined metric function. The best-performing candidate becomes the starting point for the next iteration. This exploration-focused process runs iteratively for a user-specified number of iterations, with each iteration building on what was learned and achieved in the previous one.We recommend standard mode for short prompts that need significant expansion — for example, a two-line math prompt that needs to grow into detailed reasoning protocols. Edit mode is a better choice for longer and already well-crafted prompts containing structured content like API schemas, compliance rules, or domain taxonomies, where full rewrites risk silently dropping or reorganizing carefully crafted sections. For a prompt with 50,000–100,000 tokens, a typical iteration produces three to five edits totaling 500–1,000 tokens, versus regeneration of the entire prompt. More generally, Promptimus adds content only when the optimization loop surfaces unaddressed failure modes, so prompt length plateaus within the first few iterations. This means that the relative serving-time impact is small for already long production prompts and larger for short starter templates. If the optimized prompt is served as a cached system prompt, the additional cost is one call during the cache's time to live, which becomes negligible at scale. Empirical experiments and analysis We evaluated Promptimus against six leading automatic prompt optimization methods across 20 public benchmarks spanning reasoning, math, question answering, text-to-SQL, coding, function calling, instruction following, and multimodal tasks. All methods used the same optimizer model and evaluation budgets with Claude Sonnet 4.6 as the target model, averaged over five random seeds. Each benchmark used 20 dev samples for optimization and 100 held-out test examples for evaluation. As reported in the table below, Promptimus achieves the best result on 16 of 20 benchmarks and ties on one, outperforming all six baselines on average (0.792 vs. 0.765 for the best-of-six baseline). The largest gains appear on tasks where the metric has a decomposable structure. Notably, Promptimus with edit mode outperforms all four multimodal benchmarks, suggesting that vision-language prompts benefit from preserving existing visual-analysis structure rather than rewriting it. BenchmarkMetricNo optimizationBest of six baselinesPromptimusModeBBH-CausalJudgeAcc [0,1]0.5380.726 (GEPA)0.718StandardBBH-DisambigQAAcc [0,1]0.6010.868 (GPO)0.908StandardBBH-GeoShapesAcc [0,1]0.7470.770 (OPRO)0.936StandardBBH-RuinNamesAcc [0,1]0.9180.926 (GEPA)0.928StandardBBH-SnarksAcc [0,1]0.3240.920 (OPRO)0.908EditGSM8KAcc [0,1]0.6580.964 (MIPROv2)0.958StandardDAPO-AIMEAcc [0,1]0.7030.730 (ProTeGi)0.79StandardHotPotQAF1 [0,1]0.160.832 (MIPROv2)0.839StandardSpiderExAcc [0,1]0.680.846 (GEPA)0.85EditBIRDExAcc [0,1]0.6260.684 (ProTeGi)0.684StandardBigCodeBench-hardPass@1 [0,1]0.3390.336 (ProTeGi)0.345StandardCodeforcesPass@1 [0,1]0.5890.808 (TextGrad)0.818EditBFCLAST [0,1]0.8820.968 (MIPROv2)0.98StandardNesT-FuLPMacc [0,1]0.3750.429 (TextGrad)0.469StandardIFBenchAcc [0,1]0.4980.509 (GEPA)0.53StandardIFEvalStrict [0,1]0.8760.886 (GPO)0.892StandardMathVistaAcc [0,1]0.4330.606 (GPO)0.644EditChartQARelaxed Acc [0,1]0.2790.828 (ProTeGi)0.834EditAI2DAcc [0,1]0.8340.824 (MIPROv2)0.868EditDeFactifyAcc [0,1]0.8350.922 (MIPROv2)0.938EditAverage0.5950.7650.792The figure below shows convergence through iterations on two representative benchmarks. Promptimus edit mode reaches 90% of its final development score in a median of about 300 metric calls, faster than all baselines. Both modes typically plateau within eight iterations, with the bulk of improvement concentrated in the first three to five iterations. Importantly, dev set gains transfer to the held-out test set. Sometimes baselines match or even exceed Promptimus on dev but fall behind on test, indicating overfitting. We attribute this to edit mode's surgical modifications, which preserve generalizable prompt structure, and metric probing, which produces failure signals that transfer across examples, as opposed to memorization of dev-set patterns. We also evaluated Promptimus across multiple LLMs using a public benchmark and Amazon enterprise use cases, spanning the tasks of classification, text-to-SQL, math reasoning, coding, multimodal understanding, and complex API generation on seven target models. Promptimus improved baseline prompts on all nine tasks, with gains ranging from 3.18% to 90.27%. Dev sets ranged from 30 to 160 examples, with the majority of tasks using fewer than 100, demonstrating the system's sample efficiency. The results also highlight model-agnostic generalizability: the same optimization framework produced meaningful gains across both proprietary and open-source target models without task-specific engineering. TaskTarget LLMPerformance metricDev set sizeNo optimizationOptimizedComplex API call generationGPT-OSS-120BAPI Acc (user-defined) [0,1]430.450.86Classification_ANova ProF1 score and FPR score [0,1]2100.640.78Multimodal classification_BHaiku-4.5Accuracy [0,1]1600.510.76Classification_CNova LiteAccuracy [0,1]850.560.58Text2sql_ANova-MicroExecution Accuracy [0,1]500.720.83Math reasoning_AQwen3-235B[WS12] (non-reasoning)Accuracy (user-defined) [0,1]300.470.50Math reasoning_BClaude-4.5-Opus (non-reasoning)Accuracy (user-defined) [0,1]300.600.73Coding_AGPT-OSS-120BPass@1 [0,1]1000.260.33Coding_BGPT-OSS-120BPass@1 [0,1]310.560.64Following are examples of how Promptimus improved already fine-grained prompts to further drive application performance for a variety of use cases. Example 1: CodeForces (coding benchmark designed to evaluate LLM reasoning) This use case is to use an LLM to generate a Python function based on a user-provided problem description. We used 50 dev samples (sampled from the original dev set) and 148 test samples with a user-defined scoring approach. The Promptimus (edit mode) optimization converged in five iterations. Original vs. optimized prompt (deletions in italic, additions in bold)-When tackling complex reasoning tasks, you have access to the following -actions. Use them as needed to progress through your thought process. -[ASSESS] -[ADVANCE] -[VERIFY] -[SIMPLIFY] -[SYNTHESIZE] -[PIVOT] -[OUTPUT] -You should strictly follow the format below: -[ACTION NAME] -# Your action step 1 -# Your action step 2 -... -Next action: [NEXT ACTION NAME] +You are an expert competitive programmer. Solve the given programming +problem in Python using the strict 2-phase reasoning structure defined below. + ## ABSOLUTE RULE – ONE [OUTPUT] BLOCK ONLY – ZERO EXCEPTIONS + The first [OUTPUT] block encountered is the ONLY one evaluated. A second [OUTPUT] block causes + immediate evaluation failure and a score of 0. + ## CRITICAL CONSTRAINTS + Standard Library Only – Use ONLY Python standard library modules. No exceptions. + Forbidden: sortedcontainers, numpy, scipy, pandas. Allowed: bisect, heapq, collections, math, + itertools, functools, sys. + If you need a sorted structure: implement using bisect + a plain list. + Sorting Pitfall Warning: + Never use sort(reverse=True) when the secondary sort direction differs from the primary. + Descending by key A, ascending by key B: items.sort(key=lambda x: (-x[0], x[1])) + I /O Consistency Rule: + Use exactly ONE I/O method throughout – no mixing. + Strategy A: input = sys.stdin.readline at top, then use input() everywhere. + Strategy B: use sys.stdin.readline() directly everywhere. + Variable Initialization Rule: + Declare all variables that are conditionally assigned BEFORE their conditional block. + ## STRICT 2-PHASE STRUCTURE + ### PHASE 1 – [ASSESS] (ONE block only) + 5 mandatory gates (G1–G5). Each gate requires a one-line YES/NO + justification. + G1 – Brute force feasible? Is O(nˆ2) within time constraints? + G2 – All variables initialized before conditional use? + G3 – I/O strategy chosen and consistent? Declare exactly one strategy. + G4 – Demo output reproducible by hand? Perform explicit dry run on demo input. + G5 – Any mutable structure modified during iteration? Confirm index recomputation. + End with: Chosen approach: [algorithm name], O([complexity]) – Tier [1/2/3] + Tier 1 = Brute-force correct, Tier 2 = Optimized correct, Tier 3 = Optimal. + Fallback Rule: If you cannot confidently implement Tier 2+, commit to Tier 1. A slow, correct + solution scores higher than a fast, broken one. + ### PHASE 2 – [OUTPUT] (ONE block only, immediately after ASSESS) + First line inside [OUTPUT] must declare I/O strategy as a comment. + Produce the complete Python solution. No other action types permitted. + ## CRITICAL OUTPUT RULES + 1. Exactly ONE [OUTPUT] block. Fix mistakes inline – never open a second. + 2. Inside [OUTPUT], the ONLY content is the fenced Python code block. + 3. Reasoning word budget: entire [ASSESS] block must not exceed 250 words. + 4. No trailing empty lines in output. + 5. Never end your response with only reasoning – even brute-force is acceptable over no solution. + 6. Never output -1 or “no solution” if the problem guarantees a solution always exists. + [. . . mandatory code scaffold template with I/O strategy declaration, imports, solve() structure, sorting/mutation reminders, output + formatting rules . . . ] Title: {problem_title} Time Limit: {time_limit} Memory Limit: {memory_limit} Problem Description: {problem_description} Output Specification: {output_specification} Demo Input: {demo_input} Demo Output: {demo_output} Note: {demo_note} -Write Python code to solve the problem. Present the code in “‘python ... “‘ at the end. +Solve the problem using the 2-phase structure: [ASSESS] block (5 mandatory gates G1–G5, ≤250 words), +then [OUTPUT] block (fenced Python solution)Example 2: Multimodal AI agent This AI agent is for Amazon to detect construction defects. The original and optimized prompts are shown below. We used the vision-language model qwen3-vl-235b-a22b on Amazon Bedrock to examine the images taken by inspectors and identify construction defect categories and risk levels. The optimization process looped in three iterations with 16 dev samples. The recommendations generated by the metric analyzer and instruction optimizer in Promptimus (including providing a role, a task objective, defect categories with examples, a category disambiguation section, analysis instructions with a decision tree, output format requirements, and critical output requirements) improved the image classification accuracy from 0.438 to 0.812. When we applied the optimized prompt to the test sample set (17 samples), accuracy improved from 0.471 to 0.529. Example 3: Defactify (multimodal fact verification) This is a comprehensive framework for evaluating an LLM’s ability to perform multimodal fact verification, detect misinformation, and identify AI-generated content. The Promptimus metric analyzer found that the model defaults to ''Real'' for photorealistic AI-generated images. The optimizer introduces an adversarial dual-hypothesis framework with asymmetric weighting that biases the model toward “AI-generated”. For example, with the original prompt, the model dismisses a clock with garbled numbers as an “artistic design choice” and is fooled by photorealistic textures. After optimization, by contrast, the adversarial dual-hypothesis protocol forces systematic signal enumeration, catching the garbled clock numerals that the baseline dismissed. Conclusion and future work Compared to other metric-driven prompt optimization approaches, Promptimus excels at preventing exploitation through targeted and exploitation-focused refinements. It is fully generalizable, adaptive to user-defined metric functions and task domains without manual engineering. The dense feedback loop drives automatic analysis on metric-function code, identifies debugging checkpoints, and generates adaptive, task-aware exploration strategies that target the specific failure modes of each prompt-and-task combination. Particularly, our approach is sample efficient, requiring only a small number of dev examples (typically 20–50) to drive significant improvements, fitting it for enterprise scenarios where labeled data is scarce or expensive to obtain. Furthermore, its model-agnostic design enables it to rapidly adapt prompts to target models for seamless enterprise-level model migration. We are making this innovation available through Amazon Bedrock to enable model migration for enterprise generative-AI applications with zero manual engineering and minimal labeled datasets.

Before the "last mile" delivery driver sets off for your home, your Amazon item has moved through the middle-mile network of fulfillment centers and sort centers, which brings products close enough to customers to make our same-day or next-day shipping promises possible. For years, Amazon engineers and scientists have been pushing computational boundaries to optimize this network under uncertainty, and that push has accelerated as the network has grown more complex. What happens when a huge snowstorm closes major highways, a sort center is hit by a power outage, or demand for a viral product spikes? These headline disruptions get attention because they're obvious system shocks that vividly illustrate the challenge of planning for uncertainty. But the most important sources of uncertainty are far more subtle: the day-to-day variations in demand and travel times that, if you don't look closely enough, erode efficiency across the entire network. We've found that even when we consider just demand variability, optimizing for uncertainty promises potential savings of 0.5%. This is a small percentage, but we obsess over small percentages because real customer experiences lie behind them. And demand variability is just one piece of a puzzle that includes road delays, processing time fluctuations, and countless other microvariations. Months before a customer clicks "Buy Now", Amazon's logistics experts consider a multitude of middle-mile routing questions: What routes should trucks take between warehouses? When should shipments depart? Where should inventory be positioned to meet customer demand? The proactive shaping of the network's structure and timing is called network design. Our challenge is not to optimize for perfect conditions but rather to build plans that remain effective even when things don't go as expected. A computational puzzle of staggering complexity Even if we could count on perfect conditions, optimizing the middle-mile network is challenging because it requires coordinating tens of millions of different products moving through hundreds of facilities, each with limited capacity and specific operating hours. A key difficulty is the mix of optimization decisions involved. Some are a matter of degree (what volume of packages to send down a particular route). Others are binary (open this shipping lane or not; depart now or wait for more cargo). Put them together, and you get what’s called a mixed-integer optimization problem, a kind of problem where the solution strategies explode combinatorially in both computational time and memory space. Consider that with only 300 yes-or-no decisions, there are already more possible combinations than atoms in the observable universe. Amazon's network involves millions of such decisions, compounded by delivery windows that restrict when shipments can arrive or depart. State-of-the-art optimization software struggles to solve this problem, even with “perfect information”. In the real world, information is far from perfect, and a plan that looks optimal on paper can unravel when conditions change. The challenge of handling uncertainty Uncertainty shows up in two different ways. First, those day-to-day fluctuations in variables like demand or travel times. Second, the structural shocks: a weather-driven road closure or unexpected facility shutdown. In academic work, a common strategy is to model many scenarios the network might face and then "robustify" the solution so that it performs well across them. But at Amazon's scale, this approach founders. There is always a staggering number of things that can go wrong, and trying to robustify against each of them individually is a hopeless task. Instead of chasing an impossible guarantee, we shift to a more practical goal: optionality. Our aim is to design a system with enough alternative routes and workable options that day-to-day fluctuations and shocks trigger effective adaptation rather than crises. In practice, our sought-after flexibility requires designing candidate networks with built-in options and stress-testing those designs against many plausible futures. That’s where Amazon’s in-house computational tools come in. Making network design tractable Amazon’s network design tool makes the middle-mile-network problem solvable at scale. It starts with a simple insight: not every possible route is worth considering. If you were planning a road trip, you would naturally focus on a handful of sensible routes. The tool applies this principle by identifying possible “consolidation points”, such as sort centers where packages from multiple origins can share trucks to common destinations, and then finding efficient routes that use them. We must also respect the clock, because Amazon facilities run on precise operational schedules. For example, a sort center might accept inbound shipments from 2:00 a.m. to 6:00 a.m. and dispatch outbound trucks from 8:00 a.m. to 12:00 noon. Ideally, planners would model these schedules at fine resolution (say, 15-minute intervals), but this creates another explosion of possibilities. On the other hand, a coarse resolution of, say, 24-hour intervals would make for fast but useless planning: packages would arrive after a facility has closed for the night, and trucks would be scheduled to depart before loading their cargo. Amazon planners overcame this stubborn problem while still supporting operational reality. The optimization approach solves at a fairly coarse time resolution, but for each candidate route, it includes precomputed “timing bounds” — the latest feasible truck departure and earliest feasible arrival — with 15-minute precision. That way, when the tool chooses routes, it's choosing those that will work on real-world schedules. Risk-aware network adjustments at scale Even with these algorithmic advances, the solution to a single deterministic planning problem of Amazon’s scale can take hours to compute because of the difficulties of parallelizing the underlying algorithm. Adding uncertainty compounds the challenge. One naïve way to account for uncertainty on the middle-mile network would be to simplify the problem by assuming that more packages flow between locations that are large and close together. But the middle mile isn’t a set of independent pipes. Product flows interact. A spike in demand at one fulfillment center affects nearby facilities in particular ways; a new delivery station changes a region’s patterns. To better capture those complex dependencies, we developed an approach enabling risk-aware network design via Monte Carlo methods. Amazon's risk-aware network-design models start by creating many permutations of synthetic origin-destination flow data to represent both day-to-day fluctuations in demand as well as larger structural shocks. One critical component of the models is a graph attention network model that represents the middle-mile network as two interconnected graphs. The first is a site graph whose nodes represent fulfillment centers and delivery stations, with the edges representing both shipping routes and geographic proximity. This allows the model to learn spatial patterns, such as higher demand around dense population centers. The second graph works at a higher level: each node represents a specific origin-destination pair. This structure lets us see correlations too subtle for the site graph to capture. It is like understanding traffic patterns: knowing that two highways are close (site graph) doesn't tell you whether they compete for the same commuters (origin-destination graph). To illustrate, consider two nearby fulfillment centers in northern Connecticut, both serving New York City. A model using only the site graph might estimate that each facility sends 8,000 packages to NYC, when in reality the volumes are much lower because the two facilities share that demand. The site graph understands that the fulfillment centers are proximal, but it doesn't fully capture that their flows to NYC are interdependent. The origin-destination graph solves this by representing each facility-to-destination pair as its own node, allowing the model to learn that when two similar facilities serve the same area, their shipments are interdependent. More broadly, this structure lets the model discover that origin-destination pairs with similar characteristics — such as suburban fulfillment centers delivering to urban areas — may exhibit correlated demand, even when they are far apart. Armed with realistic demand scenarios that respect spatial correlations and understand how network disturbances propagate across space, we can generate candidate network designs that work well under a variety of demand conditions. Keeping delivery promises under uncertainty Because the models train on historical shipping data, we can generate realistic demand scenarios that respect spatial correlations. And crucially, because the tools understand how network disturbances propagate across space, we can produce plausible scenarios the network has never encountered before, such as demand shifts driven by a new facility opening or a major regional weather event. That’s the missing half of the loop: one product designs candidate future networks, while another generates the scenarios to stress-test them. So instead of optimizing a single forecast, Amazon planners can evaluate their network designs across hundreds of plausible scenarios and preserve the options that keep the network flexible in the face of uncertainty. Overall, this enables us to distinguish between network designs that appear efficient on average but are fragile under stress and those that may incur slightly higher steady-state costs yet deliver more-stable performance. For customers, this research translates into more-reliable delivery promises, including during peak shopping periods and genuine disruptions. By combining advanced optimization techniques with machine learning, Amazon is building a middle-mile network designed to adapt to the world as it really is. So when a winter storm buries a region under two feet of snow on the same day a new must-have product goes viral, the network can absorb the shock and recover as quickly as conditions allow. But the work of building resilience against uncertainty is not finished. As the network grows, so does our commitment to advancing the computational tools that keep delivery promises reliable, day after day.

When Amazon places a purchase order with a vendor, a deceptively simple question arises: how many units should go to which fulfillment center, and when? Amazon optimizes this decision based on its demand forecasts, inventory positions, and transportation costs. The vendor, meanwhile, has its own production schedules, warehouse locations, and shipping economics. Each side optimizes independently, and the result is often a plan that is suboptimal for both, resulting in higher costs for all. This is a classical problem in economics: “ coordination under asymmetric information”. Each party holds cost and capacity data the other cannot observe, yet their decisions are deeply intertwined. The theoretical tools for solving such problems have existed for decades, rooted in mechanism design, the branch of economics that asks whether transaction rules can be designed so that self-interested parties nonetheless produce an outcome that is good for everyone. Specifically, solutions to this problem tend to involve the Vickrey-Clarke-Groves (VCG) framework, one of the foundational results in mechanism design. What has been missing is a practical architecture that makes these ideas work at supply chain scale. In new work, my colleagues in Amazon’s Supply Chain Optimization Technologies (SCOT) organization and I show how combining VCG with Amazon's consensus planning protocol (CPP), a distributed, agent-based optimization framework, achieves exactly this. The resulting system, called Flo Pro, was successfully piloted over nine weeks with a prominent consumer-product manufacturer, demonstrating that the theory translates into real cost savings. The coordination gap To understand the opportunity Flo Pro presents, consider what happens today. Amazon issues purchase orders under a just-in-time (JIT) policy: it decides when, where, and how many units it wants, and the vendor decides how much of each order to fulfill. Within this sequential, noncooperative process, there’s room for further optimization: A vendor might be able to ship far more cheaply to one fulfillment center than another, but Amazon's JIT orders don't incorporate this information. Conversely, the vendor doesn't know Amazon's downstream demand patterns or outbound transportation costs, resulting in information asymmetry and preventing both parties from identifying the most cost-effective solution for all. The potential benefits from collaboration are easy to state in principle. If both parties shared their information, they could compute an optimized supply plan minimizing total supply-chain cost inbound and outbound, production and fulfillment. The hard question is how to realize these synergies when neither party wants to fully reveal its proprietary cost structure. From auction theory to supply chain coordination The VCG mechanism, named after William Vickrey, Edward Clarke, and Theodore Groves, achieves two ends simultaneously: social efficiency (the outcome maximizes total welfare) and incentive compatibility (every participant's best strategy is to report truthfully). The classic application is auctions, but the logic is far more general. In our setting, VCG works as follows. Amazon and the vendor each submit implicitly, through their optimization agents, their true preferences about supply plans. The mechanism computes the jointly optimal plan, then determines a transfer payment that equals each party's externality on the other. Concretely, the vendor pays Amazon an amount equal to the cost Amazon incurs by deviating from its preferred JIT plan to accommodate the proposed solution, a payment known as a cost-benefit transfer (CBT). Because this payment structure makes truthful reporting a dominant strategy, neither party benefits from misrepresenting its costs, regardless of what the other side does. CPP as the computational backbone The theoretical elegance of VCG faces a well-known practical barrier: it requires agents to submit their complete utility functions. In high-dimensional supply-chain problems with dozens of fulfillment centers, multiple products, and rolling weekly horizons, this is infeasible. This is where CPP comes in. CPP is a distributed optimization protocol based on the alternating-direction method of multipliers (ADMM). Rather than asking agents to reveal everything at once, CPP works iteratively. A central coordinator proposes a consensus plan and a set of prices. Each agent responds with its preferred plan given those prices — a "best response" that requires solving only the agent's own local optimization problem. The coordinator then updates the proposal, and the process repeats until convergence. The connection between CPP and VCG is natural and deep. CPP submissions from a truthful agent — one that honestly optimizes in response to each query — are equivalent to the submission of a truthful utility report in the direct VCG mechanism. The CPP iterations serve as the computational engine that finds the socially efficient plan. A second CPP run with one agent removed computes the cost to the remaining agent of its preferred plan; this provides the counterfactual needed to calculate the VCG transfer. The outcome is identical to that of the direct mechanism, but the information requirements are radically lighter: the vendor never reveals its cost structure, only its responses to iterative queries. This property — what we might call “information privacy” — is practically important. Vendors are understandably reluctant to disclose their production costs and capacity constraints. With CPP-based VCG, they don't have to. Their agents communicate preferences implicitly, through their optimization behaviors, and the mechanism extracts only the information needed to compute the efficient plan and the associated transfer payment. From theory to a rolling horizon Real supply chains don't stand still. Demand forecasts shift, supply conditions change, and plans must be updated continuously. We extend the static VCG framework to a dynamic, rolling-horizon setting inspired by the dynamic pivot mechanism that my colleague Juuso Välimäki and I described in 2010 and 2019. Each week, Amazon and the vendor plan a six-week forward-looking horizon. The mechanism issues a purchase order for the current week, computes what the resulting JIT policy would look like going forward, and determines the CBT. The CBT has an intuitive interpretation: it is the immediate cost of the current-week deviation plus the certainty-equivalent cost — that is, the cost that Amazon is willing to pay today to avoid an uncertain cost in the future — of that deviation on future periods. Whenever the proposed plan departs from JIT, the vendor compensates Amazon for the additional cost incurred, ensuring that neither Amazon nor the vendor is ever worse off from participating and benefiting the overall supply chain cost structure. This one-directional payment structure keeps the mechanism simple and robust, though extending it to two-way transfers — where Amazon might also compensate the vendor — remains an open design challenge A menu of contracts as an alternative For settings where the decision space is lower-dimensional, we also develop a “menu-of-contracts” approach. Here, Amazon computes a set of candidate supply plans and their associated prices — each price equal to the cost Amazon incurs from that plan— and offers the full menu to the vendor. The vendor simply picks the option that maximizes its own utility. By the logic of VCG, the vendor's best strategy is to choose the socially efficient plan. This approach has the advantage of transparency: the vendor sees concrete options and prices, rather than participating in an iterative optimization. It also opens the door to incorporating partial information: if a vendor indicates a general preference (say, for shipping more to one region), Amazon can tailor the menu accordingly. In our numerical example, the menu approach recovers the first-best outcome, with the vendor choosing the globally optimal plan from among the offered alternatives. Looking ahead The CPP-VCG framework is, at its core, a general-purpose tool for achieving consistent outcomes when each party acts on information unavailable to the other. The supply chain application we describe here is a natural first use case, but the underlying logic extends well beyond it. Vendor negotiations, Fulfillment-by-Amazon seller collaboration, and multiparty logistics planning all involve the same fundamental structure: interdependent decisions, private costs, and benefits that can be unlocked only through carefully designed incentive-compatible mechanisms. Several open questions remain. How should the mechanism handle the situation in which the vendor faces supply shortages and cannot deliver the agreed-upon quantities? Can mutual commitment structures — where both parties share obligations — improve outcomes when forecasts are highly uncertain? These are questions that sit at the intersection of economic theory and large-scale systems engineering, precisely the space where mechanism design has the most to offer. With Flo Pro, we have taken a first step toward making that potential concrete.

Large language models, the highest-profile machine learning (ML) models used today, are trained on huge corpora of public data. But many ML models are trained on smaller, proprietary datasets, which can be highly sensitive and should be kept private. Examples include a hospital fine-tuning a diagnostic model on patient radiology scans, a bank training a fraud detector on transaction histories, or a pharmaceutical company building a drug interaction model from clinical trial records. In each case, the training data itself is the asset that must be protected, but a well-constructed attack on these models can potentially extract information about their underlying training data. Such attacks are possible when the attacker is restricted to submitting adversarial inference queries to a model trained by a single data owner. Alternatively, when multiple data owners collaborate to train a model through federated learning (FL), in which a central server produces a global model by aggregating model updates generated from siloed datasets (instead of collocating the raw data), there exist attacks in which an adversarial server can reconstruct training data from the model updates. Consider three hospitals collaborating to train a shared cancer-screening model without pooling patient records. If the aggregation server can reconstruct one hospital's training images, then the privacy promise of federated learning is broken, and so is each hospital's compliance with patient consent agreements. Finally, an adversarial FL participant could even potentially reconstruct an honest participant's private training data from the global model. These risks are not hypothetical. A 2023 paper from Google DeepMind demonstrated that GPT-3.5-turbo could be prompted to regurgitate verbatim training data, including personally identifiable information. Smaller, domain-specific models trained on concentrated, sensitive datasets are even more vulnerable. As organizations increasingly train models on sensitive financial records, patient health data, and proprietary business intelligence, the attack surface grows proportionally. A successful attack against a healthcare model could reveal whether a specific patient's records were used in training, a violation of regulations such as the US Health Insurance Portability and Accountability Act (HIPAA) and the EU's General Data Protection Regulation (GDPR). An attack against a federated-learning system could reconstruct raw training samples that should never have left their source. For any organization training on private data, understanding and mitigating these threats is no longer optional; it is necessary for responsible AI deployment. In this post, we walk through three escalating attack scenarios: membership inference against a single model, data reconstruction from federated-learning gradients, and training-data extraction from a shared global model. We show how differential privacy and secure multiparty computation defeat each one. An attack on model inference Anyone with query access to a model can potentially determine whether a specific record was used to train it, an attack known as membership inference. Imagine that a hospital deploys a diagnostic model as an API for referring physicians. A malicious actor could probe the API to determine whether a particular patient's records were included in the training data. This would confirm that the patient was treated at the hospital and reveal details about their medical history. In a 2023 paper at the Conference on Neural Information Processing Systems (NeurIPS), Amazon Web Services researchers showed how this works in practice. A trained model tends to produce higher-confidence predictions for inputs it was trained on, a form of overfitting the attacker can exploit. The attacker first generates a dataset that approximates the distribution of the model's training data, then records the model's confidence scores on those samples. Using these scores as labels, the attacker trains a proxy model that learns a confidence-score cutoff separating training data from non-training data. Given a candidate record, the attacker evaluates the proxy model to obtain a cutoff, then queries the target model. If the target model's confidence score exceeds the cutoff, the record was likely in the training set. The authors demonstrated this against a ResNet-50 model trained on ImageNet-1k: 97% of records their attack flagged as training data were indeed training data. Mitigation through differential privacy We’ll show how to mitigate such membership inference attacks with differential privacy (DP), a mathematical framework for computing aggregate statistics (e.g., an average) while bounding how much any single input can influence the result. The core idea: if we can randomize the function so that adding or removing one record from the dataset barely changes the distribution of the function output, an attacker cannot confidently determine whether that record was included. Formally, a randomized function is differentially private if, for any single record added to or removed from the input dataset, the probability of any given output changes by at most a factor of eε, where e is the base of the natural logarithm and ε is the privacy budget. A smaller ε means tighter privacy but more noise in the computation, and vice versa. While NIST guidance suggests that ε < 1 will generally enforce a low enough privacy risk, many real-world deployments operate between 1 and 10, with situation-dependent privacy outcomes. Empirical studies indicate that ε as high as 3 can still provide meaningful data privacy against attacks like membership inference, though our understanding of the effective guarantees of DP against such attacks continues to evolve. DP defeats membership inference because the attack relies on a gap between the model's confidence on training data and on unseen data. DP narrows that gap by ensuring the model would have learned nearly the same parameters whether or not any particular record was included in its training data. How can this approach be applied to ML? Neural networks are trained using stochastic gradient descent (SGD), in which the difference between the model’s output on a training sample and the target output for the sample is propagated back through the model, and the model parameters are adjusted to reduce the difference; the adjustment corresponding to the sample is called a gradient. In practice, the model parameters are typically adjusted according to a batch gradient — the average of sample-specific gradients for a batch of samples. In a landmark 2016 paper, Google researchers introduced DP-SGD, which adds calibrated Gaussian noise to each batch gradient during training. We implemented DP-SGD and trained a neural network on the EMNIST handwritten-letter dataset. The DP model achieved 78% test accuracy at ε = 1.5 and 82% at ε = 3.0, compared to 90% without DP. DP addresses attacks on a single model, but what happens when multiple organizations collaborate to train one? Federated learning introduces a different attack surface, one that targets the training process itself. Data leakage from federated learning Federated learning is a method of decentralized ML in which a global model is trained on datasets distributed across multiple parties, without direct sharing of the datasets. Each party trains an initial model on a local training batch, obtaining a local gradient. The local gradients are then sent to a central server, which averages them into a global gradient. The parties then produce copies of the global model by updating their local models with the global gradient. However, in a 2019 NeurIPS paper, a team of MIT researchers demonstrated a surprising result: the parties' local gradients leak information about the training samples from which they're computed, enabling model inversion attacks in which the server can reconstruct the parties' training samples. Even in scenarios in which the server is not viewed as adversarial, this attack demonstrates that the gradients leak the parties' training data, defeating the privacy goals of FL. This attack relies on the observation that a gradient directly contains data about the sample from which it is computed. Consequently, a sample can generally be reconstructed from its gradient, and two semantically distinct training batches are unlikely to admit the same batch gradient. Therefore, the attacker frames the problem of reconstructing a party's batch samples from its local gradient as an optimization problem: find the training batch whose gradient is minimally distant from the target gradient. The attacker can then approximately compute the solution (the training batch) by applying SGD. In our experiments on the EMNIST dataset, the attack recovered single-sample batches exactly and three samples from a batch of size seven. Preventing this data leakage requires ensuring that no party, including the server, ever sees another party's gradient in the clear. Mitigation through secure multiparty computation Secure multiparty computation (MPC) is a cryptographic protocol that lets multiple parties jointly compute a function over their private inputs, without revealing anything beyond the function's output. Intuitively, the parties exchange only encrypted intermediate values, so no party ever sees another's raw input. A simple example illustrates the core idea: suppose three parties hold private values x, y, and z. Each party splits its value into three random shares that sum to it, then distributes one share to each party. Each party sums the shares it receives. The resulting sums are themselves random, but they add up to x + y + z. After exchanging these sums, all parties learn the total but nothing about each other's individual inputs. Private federated learning (PFL) applies this secure-sum technique to FL: instead of sending raw local gradients to a server, the parties secret-share their gradients and aggregate them via MPC, so the server only ever sees the summed result. More efficient PFL protocols exist, including one presented in a 2023 paper coauthored by Amazon senior principal scientist Tal Rabin, but the core security principle is the same. We ran our model inversion attack against a party's local gradient computed under our PFL protocol, again using the EMNIST dataset. The attack was unable to reconstruct any training samples. MPC protects the gradients exchanged during FL, but the global model itself is shared with all participants. Can an adversarial participant exploit the model to recover others' data? We’ll explore this problem in the next section. An attack on FL global models and mitigation with DP We've seen how PFL enables n parties to securely compute a global FL model. However, the 2022 paper of Fowl et al. and 2025 paper of Shi et al. together describe an attack that enables an adversarial FL participant to reconstruct another participant's training data from the global model itself. In this attack, the attacker adds a preprocessing layer with ReLU activation (a common neural-network activation function that outputs positive inputs verbatim but outputs zeros for negative inputs) to the model. That layer consists of nB neurons, where B is the batch size. This is because each of the n parties produces a local gradient that is an average of B sample-specific gradients, so the global FL gradient is an average of nB sample-specific gradients; each of the nB neurons in the preprocessing layer will be used to reconstruct a distinct training sample. The attacker carefully crafts the preprocessing layer's parameters so that ReLU activates the signals of all samples in the first neuron of the global gradient, all but one sample in the second neuron of the global gradient, all but two samples in the third neuron of the global gradient, etc. Therefore, the attacker simply examines the entries of the global gradient corresponding to the nB neurons and successively subtracts the components between adjacent neurons to tease apart the nB sample-specific gradients. As we mentioned earlier, a training sample can be directly recovered from its gradient. In our experiments on the EMNIST dataset, the attack recovered all but one of the parties' local batch samples from the global gradient. But after altering our private FL protocol to instead output a differentially private global gradient — computed via DP-SGD with privacy budget of 1.5 — the attack failed to recover any meaningful information from the global gradient. Taken together, DP and MPC form complementary layers of defense: MPC protects what is exchanged during training, and DP protects what the final model reveals. Building defenses before attacks scale The experiments above have clear implications: attacks on ML training data are practical today, and the private-computing tools to defeat them are mature enough to deploy. The privacy-utility tradeoff is real: our DP-SGD models retained 78–82% accuracy at meaningful privacy budgets, compared to 90% without DP. It is worth noting that the accuracy impact of DP depends heavily on the task and dataset. Our EMNIST experiments used a relatively small model on handwritten letters, where the noise has an outsized effect. In practice, larger models trained on richer datasets absorb DP noise more gracefully. NIST SP 800-226 notes that large models pretrained on public data show strong privacy-utility tradeoffs when fine-tuned with DP-SGD. For many production use cases, such as fraud detection or clinical risk scoring, a modest accuracy reduction is an acceptable cost when the alternative is exposing protected data to the attacks described above. The right privacy budget is ultimately application dependent: a model screening radiology scans may tolerate less accuracy loss than one flagging suspicious transactions, and organizations should calibrate ε to their specific risk and regulatory requirements. These techniques are already in use at Amazon. We are building private-computing capabilities — differentially private training pipelines and secure aggregation for federated learning across organizational boundaries — into production systems. For instance, our fraud prevention teams use differentially private training to protect customer financial data while maintaining detection accuracy. If your organization trains models on sensitive data, we invite you to explore AWS's privacy-preserving ML capabilities and connect with our team.

At Amazon, AI now touches everything from warehouse logistics to customer service chatbots to AWS cloud services used by thousands of enterprises, making it a business-critical technology. It’s therefore imperative that the models Amazon develops and deploys are as safe, fair, and robust as possible: responsible AI (RAI) is not an optional add-on. As Rahul Gupta, senior science manager and RAI lead for Amazon’s Artificial General Intelligence (AGI) organization, puts it, “Responsibility is baked into the product design from day one.” Amazon’s commitment to safety and responsibility goes back long before the generative-AI boom. Gupta and researchers on his team worked in the Alexa AI organization, where the company “developed some muscle on defining how RAI should be done.” The focus, he recalls, was on developing policies and implementations as well as methods to evaluate their effectiveness. As Amazon began building its own large models, the RAI expertise from Alexa proved a valuable resource. In concert with Amazon’s policy team, AGI scientists have built an RAI pipeline that addresses four phases of model development: pretraining, post-training, evaluation, and third-party monitoring. At each stage, researchers grapple with distinct challenges to ensure that trustworthy systems can adapt, at scale, across situations, applications, and geographies. From this framework, Amazon has built over 70 internal and external RAI tools, funded or published more than 500 research papers, and delivered tens of thousands of hours of RAI-focused training to its employees. Amazon has a three-pronged approach to RAI: anticipate risks before they materialize, teach models to navigate ambiguity, and build systems that can adapt — to government transitions, high-profile incidents, new regulations, and other social changes. Below are some of the scientists across Amazon’s responsible-AI and policy teams who put this approach into practice — each tackling a different phase of the AI lifecycle. Teaching foundations: Pretraining Chentao Ye is a senior applied scientist on the AGI RAI team, working on pretraining, the earliest stage of LLM training, where the model develops general linguistic competences. It’s become increasingly critical to address RAI at this stage, says Ye, to ensure that the model has the information necessary to adapt to policies established by Amazon’s policy team. “Pretraining is the stage where we teach our most fundamental concepts of RAI,” Ye says. “It’s like teaching a child about the world before we expect them to make some decisions.” Pretraining typically involves large volumes of public data, but the RAI team augments that data with datasets specifically designed to instill principles of safety, security, and fairness. Those datasets are vast and diverse — a “rich diet” of content including internal and public RAI guidance, best practices, RAI-related news and incidents, information about domains such as chemical and nuclear engineering and coding security, text, audio, and images. Also included in the corpus is information in different languages and from different cultures, to ensure the model is global and multilingual. To help the model better incorporate this array of information, researchers create training tasks, also known as learning exercises, for it. “Having this data isn't enough. We need to help the model process and understand it effectively,” Ye says. For instance, Ye and his colleagues might take a policy document about privacy and convert it into multiple learning exercises: explaining privacy concepts, answering questions about compliance, and determining whether certain actions would violate privacy guidelines. These varied tasks help the model develop a deeper, more nuanced understanding of RAI principles. Another active area of research is how to handle potentially harmful content in the training corpus. “It's not simply about filtering everything out,” Ye explains. “If a model has never encountered certain harmful concepts during pretraining, it won't recognize them as sensitive, making post-training guardrails less effective.” The team is exploring approaches that add educational context to certain filtered content before reintroducing it — teaching the model what harm looks like and why it should be avoided, rather than leaving it entirely unaware. In addition to RAI acquisition, another area of focus is what’s called RAI modality alignment. LLMs need to understand how to apply RAI principles across all the modalities they encounter. Modality alignment maps other modalities into a semantic space they share with text, which is often more readily available, Ye explains. For example, a college textbook might include figures of high-risk chemical, biological, radiological, and nuclear materials (CBRN) and text descriptions of the same concepts. The team designs a range of LLM tasks that effectively encode the data into the same space. One active research area is developing a variety of techniques to test for pretraining quality, says Ye. The team is taking two complementary approaches. The first tests whether the model has actually acquired RAI knowledge during pretraining. “We use metrics like perplexity” — which quantifies how well a probability distribution predicts a given sample — “to measure how well the model can generate content in specific RAI domains,” Ye explains. The second approach tests the way that the model responds to sparse questions that might appear in later testing exercises, where the expected responses — like refusals or deflections — weren't explicitly taught during pretraining. “This helps us test whether the RAI knowledge it gained during pretraining enables it to generalize to real-world scenarios with just limited examples or instructions,” Ye says. Post-training: Reinforcement learning from human feedback Once models learn to follow instructions and produce both helpful and harmless responses, they advance to reinforcement learning from human feedback (RLHF). Senior applied scientist Charith Peris, who leads this phase of model development, and applied scientist Yao Ma explain that RLHF focuses on using feedback from or preference comparison with humans to give models a sense of judgement. “RLHF is done to make sure the foundation model aligns with the behavior expected by humans,” says Peris. This stage of training provides the model with a reward based on how well its response to a query meets a predetermined criterion. The rewards are provided by various response verification systems. One approach uses so-called auxiliary-reward models, which are trained on outputs that humans have ranked. For responsible AI, this stage offers the ability to optimize the model to generate responses that are “policy adherent,” hewing to the rules and guidelines devised by Amazon’s policy team. “Providing the right rewards is a critical part of RLHF,” says Ma. In one case, the core model itself is used to generate multiple responses to a range of unsafe and borderline safe queries. These responses are ranked and rated by humans based on their helpfulness and policy adherence and then used to train auxiliary-reward models. Another response verification approach uses an independent LLM as a judge. The model generates a response for each prompt in the training set, and this response, together with a set of rubrics about what makes a response policy adherent, is passed to the judge. The judge is then instructed to provide a score based on how well the response aligns with the rubrics. Both the auxiliary-reward models and the judge-based systems can be used individually or in combination to provide RLHF rewards. The model is evaluated in two phases: during and after training. In the first phase, the model is tested at frequent, short intervals using lightweight benchmarks that provide directional signals on performance across critical capabilities. In the second phase, saved checkpoints, each a complete snapshot of the model's state and parameters at a given point in training, are systematically evaluated against a broader set of test data to identify which checkpoint achieved the best overall performance. Behavior in check: Evaluations A major focus of the evaluations team is to build model-breaking datasets — robust collections of prompts that trigger inappropriate, unsafe, or policy-violating responses. “We know models are improving month over month,” says Jwala Dhamala, a senior scientist with Amazon AGI . Bigger, better responsible-AI datasets are playing a large part in this, she says, as well as improved mechanisms to capture how well the models incorporate responsible-AI principles spanning multiple modalities and regions. Working closely with Amazon’s policy team, Dhamala says, is key to developing evaluations for RAI. Amazon’s RAI work has eight pillars: privacy and security; safety; fairness; veracity and robustness; explainability; controllability; governance; and transparency. "For each pillar, we focus on tests that could lead the model to output something that violates responsible-AI policies. Simultaneously, we focus on testing if a model is refusing excessively or refusing to respond to benign requests," Dhamala explains. The data comes from everywhere: human experts known as red teamers who try to break models, external security partners, public benchmarks from universities, even social media where real-world problems surface organically. The RAI team evaluates models throughout the model-training and deployment cycle, Dhamala explains, from pretraining to post-training and predeployment, when all scaffolding is attached. Each stage has its own specially designed evaluation processes, and more testing happens in the later stages, when the model is closer to end users. "We collect datasets, evaluate, then collect new datasets, evaluate again,” Dhamala says. She adds that the team is currently working to automate more of the evaluation process. It’s also pushing into newer areas of research. Deception in conversations that require many back-and-forth interactions over weeks or months (also called long-horizon interactions) is emerging as a concern, but there aren't many established benchmarks for detecting it. Creating them requires an understanding of what deception means across different long-horizon contexts, an understanding grounded in social-science research. Another open area of research is an automatic red-teaming framework to evaluate emerging responsible-AI risks. The idea is that an autonomous agent or a system of agents would compete or collaborate in attempts to provoke undesired behaviors. Third-party collaborations: Frontier risks While most RAI work addresses common misuse patterns, Tong Wang, a senior applied scientist with AGI, focuses on a different category of risk: frontier risks, or “systemic risks that could take down entire systems.” These include the use of AI models to research CBRN (chemical biological, radiological, and nuclear) attacks and to research or launch cyberattacks. These are scenarios where AI capabilities could enable nonexperts to cause catastrophic harm. The evaluation process for frontier risks is exacting. First, automated benchmarks test whether the model has acquired dangerous knowledge. If it passes certain thresholds — answering questions about weapons of mass destruction with concerning accuracy — that triggers human review. Third-party experts in relevant domains evaluate whether the model has crossed safety boundaries. And the process is ongoing: with each model update, the team compares the new model’s capabilities against those of earlier models. "We have to be very careful,” Wang says. “False positives and false negatives both have costs." With public models, identified risks are mitigated by guardrails: when a person asks about a particular topic at a particular level of specificity, the model simply won’t respond. But legitimate researchers — scientists at universities and labs with relevant expertise and appropriate oversight — may need access to restricted information for their work. Wang’s team is exploring mechanisms to provide “specialized access with heavy monitoring” for these trusted users. Those mechanisms involve what Wang calls “configurability”, using techniques like low-rank adaptors (LoRA) to make surgical changes to a model's behavior for specific use cases, without retraining the entire model. "We add configuration on top that doesn't touch the base model itself," he says. "You're not retraining a billion parameters, just a few.” Today, this approach is already in use for certain content policies. But extending it to frontier risks like CBRN is a harder problem; both the data collection and computational costs are significantly higher. "It's an open research area, studying which approaches work best," Wang notes. Agreed-upon values: Writing the policies "We partner with the Amazon science team throughout the entire model development lifecycle," explains Claire O'Brien Rajkumar, leader of the responsible-AI policy and product team. The process starts with understanding what a product team wants to launch — whether it's an image generation model or a large language model — and mapping potential harms against Amazon's eight core dimensions of responsible AI. Before building an image generator, for instance, the team might anticipate risks such as deepfakes, bias amplification (for instance, an image depicting doctors only as white males), or attempts to generate disturbing content. Identified risks are translated into specific policies that define behavioral boundaries for the model under development. These policies become "backward-working guidelines," O’Brien Rajkumar says, that inform every subsequent decision during model building. For instance, rather than sourcing images from a single vendor that might show only white male doctors, the team ensures diverse data collection that reflects the complexity of the real world. Amazon’s policies are informed by factors including industry trends, customer requests, regulations, and legal requirements (particularly around copyright and content licensing). The team actively participates in industry groups like the Frontier Model Forum and Partnership on AI, collaborating with competitors to establish best practices in an under-regulated space. Academic partnerships help identify emerging risks through the development of benchmarks as well as engagements such as the Trusted AI track of the Amazon Nova AI Challenge, where university students compete to identify safety vulnerabilities in Nova models and the associated fixes. Customer feedback shapes practical policy decisions, such as carving out exceptions for legitimate use cases such as LLM-based security testing, even when the general policy prohibits malware generation. The policy team operates through cross-functional working groups that include legal, public-policy, product, security, and RAI experts. Regulatory developments like the EU AI Act and California's AI Transparency Act directly influence policy evolution. "These are living, breathing things," O'Brien Rajkumar notes, acknowledging that policies must adapt as society becomes more comfortable or less comfortable with certain AI risks. Beyond policy development, and specific responsible-product guidelines, the team manages the implementation of AI safeguards and oversees red-teaming operations using both in-house experts and third-party vendors. It also conducts manual reviews of model outputs to assess real-world risk. “These are high-judgement decisions, working on the boundaries of what violates policy or not,” says O’Brien Rajkumar. “We have to really understand what each policy means in practice.”

As large language models (LLMs) become increasingly useful across a variety of domains, the stakes of keeping them safe rise accordingly. Because bad actors might, for instance, try to use LLMs to write malicious code or make step-by-step guides for synthesizing toxic compounds, researchers are developing rigorous safeguards to keep LLMs from generating content that could pose serious public safety and security risks. The most common way to assess the risks to LLMs is called red-teaming, where human evaluators design adversarial prompts intended to elicit harmful responses. But expert-curated sets of prompts cannot capture the full range of possible outcomes. Moreover, many evaluations focus on isolated prompts rather than conversations, which are where harmful behavior often emerges. Finally, today’s benchmark failure metrics provide only a single score, rather than confidence bounds on worst-case conversational risks. This makes the findings unreliable and non-generalizable to the vast space of possible conversations. In a paper we presented at this year’s International Conference on Learning Representations (ICLR), we, along with researchers from the University of Illinois Urbana-Champaign (UIUC), address these red-teaming limitations by focusing on the failures within conversational threat models and then assigning a probability to an attack rate, which is defined as the number of successful attacks divided by the total number of attacks. Our approach, called the C3LLM (certifying catastrophic conversational risks in LLMs) framework, shifts the focus of benchmarking failure from empirical spot-checking to statistical certification. How to model a conversation In order to build our framework, we first needed to model conversations, also known as “multiturn dialogues.” We used a graph where each node corresponds to a prompt. The edges that connect the nodes indicate that the prompts are semantically related. This graph approximates plausible conversational transitions, capturing how a user might naturally progress through related questions. In this way, we generate a more complete picture of queries, one that maintains the complexity of possible conversations. The graph also lets us define the distribution of conversational threats, allowing us to determine the probability of harm across a range of adversarial capabilities. We simulate the lowest level of adversarial capability by sampling prompts independently, which is similar to traditional benchmarking, focusing on a single node or query at a time. This approach is denoted as Random Node with Jailbreak (RNwJ) is our result. The next level up involves sampling a sequence that follows semantically connected paths through the graph. We developed two variants, the first is termed Graph Path vanilla (GPv), where each query is sampled following the graph, the second appraoch — Graph Path harmful target constraint (GPh), restricts the final query to come from a target harmful set. For the most advanced level of bad-actor capabilities, we approximate adversarial steering, when a bad actor coaxes an LLM toward a harmful output. For this level, we sample adaptively, examining prior movements throughout the graph-based conversation to map the distance to a query that ultimately produces the harmful output. This approach — Adaptive with Rejection (AwR) — can mimic realistic red-teaming where an attacker adapts their phrasing to circumvent safety mechanisms. The graph gives us the ability to create sets of multiturn-dialogue prompts — specific sequences of queries — that we can run on a target LLM. We then label the LLM responses as catastrophic or non-catastrophic using a separate ChatGPT-based judging mechanism that determines whether the model responses are harmful. This produces empirical estimates of the attack success rates under each conversational distribution. Given the attack success rate, C3LLM uses the Clopper-Pearson method to calculate the lower and upper bounds on the probability of catastrophic risk. Application: How does C3LLM perform on frontier LLMs? UIUC researchers applied the proposed C3LLM framework to frontier proprietary models available at the time of the study, such as Claude-Sonnet-4 and Nova Premier, as well as open-weights models (models whose trained parameters are publicly available). The following figures show the certification results on the chemical/biological benchmark. Each panel shows the distribution of lower bounds and upper bounds under different specifications for one LLM. The following figures show the certification results on the cybercrime benchmark. Each panel shows the distribution of lower and upper bounds under different specifications for one LLM. The results reveal that catastrophic risks are nontrivial for all frontier LLMs, with notable differences in safety across models. By comparing the bounds, we observe that among the models evaluated, Claude-Sonnet-4 and Nova Premier are safer than the others, while Mistral-Large and DeepSeek-R1 exhibit higher risks. In particular, Nova Premier demonstrates consistently low risk levels, largely because its built-in guardrails often block potentially unsafe content. On the other hand, DeepSeek-R1 reaches a certified lower bound of over 70% in cybercrime scenarios under RNwJ distributions. Unlike prior work that reports attack success rates on fixed benchmarks, our approach provides high-confidence probabilistic bounds over large conversation spaces, enabling meaningful comparisons across models. We open-sourced the C3LLM framework for reproducibility and hope it enables researchers in industry and academia to perform more-principled safety studies.

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. 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. 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: to formalize the semantics of the WebAssembly language, to identify errors and, in particular, to prove the soundness of its type system; to create a verification framework for the Cogent programming language; to prove the correctness of algorithms for conflict-free replicated data types, which are used for distributed editing; to formalize numerous results in pure mathematics; to verify cryptographic protocols at an abstract level. Isabelle is free, open source, and available to download. It runs on all the main operating systems on any machine that has enough memory.