Our findings said 'this bucket is public.' Users asked 'what do I change to fix it?' We derived the answer mechanically from the predicate AST — no per-rule authoring needed. Here's how counterfactual reasoning turns detection output into actionable fixes.

The finding that doesn't help

Finding: CTL.S3.PUBLIC.001
  Asset:     arn:aws:s3:::prod-assets
  Severity:  high

  DEFECT:
    The bucket's ACL grants read access to the
    AllUsers principal.

  REMEDIATION:
    Remove public access from the bucket ACL,
    or enable Block Public Access.

An engineer reading this knows what's wrong. But does not know:

• Which specific property in their configuration to change
• The current value of the property
• What value would eliminate the finding
• Whether there are multiple independent fixes (change any one)

DEFECT says "the ACL grants AllUsers read access." REMEDIATION says "remove public access." Neither tells the engineer which line to edit and what to put there.

The engineer opens the console, finds the bucket, reads the ACL, identifies the grant, figures out the fix. Per finding. Fifty times a week.

We added a DELTA section that answers the question directly:

  DELTA:
    Change: bucket ACL grantee
    Current: AllUsers
    Fix: change to any value other than AllUsers,
         or remove the grant

The engineer reads the delta, edits the configuration, re-runs. No console. No manual investigation. The finding told them what to change.

1. The delta comes from the predicate

The delta isn't authored. Nobody wrote "change bucket ACL grantee" for this control. It's derived mechanically from the same predicate that produced the finding.

Every control has a predicate — the condition it checks against observation data. For CTL.S3.PUBLIC.001, the predicate is:

storage.access.acl.grants[].grantee == "AllUsers"

This predicate has three components:

• Property path: storage.access.acl.grants[].grantee
• Operator: ==
• Value: "AllUsers"

The finding fires because the property has a value matching the predicate. The delta inverts this: what change to the property would make the predicate stop matching?

== "AllUsers"  →  "change to any value other than AllUsers"
== true        →  "set to false (disable)"
== false       →  "set to true (enable)"
contains "X"   →  "remove X from the list"
> 90           →  "reduce to 90 or below"

Each operator has a natural inverse. The inverse, applied to the observed value, is the counterfactual fix.

2. Why it's a counterfactual, not advice

The REMEDIATION field is advice. It's authored by a human who understands the vulnerability: "Remove public access from the bucket ACL." Good advice. Generic. The same text for every bucket that triggers this control, regardless of the specific configuration.

The DELTA field is a counterfactual. It's derived from the specific observation data the engine evaluated:

DELTA:
  Change: bucket ACL grantee
  Current: AllUsers          ← YOUR bucket has this now
  Fix: change to any value   ← this makes YOUR finding
       other than AllUsers      disappear

Advice says "you should probably do X." A counterfactual says "if you do X, this specific finding provably disappears." We verified this: modify the observation data per the delta's suggestion, re-run Stave, finding eliminated. The delta isn't a recommendation. It's a mechanical fact about the predicate.

This is Andreas Zeller's counterfactual causality applied to configuration: "if this value were different, the failure would not occur." The delta computes the minimal difference.

3. Walking the predicate AST

Our predicates aren't strings. They're structured trees — parsed and typed before evaluation. The derivation walks the tree, not a regex.

func DeriveDelta(pred *UnsafePredicate, observed []ObservedProperty) []DeltaPath {
    var paths []DeltaPath
    for _, clause := range pred.Misconfigurations {
        if isKindGate(clause) {
            continue // scope condition, not actionable
        }

        label := registry.Label(clause.PropertyPath)
        if label == "" {
            continue // unlabeled path, skip rather than show schema names
        }

        current := findObserved(observed, clause.PropertyPath)
        fix := invertOperator(clause.Operator, clause.Value)

        paths = append(paths, DeltaPath{
            PropertyLabel: label,
            CurrentValue:  current,
            FixAction:     fix,
        })
    }
    return paths
}

Three moving parts:

The property registry. Maps schema paths to human-readable labels. storage.access.acl.grants[].grantee becomes "bucket ACL grantee." Authored once for the observation schema (~150 hand-tuned labels), with an algorithmic fallback that handles the rest by stripping namespaces and expanding abbreviations. Covers 99.6% of controls.

The operator inverter. Maps each operator to its counterfactual phrase. == becomes "change to any value other than." contains becomes "remove from the list." > N becomes "reduce to N or below." Boolean-aware: == true becomes "set to false (disable)" not "change to any value other than true."

The observed-value lookup. Pairs each predicate clause with the actual value the engine read during evaluation. The delta shows what YOUR configuration has, not what the predicate checks in the abstract.

4. Compound predicates: independent fix paths

Simple predicates produce one delta. Compound predicates (AND) produce multiple independent fix paths:

Finding: CTL.IAM.ESCALATION.001
  Asset: arn:aws:iam::123456:role/DeployerRole

  DEFECT:
    The role grants iam:PassRole and
    lambda:InvokeFunction without resource
    constraints.

  DELTA:
    Any ONE of these changes eliminates this finding:

    1. role permissions
       Current: [iam:PassRole, lambda:InvokeFunction, ...]
       Fix: remove iam:PassRole from the list

    2. role permissions
       Current: [iam:PassRole, lambda:InvokeFunction, ...]
       Fix: remove lambda:InvokeFunction from the list

The predicate is permissions contains "iam:PassRole" AND permissions contains "lambda:InvokeFunction". Both clauses must be true for the finding to fire. Negating either one eliminates the finding. The delta shows both options; the engineer picks whichever is cheaper.

This is the practical value of walking the AST. A string-based approach would have to parse "A AND B" with regex. The AST already has the conjunction structure — each child of an AND node is an independent fix path.

5. What the derivation skips

Not every predicate clause produces a useful delta:

Kind-gates. Many predicates start with a scope condition: asset.kind == "bucket". This isn't an actionable defect — you can't "change the asset kind" to fix a security issue. The derivation filters these out. Any clause matching *.kind == value or *.type == value is a scope condition, not a delta candidate.

Parameter references. Some predicates compare against configurable thresholds: password_length < $min_length. The threshold is a parameter, not a fixed value. The delta for these would be "increase to at least $min_length" — useful but requires resolving the parameter. Skipped in the current implementation; the REMEDIATION field covers these cases with authored guidance.

Complex OR branches. AND predicates produce independent fix paths (fix any one). OR predicates require fixing all branches (any one independently triggers the finding). The rendering for "ALL of these changes are needed" is less intuitive than "any ONE." Currently skipped — OR predicates show no DELTA section and fall back to REMEDIATION.

Unlabeled property paths. If the property registry doesn't have a human-readable label for a path, the derivation skips it rather than showing raw schema names like identity.credentials.access_key.last_rotated. Schema paths in user-facing output look like implementation leaking through. Better to show nothing than to show noise.

6. Coverage without authoring

The derivation covers 672 of 675 controls. No per-control authoring. The same three inputs — property registry, operator inverter, observed values — produce deltas for every control whose predicate the AST walker can handle.

Compare with the defect description, which uses the same infrastructure:

The DELTA section reuses the property registry from defect derivation. Authoring the registry once serves both purposes. The operator inverter is ~30 lines of Go. The AST walker is shared with defect derivation.

Total new code for the delta: the inverter function and the rendering. The infrastructure was already built.

7. Verifying the counterfactual

A delta that says "change X to Y" but doesn't eliminate the finding is worse than no delta at all. The user follows the suggestion, re-runs, and the finding persists. Trust is destroyed.

We verified the counterfactual by testing it:

1. Run Stave against a fixture → finding fires, delta says "change public_read to false"
2. Modify the observation: set public_read to false
3. Re-run Stave → finding eliminated

The delta's suggestion genuinely eliminates the finding. This isn't a proof for every possible observation (the predicate logic guarantees it — negating any clause in an AND predicate makes the conjunction false), but running it confirms the derivation doesn't have bugs the logic guarantees shouldn't exist.

When to add counterfactual output

The pattern applies to any tool that evaluates conditions against data:

1. Linters that flag rule violations can show "change this token/value to eliminate the warning." The lint rule's AST encodes what it checks; the inverse is the fix.

2. Policy engines that evaluate policies against configurations can show "this policy clause fails because of this value; changing it to X makes the policy pass."

3. Compliance scanners that check controls against evidence can show "this control fails because this property is X; the control passes when the property is Y."

4. Validators that check schemas against data can show "this field fails validation because its value is X; valid values are Y."

The common prerequisite: the tool's rules must be structured (AST, typed predicates, parsed expressions) rather than opaque (arbitrary code, black-box functions). If you can walk the rule's structure, you can invert it. If the rule is a function pointer, you can't.

Reducing the Triage Time

Most security tools stop at detection. They tell you what's wrong. Some add remediation — authored advice about what to do. Very few tell you the specific, mechanically-verified change that eliminates the specific finding on your specific configuration.

The gap between "this bucket is public" and "change grants[0].grantee from AllUsers to a restricted principal" is where triage time lives. The first is a finding. The second is an action. Engineers act on actions, not findings.

The delta closes that gap without per-rule authoring. The predicate already knows what it checks. The observation already records what exists. The counterfactual is the mechanical inverse of the match. The only work is building the inversion — once — and letting it scale to every rule in the catalog.

Your security tool already knows why the finding fired. It should tell the user what to change.

The code discussed in this article is from Stave, an open-source security CLI that evaluates cloud configurations against a catalog of controls.