What if you could combine the creative power of generative AI with the mathematical certainty of formal verification? In this episode, Danilo Poccia — Principal Developer Advocate at AWS — breaks down automated reasoning, a field of AI that has been quietly powering critical AWS services for years and is now becoming essential for production AI systems. We explore why generative AI alone is not enough for high-stakes applications, and how automated reasoning provides mathematical proof — not probabilistic guesses — that your AI agents are following the rules. Danilo traces the roots of automated reasoning back to the 'symbolist' branch of AI, explains how AWS has used it internally for years to verify S3 bucket policies, encryption algorithms, and network configurations, and shows how it now converges with neural networks in what researchers call neurosymbolic AI. On the practical side, we dig into Amazon Bedrock Guardrails with Automated Reasoning checks — the first and only generative AI safeguard that uses formal logic to verify response accuracy. Danilo walks through how developers can use policy verification for agentic systems and tool access control with Cedar, and how AgentCore Gateway fits into the picture for managing MCP-based tool interactions at scale. We also cover the open source landscape: Dafny for verification-aware programming, Lean as a theorem prover, Prolog for logic programming, and the growing ecosystem of MCP servers that bring these capabilities into everyday development workflows. Whether you are building AI agents for production or just curious about what comes after prompt engineering, this conversation will change how you think about AI reliability.

With Danilo Poccia, Principal Developer Advocate, AWS Developer Relations

Neurosymbolic AI: Combining GenAI with Mathematical Proof — with Danilo Poccia