Skip to main content

Deterministic Verification for Infrastructure as Code (IaC) using Z3 and Graph Theory.

Project description

QWED Logo

☁️ QWED-Infra

Deterministic Verification for Infrastructure as Code (IaC)

"Don't let AI hallucinate your cloud bill to $20,000."

Verified by QWED PyPI License Python 3.10+ GitHub stars GitHub Developer Program

Sponsor QWED on GitHub

Twitter LinkedIn


🚨 The Problem

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.

💡 What QWED-Infra Is (and Isn't)

✅ QWED-Infra IS:

  • 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/False with 100% certainty.
  • A "Guard" Layer: Plugs into CI/CD to block AI-generated PRs that violate rules.

❌ QWED-Infra is NOT:

  • 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.

🆚 How We're Different

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

🛡️ The Four Guards

1. IamGuard (The Security Math)

Converts AWS IAM Policies into logical formulas.

  • Wildcards: Handles s3:Get* vs s3:GetObject — proved symbolically in Z3.
  • Logic: Proves Deny statements 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.

2. NetworkGuard (The Topology Graph)

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.

3. CostGuard (The Budget Enforcer)

Prevents financial ruin.

  • Static Catalog: Embedded prices for standard AWS resources.
  • Budget Checks: if estimated_cost > $500: Block Deployment.

4. ArtifactBoundaryGuard (The Release Gate)

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.toml hatch build config only includes intended paths.
  • Fail-Closed: Unknown backends, missing configs, or unparseable files produce BLOCKED, never a silent pass.

📦 Installation

pip install qwed-infra

(Node.js/npm SDK coming soon)


⚡ Usage Examples

Verify IAM Policies

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)

Verify Network Reachability

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 / UNVERIFIABLE

Enforce Budget

from 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"

Verify Package Boundary

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.")

❓ FAQ

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.


🗺️ Roadmap

  • 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.

🌐 QWED Ecosystem

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

🛡️ What Does "Verified by QWED" Mean?

When you see the Verified by QWED badge on a repository, it is a technical guarantee that:

  1. Deterministic Verification: The software uses symbolic solvers (Z3, graph theory) — not AI confidence scores — to prove correctness.
  2. Fail-Closed Architecture: If the infrastructure cannot be fully parsed or verified, it is blocked, not silently passed.
  3. 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."


⭐ Star History

Star History Chart


📄 Citation

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}
}

👥 Contributors

Rahul Dass

Thanks to everyone building QWED. See all contributors →


🙏 Contributors Wanted

Good First Issues

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

→ Read CONTRIBUTING.md


📄 License

Apache 2.0 - Open Source.

Safe Infrastructure is Scalable Infrastructure.
Built by QWED-AI

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

qwed_infra-0.2.0.tar.gz (62.1 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

qwed_infra-0.2.0-py3-none-any.whl (34.9 kB view details)

Uploaded Python 3

File details

Details for the file qwed_infra-0.2.0.tar.gz.

File metadata

  • Download URL: qwed_infra-0.2.0.tar.gz
  • Upload date:
  • Size: 62.1 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/6.1.0 CPython/3.13.7

File hashes

Hashes for qwed_infra-0.2.0.tar.gz
Algorithm Hash digest
SHA256 49b5c6480cc671588ea779323749cf45f799c6aaa64e514ebab71c57956061c5
MD5 9c5c5744bf72271df51df78388803f19
BLAKE2b-256 d60e1eae3abe4d64cbe64d98c79bca363a2baecdcd5a1d96743aed46ce8add91

See more details on using hashes here.

Provenance

The following attestation bundles were made for qwed_infra-0.2.0.tar.gz:

Publisher: publish.yml on QWED-AI/qwed-infra

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file qwed_infra-0.2.0-py3-none-any.whl.

File metadata

  • Download URL: qwed_infra-0.2.0-py3-none-any.whl
  • Upload date:
  • Size: 34.9 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/6.1.0 CPython/3.13.7

File hashes

Hashes for qwed_infra-0.2.0-py3-none-any.whl
Algorithm Hash digest
SHA256 5ebe3279ac982f36b33a0a1bc370e07bc7155260d53863e18b46f45af3c72c2e
MD5 22f8c98dc54827a9adc09b222e72e949
BLAKE2b-256 15d460f2491b9af02edf2610ce878ce61061cc7f0faa9ac24ca1cd022a28a263

See more details on using hashes here.

Provenance

The following attestation bundles were made for qwed_infra-0.2.0-py3-none-any.whl:

Publisher: publish.yml on QWED-AI/qwed-infra

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page