Episode 187 - GluuFederation/identerati-office-hours GitHub Wiki
Title: Automated Reasoning Meets AI: The Next Leap in Verified Infrastructure
- Host: Mike Schwartz, Founder/CEO Gluu
- Guest: Varun Pant, Product Leader AWS
- Guest: Rohit Khare, Product Manager & Software Architect
Channels
Description
Automated reasoning technologies — including solvers and theorem provers — have long secured critical infrastructure by mathematically verifying systems and policies. From AWS ensuring secure S3 configurations to formally verified authorization engines like Cedar, these tools provide strong guarantees of reliability and security. Now, AI is accelerating this field at scale, enabling natural language policy creation, AI-driven proof discovery, and the development of verified computer science libraries — marking a new era where intelligent systems and formal verification work together to build safer, more trustworthy software.
Homework
- ACM Paper — Why AI systems need machine-checkable certificates of correctness
- Github Repo — Lean's answer to Mathlib but for CS: verified algorithms, data structures, and cryptographic foundations
- Lean Project Homepage — the theorem prover powering the autoformalization wave
- How Automated Reasoning checks in Amazon Bedrock transform generative AI compliance
- 50 Years of Failure Presentation at FormalWorld
Takeaways
-
⚡ Formal reasoning is like the US Constitution. Although federal, state and local laws provide increasing specificity, the Constitution provides the core "bones" of the legal system--the stuff that must always be true. Enterprises won't be able to make policies to address every possible contingency. But the core policies prevent some unacceptable risks--e.g. max radiation.
-
⚡ Relying on LLMs is not appropriate for some risks. For example, in the financial sector breaking regulations can result in fines or other business impacts. Formal systems (e.g., SMT solvers or theorem provers) enforce correctness by enforcing mathematically provable constraints. This enables deterministic validation of policies (e.g., insurance claims rules or access controls) instead of approximate compliance checks.
-
⚡ The “why now” inflection point is driven by five converging factors: (1) faster solvers, (2) mature theorem provers like Lean, (3) large formal libraries, (4) LLM-assisted auto-formalization, and (5) reinforcement learning on proof systems. Together, these create a feedback loop where models improve reasoning while formal systems ensure correctness.
-
⚡ Formal methods have challenges: performance, scale, difficulty of writing correct specifications. But it's clear that deterministic external control layers are necessary to control certain high value agentic business flows.