IAM Axiom Verifier
A Neuro-Symbolic Inference Engine for AWS Security & FinOps — mathematically auditing IAM policies with LLMs and SMT solvers.
🧪 Experimental PoC. Early-stage prototype. It is functional but actively evolving. Use in production environments is not recommended yet.
Screenshots
IAM policy auditing process via symbolic reasoning
Mathematical counter-example generation for security gaps
Overview
IAM Axiom Verifier is a mathematical auditing tool for AWS environments. It combines the flexibility of Large Language Models (LLMs) for semantic routing with the absolute rigor of SMT solvers (Formal Verification) to evaluate IAM policies. Instead of relying on regular expressions, heuristics, or AI hallucinations, this engine translates the AWS state into a system of inequalities and boolean logic, mathematically demonstrating risk vectors. The engine works by first using an LLM to semantically parse and understand the intent behind IAM policies, then feeds those parsed intents into a Z3 SMT solver that formally verifies security properties. This hybrid approach means you get both the language understanding of AI and the mathematical certainty of formal verification — eliminating false positives caused by hallucinations while maintaining the ability to reason about complex permission relationships.
Why Formal Verification?
Traditional CSPM
Pattern matching with regex. High false-positive rates. Cannot reason about transitive permissions.
AI-only tools
Can hallucinate findings. No mathematical guarantees. Output varies between runs.
IAM Axiom Verifier
Mathematically proven findings. Zero false positives by construction. Reproducible every time.
Architecture
The engine is structured in two phases: 1. Semantic Layer (LLM Router): An LLM parses raw IAM policy JSON, understanding the semantic intent of each statement. It extracts principals, actions, resources, and conditions into a structured intermediate representation. 2. Formal Verification Layer (Z3 SMT Solver): The structured representation is translated into Z3 constraints — a set of mathematical assertions about the permissions system. The solver then explores the full permission space to find provable security violations and risk vectors. This separation ensures that language ambiguity is handled by the LLM (which is good at NLU) while logical correctness is guaranteed by the SMT solver (which provides mathematical proofs).