Recent advancements in Generative AI have enabled customers to use LLMs to generate infrastructure code using AWS CLI commands. Because humans can make mistakes, when deployed such LLM-generated infrastructure code can have negative impacts, including on security.x000D
Motivated by this challenge, this demonstration introduces participants to automated reasoning tooling that enhanced security in production for Amazon Q chat. x000D
AWS Q Chat enables natural language interaction with AWS resources while employing automated reasoning to verify every generated API call against comprehensive semantic logic models. This prevents potentially harmful operations before execution and suggests corrections, creating a feedback loop that iterates until verifiably correct code is produced. Through this work, we demonstrate how organizations can leverage GenAI's efficiency while maintaining the rigorous verification standards required for production environments and participants will learn how to integrate these tools into their workflows to prevent security regressions and ensure reliable infrastructure management. This tutorial Scientists, Engineers, Security professionals and anyone interested in applying formal verification to their infrastructure.