stave-reasoning-engines

name	stave-reasoning-engines
description	Export Stave observation facts to JSONL/SMT-LIB and derive compound cross-asset chains with Z3, Soufflé, or Prolog — detection CEL alone cannot express
triggers	["reasoning engine","Z3 / Soufflé / Prolog","compound chain detection","export-sir","graph traversal escalation","transitive closure of permissions"]
requires	["a built stave binary (run stave-setup first)","one engine — z3 (pip install z3-solver) | souffle (apt) | swi-prolog (apt)"]

stave-reasoning-engines

What this skill does

Exports Stave's raw observation properties as facts, then runs a reasoning engine to compute a multi-hop chain (e.g. user → role → admin) by tracing the specific ARN edges — not by control co-occurrence.

Time: ~30 minutes. No AWS needed (works off any observation dir).

Steps

1. Export facts to JSONL (triples)

./stave export-sir --observations <your-obs-dir> --format jsonl --eval-time 2026-01-02T00:00:00Z > facts.jsonl
grep -c '"source":"observation"' facts.jsonl    # raw observation primitives

Each line is {subject, predicate, object, source}; predicate is the dot-joined property path (e.g. identity.escalation.create_access_key.target_user_arn).

2. Export SMT-LIB and check it's well-formed

./stave export-sir --observations <your-obs-dir> --format smt2 --eval-time 2026-01-02T00:00:00Z > check.smt2
o=$(grep -o '(' check.smt2 | wc -l); c=$(grep -o ')' check.smt2 | wc -l)
[ "$o" = "$c" ] && echo "balanced ($o)" || echo "UNBALANCED"

The SMT-LIB declares binary per-path predicates ((declare-fun <path> (String String) Bool)) and is facts-only (no (check-sat)) — you append your own query.

3. Install one engine

pip install z3-solver --break-system-packages   # OR: sudo apt install souffle | swi-prolog

4. Consume the facts

• Soufflé / Prolog: turn the JSONL observation triples into observation(s,p,o) facts (the 3 fields map directly), then write rules that chain edges, e.g. escalates(U,T) :- observation(U,"identity.escalation.create_access_key.present","true"), observation(U,"identity.escalation.create_access_key.target_user_arn",T).
• Z3: append a query over the emitted binary predicates and assert the NEGATION of the chain, then (check-sat).

5. Run and interpret

• Soufflé emits a tuple → the chain is connected between those specific assets.
• Prolog proves the goal → a path was traversed.
• Z3 unsat → the chain is forced by the facts (it must exist).
• Z3 sat → not derivable (the edges don't connect).

This is graph-traversal compound detection: it fires only when the ARNs connect, which per-resource rules cannot express.

Success

You derived a compound chain from observation primitives with a reasoning engine, independent of Stave's own conclusions.