Deterministic Verification for Infrastructure as Code (IaC)
"Don't let AI hallucinate your cloud bill to $20,000."
AI agents like Devin, GitHub Copilot Workspace, and Cursor are writing Terraform and Kubernetes configs. But AI doesn't understand consequences.
| Case | What AI Wrote | Real World Impact |
|---|---|---|
| IAM Permission | Action: "s3:*", Resource: "*" |
Data Breach: Entire bucket exposed to public. |
| Network Rule | Ingress: 0.0.0.0/0, Port: 22 |
Ransomware: SSH open to the whole internet. |
| Instance Type | instance_type = "p4d.24xlarge" |
Bankrupt: $23,000/month bill for a dev env. |
- A Deterministic Verification Engine: Uses Z3 Theorem Prover to prove IAM action/resource matching, with IP and date conditions evaluated deterministically in Python.
- A Graph Analyzer: Uses NetworkX to map and verify network reachability (Reachability Analysis).
- An Artifact Boundary Gate: Scans release packages for secrets, debug artifacts, and misconfigured build paths — blocks unsafe releases before they ship.
- Deterministic: Inputs are code, output is
True/Falsewith 100% certainty. - A "Guard" Layer: Plugs into CI/CD to block AI-generated PRs that violate rules.
- A Linter: We don't just check syntax (like TFLint). We check logic.
- A Cost Explorer: We predict costs before deployment, not after you get the bill.
- Black Box AI: We don't use LLMs to verify LLMs. We use Math.
| Feature | TFLint / Checkov / TFSec | QWED-Infra |
|---|---|---|
| Approach | Regex / Static Pattern Matching | Symbolic Execution (Z3) & Graph Theory |
| IAM Logic | Can catch s3:* text match |
Proves Allow overrides Deny logically |
| Network | Checks generic "port 22 open" | Traces Internet -> IGW -> Route -> SG -> Subnet (fail-closed on NAT/NACL/peering) |
| Cost | N/A (usually distinct tools) | Deterministic Pre-Deployment Estimation |
| Accuracy | High False Positives | Deterministic Correctness |
Converts AWS IAM Policies into logical formulas.
- Wildcards: Handles
s3:Get*vss3:GetObject— proved symbolically in Z3. - Logic: Proves
Denystatements always win — proved symbolically in Z3. - Context: Verifies against specific conditions (e.g.,
aws:SourceIp,aws:CurrentTime) — evaluated deterministically in Python, with full trace in diagnostic output.
Builds a directed graph of your VPC.
- Reachability: "Can an attacker on the Internet reach my Database?"
- Path Analysis: Traces routes through Subnets and Security Groups.
- Limitations (fail-closed): NAT Gateways, VPC Peering, NACLs, and Transit Gateway are not modeled. If any are present, the guard returns
UNVERIFIABLE— the result carries no proof and must not be used for authorization decisions.
Prevents financial ruin.
- Static Catalog: Embedded prices for standard AWS resources.
- Budget Checks:
if estimated_cost > $500: Block Deployment.
Verifies release artifacts before they ship.
- Secret Scanning: Detects leaked secrets (
.env,*.token, API keys) in package files. - Debug Artifact Detection: Blocks
.coverage,.pytest_cache,__pycache__from entering packages. - Build Config Verification: Ensures
pyproject.tomlhatch build config only includes intended paths. - Fail-Closed: Unknown backends, missing configs, or unparseable files produce
BLOCKED, never a silent pass.
pip install qwed-infra(Node.js/npm SDK coming soon)
from qwed_infra import IamGuard
guard = IamGuard()
policy = {
"Effect": "Allow",
"Action": "s3:GetObject",
"Resource": "*",
"Condition": {"IpAddress": {"aws:SourceIp": "192.168.1.0/24"}}
}
# Verify: Is it accessible from the public internet?
result = guard.verify_access(
policy,
action="s3:GetObject",
resource="my-bucket",
context={"aws:SourceIp": "8.8.8.8"} # Public IP
)
print(result.allowed) # -> False (Blocked by IP)from qwed_infra import NetworkGuard
net = NetworkGuard()
infra = {
"subnets": [
{"id": "subnet-web", "security_groups": ["sg-web"]},
],
"route_tables": [
{
"subnet_id": "subnet-web",
"routes": {"0.0.0.0/0": "igw-main"},
}
],
"security_groups": {
"sg-web": {"ingress": [{"port": 80, "cidr": "0.0.0.0/0"}]},
},
}
# Is the web subnet reachable from Internet on port 80?
result = net.verify_reachability(infra, "internet", "subnet-web", port=80)
print(result.reachable) # -> True (Risk Alert!)
# Convert to structured diagnostic for CI/CD enforcement
diagnostic = NetworkGuard.to_diagnostic(result)
print(diagnostic.status.value) # -> VERIFIED / BLOCKED / UNVERIFIABLEfrom qwed_infra import CostGuard
cost = CostGuard()
resources = {
"instances": [
{"id": "gpu", "instance_type": "p4d.24xlarge", "count": 2}
]
}
result = cost.verify_budget(resources, budget_monthly=1000)
print(result.within_budget) # -> False
print(result.reason) # -> "Estimated cost $47844.20 EXCEEDS budget $1000.00"from qwed_infra import ArtifactBoundaryGuard
guard = ArtifactBoundaryGuard()
result = guard.verify_package_boundary(package_dir="qwed_infra")
# Convert to structured diagnostic for CI/CD enforcement
diagnostic = ArtifactBoundaryGuard.to_diagnostic(result)
if diagnostic.status.value == "BLOCKED":
for finding in diagnostic.developer_fields["findings"]:
print(f"❌ {finding['finding_type']}: {finding['reason']}")
else:
print("✅ Package boundary verified — safe to ship.")Q: Do I need Terraform installed?
A: No. qwed-infra parses .tf files as text using a custom HCL parser (or operates on JSON plans).
Q: Can it verify Kubernetes? A: Currently focuses on AWS Terraform. K8s Manifest verification is on the roadmap (Phase 19).
Q: Why standard pricing?
A: We use public On-Demand pricing for "Worst Case" estimation. If you have Enterprise Discounts, qwed-infra ensures you remain safe even at list price.
- ✅ v0.1.0: IAM Z3 Logic, Basic Network Graph, Static Cost Catalog. (Released Jan 2025)
- ✅ v0.2.0: Fail-closed parser + IAM, NetworkGuard CIDR fix, CI fail-open removal, diagnostic port (audit.py/InfraDiagnosticResult), CostGuard Decimal/unknown types, ArtifactBoundaryGuard. (Current)
- 🔮 v0.3.0: Docker/deployment artifact verification, K8s manifest support, Azure provider.
| Package | Description | Repo |
|---|---|---|
| qwed ☑️ | Core deterministic AI verification (Math, Logic, Code) | GitHub |
| qwed-infra ☁️ | IaC verification (Terraform, IAM, Network, Cost, Artifact) ← you are here | GitHub |
| qwed-finance 🏦 | Financial computation verification | GitHub |
| qwed-legal 🏛️ | Legal document verification | GitHub |
| qwed-tax 💸 | Tax calculation verification | GitHub |
| qwed-mcp 🔌 | Model Context Protocol verification | GitHub |
| qwed-a2a 🔄 | Agent-to-Agent verification protocol | GitHub |
| qwed-ucp 🛒 | Unified Context Protocol | GitHub |
| open-responses 🤖 | Guards for OpenAI/LangChain agent outputs | GitHub |
| qwed-learning 📚 | Educational content verification | GitHub |
When you see the Verified by QWED badge on a repository, it is a technical guarantee that:
- Deterministic Verification: The software uses symbolic solvers (Z3, graph theory) — not AI confidence scores — to prove correctness.
- Fail-Closed Architecture: If the infrastructure cannot be fully parsed or verified, it is blocked, not silently passed.
- No Silent Degradation: Every guard produces a structured diagnostic with clear status (
VERIFIED,BLOCKED,UNVERIFIABLE). Partial verification is never presented as proof.
The badge means: "We don't trust the AI. We trust the Math."
If you use qwed-infra in your research or project:
@software{dass2026qwedinfra,
author = {Dass, Rahul},
title = {QWED-Infra: Deterministic Verification for Infrastructure as Code},
year = {2026},
publisher = {GitHub},
url = {https://github.com/QWED-AI/qwed-infra}
}
Thanks to everyone building QWED. See all contributors →
| Area | What We Need |
|---|---|
| 🧪 Testing | Edge cases for guards (NetworkGuard, ArtifactBoundaryGuard) |
| 🐛 Bugs | Fix issues or report new ones |
| 📝 Docs | Improve examples and tutorials |
| 🔧 SDKs | Terraform plan JSON integration |
Apache 2.0 - Open Source.
Built by QWED-AI