Z3 Can Prove Your Cloud is Unsafe. It Can't Tell You Why.

Z3 is one of the most powerful reasoning engines ever built. Microsoft Research created it to verify chip designs and flight software. It can take your cloud configuration, model it as a set of logical assertions, and mathematically prove whether an attack path exists.

Z3 says when it finds one:

sat

Three letters. No context. No explanation. No link to the configuration property that caused it. No fix. Just "sat" — which means "satisfiable," which means "the unsafe state you asked about is reachable," which means your cloud is vulnerable. Probably. If you encoded the question correctly. Which you can't verify from the output.

This is the gap between a powerful engine and a useful tool. The engine answers the question. The tool explains the answer. This article explains why the explanation layer matters more than the engine, and what it looks like in practice.

What Z3 outputs

Let's say you want to check whether an anonymous internet user can read PHI data from an S3 bucket through a Cognito identity pool. You model the configuration as SMT-LIB assertions, write a query, and run it through Z3.

The input Z3 sees:

(set-logic ALL)
(declare-fun allows_unauthenticated (String String) Bool)
(declare-fun maps_unauth_to (String String) Bool)
(declare-fun has_action (String String) Bool)
(declare-fun has_tag (String String) Bool)

(assert (allows_unauthenticated "pool-abc" "true"))
(assert (maps_unauth_to "pool-abc" "role/AppUnauthRole"))
(assert (has_action "role/AppUnauthRole" "s3:GetObject"))
(assert (has_tag "bucket-prod-phi" "data_classification:phi"))

(declare-const principal String)
(declare-const action String)
(declare-const resource String)

(assert (allows_unauthenticated principal "true"))
(assert (has_action principal action))
(assert (has_tag resource "data_classification:phi"))

(check-sat)
(get-model)

The output Z3 produces:

sat
(
  (define-fun principal () String "pool-abc")
  (define-fun action () String "s3:GetObject")
  (define-fun resource () String "bucket-prod-phi")
)

In SMT-LIB, sat means the forbidden state is reachable. The model names the specific pool, action, and bucket. The proof is mathematically sound.

If you're a security engineer who just wants to know whether your Cognito configuration is safe, this output is useless. You have three questions:

1. Is this result correct? Did the input assertions match your configuration, or did the translation introduce a bug?
2. What does it mean? Which specific settings in which specific files create the vulnerability?
3. What do I do about it? What's the fix, what does it cost, and how do I verify it worked?

Z3 answers none of these. It answered the math question. The security question is still open.

The two translation boundaries

Between your cloud configuration and Z3's answer, there are two translation steps. Each can introduce bugs. Each is invisible if you only look at the solver's output.

YOUR CLOUD CONFIG          THE MATH              YOUR ANSWER

  S3 bucket policy    →    SMT-LIB assertions    →    "sat"
  IAM role policy          (was the translation        (was the translation
  Cognito settings          correct?)                   back to cloud
                                                        terms correct?)

  ENCODING BOUNDARY        Z3 SOLVER              DECODING BOUNDARY
  (can have bugs)          (trusted)              (can have bugs)

Encoding bugs: Your S3 bucket has PublicAccessBlock.BlockPublicPolicy = true, but the translation emits has_public_read "bucket" "true". The assertion is wrong — the bucket is private, but Z3 thinks it's public. Z3 faithfully returns sat based on the wrong input. The "vulnerability" doesn't exist. You can't tell from sat that the encoding was wrong.

Decoding bugs: Z3 returns sat with a model. You read the model and conclude "the bucket is directly accessible from the internet." But the actual path is through the Cognito identity pool, not direct access. The model told you which variables were assigned, but the interpretation of those variables — what they mean in cloud terms — is your responsibility. Misread the model, misunderstand the vulnerability.

The solver is the most reliable component in the pipeline. The translation layers are where the bugs hide. And they're the layers that get the least attention because everyone focuses on the solver.

What an orchestration layer provides

An orchestration layer wraps the solver with five capabilities that make the answer trustworthy, traceable, and actionable:

1. Encoding explanation — "Did the tool understand my configuration?"

Before the solver runs, you see what the tool extracted from your configuration, in your language:

Configuration Summary: 7 assets, 43 facts extracted

Asset: arn:aws:s3:::prod-phi (S3 Bucket)
  ├── Public read access: ENABLED
  │   Source: prod-phi-bucket.obs.json → access.public_read
  │   Fact: a3f8c2e91b04
  │
  ├── Encryption: AES256 (SSE-S3, not KMS)
  │   Source: prod-phi-bucket.obs.json → encryption.algorithm
  │   Fact: b7d1e4f03c89
  │
  └── Data classification: PHI
      Source: prod-phi-bucket.obs.json → tags.data_classification
      Fact: c9e2a1f04d77

Asset: arn:aws:cognito-identity:...:identitypool/abc (Identity Pool)
  ├── Unauthenticated access: ALLOWED
  │   Source: cognito-pool.obs.json → identity.access.allow_unauthenticated
  │   Fact: d4e5f6a7b8c9
  │
  └── Maps unauthenticated users to: arn:aws:iam::111122223333:role/AppUnauthRole
      Source: cognito-pool.obs.json → identity.cognito.unauth_role_arn
      Fact: e5f6a7b8c9d0

No SMT-LIB. No predicate names. "Public read access: ENABLED" — the security engineer compares this to their mental model of the bucket. If the bucket is private, the encoding is wrong and the engineer knows before the solver runs.

Every fact has a unique identifier and a traceable source showing which file and which property path produced it. This is the audit trail. When the solver's answer doesn't match expectations, the engineer traces the identifier back to the source and checks whether the encoding was correct.

2. Human verdict — "What does the result mean?"

After the solver runs, you see the answer in security language:

VERDICT: UNSAFE

An anonymous internet user can read PHI data from the prod-phi
bucket through the Cognito identity pool.

The forbidden state is reachable because:
  1. Identity pool allows unauthenticated access
     (cognito-pool.obs.json → identity.access.allow_unauthenticated = true)
  2. Unauthenticated users receive credentials for AppUnauthRole
     (cognito-pool.obs.json → identity.cognito.unauth_role_arn)
  3. AppUnauthRole has s3:GetObject permission
     (iam-role.obs.json → policies.attached_policies[0].Action)
  4. Target bucket contains PHI
     (prod-phi-bucket.obs.json → tags.data_classification = phi)

Not sat. Not a model with define-fun expressions. A four-step chain in plain English, each step linked to a specific file and property path. The security engineer reads it and knows exactly which settings create the vulnerability and where they live.

3. Fix guidance — "What do I do about it?"

FIX: Disable unauthenticated access on the identity pool.

  aws cognito-identity update-identity-pool \
    --identity-pool-id us-east-1:abc123 \
    --no-allow-unauthenticated-identities

  Cost: $0. Time: 30 seconds.
  Effect: Breaks the chain at step 1.

VERIFICATION: After applying the fix, re-run the analysis.
  Expected result: SAFE
  (Z3 returns UNSAT — no assignment of principals, actions,
  and resources can satisfy the attack path conditions.)

The fix is a shell command. The cost is quantified. The effect names the specific chain step that breaks. The verification tells the engineer what to expect and explains the solver's output in cloud terms.

4. Traceability — "Which property caused this?"

Every step in the verdict traces back to a specific property in a specific file through a unique identifier:

# The verdict says step 1 caused the chain.
# Trace identifier d4e5f6a7b8c9:

grep "d4e5f6a7b8c9" facts.jsonl

# Returns:
# fact_id: d4e5f6a7b8c9
# subject: pool-abc
# predicate: allows_unauthenticated = true
# source: cognito-pool.obs.json
# property: identity.access.allow_unauthenticated
# captured: 2026-05-01T00:00:00Z

One identifier. One grep. Full trace from the verdict to the configuration property, including when the snapshot was taken. No manual correlation across output files.

5. Encoding verification — "Can I trust the translation?"

The orchestration layer verifies its own encoding by comparing each extracted fact against the raw configuration:

Encoding verification: 43/43 facts verified ✓

Every extracted fact matches the corresponding property
in the observation file. The solver's input is consistent
with the configuration snapshot.

Or, when there's a bug:

Encoding verification: 41/43 facts verified

MISMATCH:
  Fact d4e5f6a7b8c9:
    Extracted: allows_unauthenticated = "true"
    Observation: identity.access.allow_unauthenticated = "false"
    File: cognito-pool.obs.json
    → ENCODING BUG: fact says unauthenticated is allowed,
      but the configuration says it's disabled.
      The UNSAFE verdict may be incorrect.

No other tool in the market verifies its own translation layer. The security engineer doesn't need to read SMT-LIB to trust the result — the tool proves its encoding is correct, or reports where it is wrong.

What you get without orchestration vs. with it

Capability	Z3 alone	With orchestration
Prove an attack path exists	sat	UNSAFE: anonymous user can read PHI data
Explain which settings cause it	Read the SMT-LIB model	Four-step chain with file names and property paths
Verify the encoding is correct	Manually review assertions	Automated: 43/43 facts match observations
Trace the finding to a file	Grep through comments	One identifier, one grep, full trace
Get the fix	Derive it from the model	Shell command, cost, time, expected result
Run multiple solvers	Reformat per solver	Same input, three solvers, consensus
Explain to an auditor	Show them SMT-LIB	Show them the chain in English with evidence

The right column is the product. The left column is a math library. Security engineers don't need a math library — they need trustworthy answers in their language.

Why this matters more for compound detection

The orchestration layer is most valuable when the analysis spans multiple services. A single-service check ("is this bucket public?") is simple enough to verify manually. A cross-service check ("can an anonymous user reach PHI data through a chain of Cognito → IAM → S3?") involves three services, three configuration files, and dozens of properties.

The encoding has more places to be wrong. The verdict has more steps to explain. The traceability has more links to follow.

This is where raw solver output becomes dangerous. If Z3 returns sat on a three-service chain and the encoding has a bug in the IAM layer, the finding is a false positive. The security team triages it as critical, burns two sprints investigating, and discovers it was caused by a property path error in the translation code. The encoding verification catches that error before the solver runs.

If Z3 returns unsat and the encoding has a bug — a property that should be true was encoded as false — the finding is a false negative. The team thinks they're safe. They're not. The encoding verification catches that too.

The more complex the analysis, the more valuable the translation layer. Single-service checks can tolerate raw solver output. Cross-service compound detection cannot.

The bottom line

Don't evaluate formal verification tools by which solver they use. Z3, cvc5, and Yices all produce correct answers to the questions they're asked. The question is whether the question was asked correctly and whether the answer is translated back to your language.

Don't accept sat as an answer. Accept "UNSAFE: an anonymous internet user can read PHI data from the prod-phi bucket through the Cognito identity pool, caused by these four settings in these three files, fixable with this one command for $0 in 30 seconds, verified by three independent solvers, encoding confirmed correct against 43 observation properties."

That's an answer. sat is a data point.

---

The orchestration layer described in this article is implemented in Stave, an open-source static analysis tool that evaluates cloud configurations via CEL predicates and exports standardized facts for consumption by nine independent reasoning engines. The encoding explanation, verdict translation, traceability, and encoding verification are built on Stave's fact_id provenance chain — every fact carries a deterministic identifier linking the solver's input to the specific observation file and property path that produced it. All analysis runs on air-gapped snapshots with no cloud credentials required.