Amazon Scholar Aravind Srinivasan coauthored a 2014 paper about forecasting civil unrest in Latin America, which won a test-of-time award at KDD 2025.

On July 16, 2018, Amazon distinguished scientist Byron Cook was giving a keynote at the Federated Logic Conference (FloC) at the University of Oxford, a computer logic gathering held every four years since 1996. In the keynote, Cook described how his team was using an open-source software tool called cvc (cooperating validity checker) to identify logic problems in code and fix them. Sitting in the audience was Stanford University professor Clark Barrett, who had been working on cvc for almost 20 years. Cvc had been developed to analyze verification problems encoded as satisfiability modulo theory (SMT) problems. SMT is a mainstay of formal methods — the use of automated reasoning to prove that a program or system will behave as intended. By applying SMT at scale, cvc can detect logical errors in code and in systems such as those used for authentication and access management. “I was kind of stunned. It was really exciting,” Barrett says. “And this really started with this exciting moment of realizing, Hey, our work is being used by Amazon.” The encounter between Cook and Barrett ultimately led to a years-long research collaboration that culminated in Barrett’s becoming an Amazon Scholar in 2023. Initially, Amazon provided small grants to Barrett’s lab at Stanford’s School of Engineering through the Amazon Research Awards program; those grew into larger funding commitments as the research progressed. This funding supported foundational research that — together with deep technical collaboration between the two teams — enabled the development of cvc5, the latest version of the open-source software. Cvc5 has delivered significant value for both Amazon customers and the broader industry, while simultaneously advancing academic research. As one example, cvc5 is used in Automated Reasoning checks, a new Amazon Bedrock feature that verifies natural-language content against organizational policies. It powers access-policy analysis tools, including Identity and Access Management (IAM) Access Analyzer, a service that helps customers securely manage access to AWS resources. More recently, Amazon has begun deploying cvc5 for specification analysis and test generation in Kiro, a new agentic development environment. Across these applications, cvc5 now processes approximately one billion solver calls every day, enhancing security, reliability, and durability for AWS customers. A meeting of minds Working with Barrett on the project is Robert Jones, a senior principal applied scientist at AWS who shared an advisor with Clark when both were Stanford PhD students. Also involved in the project over the years were many students and postdocs keen to test their skills. More than a few have since joined Amazon to develop new implementations and applications, extending work that began when they were student researchers. “What's really fun about it is that people who have just finished their PhD, for example, often bring fresh insight to long-standing research challenges because they're thinking about them in a different way,” Jones says. “And I find that the best part of collaboration is that different people tend to build different mental models for the same problem. When those come together, you often have new insight into how to think about the problem or how to map it to a different problem you already know how to solve.” A successful coupling of academic research and commercial funding can have great impact, but as Barrett points out, there needs to be a focus on achievable goals. It’s easy to get caught up in an interesting project idea that leads to a practical dead end, Barrett says. “If you're in your ivory tower, building your tools, and you don't have access to the real problems, it's very easy to build the wrong tool. And I've actually made this mistake,” he says. “You build a hammer, and then you go around looking for a nail, and you can't quite find anything that fits. You get excited about a particular approach but don't think about what that approach could be good for. So I actually now much prefer the opposite, where I go find a real problem, and then I take a step back and say, ‘What approach can we actually use to solve that?’” When you change code, he says, “Eighty percent of the time it does better, and 20 percent of the time it does worse. This is actually not so great in some contexts.” Sorting the wheat from the chaff is essential to producing robust and scalable code, he adds, and large-scale testing is needed to find and fix issues that can be inadvertently introduced as the code changes. Analyzing interactions at that level requires multiple minds, and the more the merrier, Jones says. The old adage “many hands make light work” is particularly useful when mixing public research and practical applications. “I really like to work on hard problems that require multiple people to solve. I enjoy the collaboration involved in science,” he says. “I've always found that more minds working on the same problem together are better than one.” Barrett and Jones agree that what makes this work is a willingness to see from both points of view — the scholastic and the commercial. Sometimes a pure research goal can have very beneficial results, sometimes not, but melding these two approaches together to address serious issues can deliver huge benefits. And communication is key, both agree. “One of the hard things about academia is knowing which problems are the most important to work on and how those problems might impact the real-world problems that are being encountered in industry,” Jones says. “Having the ability to be much more open about the kinds of problems that we're struggling with and Clark telling us about his research agenda helps both of us. It enables Amazon to indicate areas of interest, and it helps Clark understand concrete problems that we encounter day to day as we try to apply these tools and techniques in practice.”

The Amazon Nova AI Challenge is back for its second year. As ten selected university teams from around the world gather in Seattle this week for bootcamp (February 2-4), they're preparing to tackle a real-world challenge in software development: building AI agents that can handle complex coding tasks while maintaining security and reliability. For the first time in an academic competition, participating teams will use Amazon Nova Forge to customize Nova models with access to tools, models and computational resources that have historically been out of reach for university research programs. From single tasks to multi-step projects Last year's competition focused on secure AI-assisted software development, with teams working to identify and address vulnerabilities in code-generating models. Teams published research papers on their approaches, and the results demonstrated practical methods for improving security in AI coding tools. This year's challenge reflects how AI coding technology has progressed. "Generative AI for software development has rapidly moved from code generation to agents that plan, build, and test changes across entire codebases and user-facing applications," said Imre Kiss, Director, Amazon Nova Software Engineering Skills, "The focus of this year's Nova Challenge reflects that shift." The 2026 challenge centers on AI agents that can work through multi-step software development tasks, including planning changes, writing code, and validating results across complex projects. Unlike generating code from a single prompt, these systems must understand context across entire codebases and make decisions that affect product quality and system security. Teams must demonstrate progress on two measures: utility (can the agent handle increasingly complex software tasks?) and safety (does it maintain appropriate safeguards?). This dual focus addresses a practical reality: as AI agents become more capable, new security challenges emerge. Each team's approach will be different: some may focus on adding secure coding patterns to their training data, others on creating training environments that teach their agents to recognize security issues, and others on building smaller, faster models with strong agentic security reasoning. The red teams will develop methods to test the applications built by these AI coding agents for weaknesses, attempting to identify potential vulnerabilities and exploits. "The competition format creates an interesting dynamic," explains Rahul Gupta, Senior Applied Science Manager, Amazon Nova Responsible AI. "As red teams discover new vulnerabilities, developer teams must adapt their agents through retraining or additional safety controls. And as developer teams strengthen their systems, red teams must develop more sophisticated testing methods." Nova Forge: Access to model customization The significant change for this year's competition is integration of Nova Forge, Amazon's service for building customized AI models. Academic institutions have historically had limited access to the models, training data, and computational resources needed for large scale AI-research. Nova Forge changes that. "What researchers (and entrepreneurs) have traditionally faced is a set of difficult trade-offs," explains Michael Johnston, an applied science leader at Amazon overseeing the challenge. "You could fine-tune an existing closed model, but only in limited ways. You could work with open-source models, but risk losing core capabilities. Or you could build from scratch, but only if you had very substantial funding." Nova Forge offers another approach. The service gives teams access to Nova model checkpoints at different training stages, allowing them to add their own data throughout the training process. The result is a customized model — what Amazon calls a "Novella" — that combines Nova's capabilities with the team's specific approach to secure software development. "This changes what's possible for academic research," says Professor Ismini Lourentzou, University of Illinois Urbana Champaign. "We're participating in the training process itself, adding our research and security methods into the model's foundation." Nova Forge provides three capabilities that competing teams will use: Custom training environments: Teams can create simulated environments where models learn from scenarios that reflect real-world secure coding workflows. Model compression: Teams can create smaller, faster models that maintain performance at lower cost by training them on examples from larger models. Safety controls: Built-in tools allow teams to implement security measures and evaluate model behavior against their safety criteria. The competing teams Ten universities were selected to compete this year from a pool of applicants spanning five countries: the United States, Portugal, the Czech Republic, South Korea, and Taiwan. The lineup includes two returning champions and eight new teams: Model Developer teams: PurpCorn, University of Illinois Urbana-Champaign - Year 1 champions BlueTWIZ, NOVA School of Science and Technology, Lisbon, Portugal AlquistCoder, Czech Technical University, Prague, Czech Republic BruinWeb, University of California, Los Angeles Slugs and Roses, University of California, Santa Cruz Red teams: PurCL, Purdue University - Year 1 champions Jay'lBreak, Johns Hopkins University TeamSecLab, Ohio State University Pr1smCode, Carnegie Mellon University Lion-x0a, Penn State University Each team receives $250,000 in sponsorship, monthly AWS credits, and the chance to compete for prizes. The winning model developer and red teams will each receive $250,000 (split among students), with second-place teams earning $100,000. Practical research For participating students, the challenge is an opportunity to work on problems with direct application. "Academic research often focuses on theoretical problems," notes Xiangzhe Xu, PhD Student, Purdue University. "Here we are working with large-scale models. That changes how we approach the science." Amazon researchers working with the teams emphasize solutions that are straightforward to implement, easy to troubleshoot, and economically viable at scale. "We want innovations that engineers can actually use," says Johnston. The challenge also gives students experience with infrastructure not typically available in academic settings. Along with Forge, and the computational resources to train and evaluate large-scale models. "For a university team, this level of access is significant," says Professor Xiangyu Zhang, Purdue University. "We're able to run experiments that would be difficult on our academic budget, and students are gaining experience with the same tools used by top-tier AI companies." What's next The first evaluation will begin after bootcamp concludes, with additional rounds scheduled through August 2026. The finals will be in September 2026 and winners will be announced October 2026 at Amazon Nova AI Challenge Summit where teams will gather to present their research and celebrate the winning teams. All participating teams will publish research papers on their methods and findings. These publications will contribute to the field of responsible AI development, with particular focus on secure AI systems, insights that will benefit software development and other applications where AI interacts with complex systems. As AI systems become more capable of software development work, the research these teams are conducting becomes increasingly relevant. As AI coding systems take on more and more complex and impactful tasks, the key question is how to ensure the resulting applications are secure, reliable, and trustworthy at scale. Stay tuned for updates on the teams' progress and coverage of theSeptember 2026 finals.