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 68 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 LeanXiaorui 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 OrchestrationAriel 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 SystemsZhengzhong 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