✓ Human-authored analysis; AI used for formatting and proofreading.
We ran an experiment. We took a security question — "can an unauthenticated principal reach a sensitive resource?" and wrote specifications for five different reasoning engines: Z3 (SMT solver), Soufflé (Datalog), Clingo (Answer Set Programming), SWI-Prolog, and PRISM (probabilistic model checking).
Then we gave each spec to an AI agent with no access to our source code. Just the spec YAML, the exported facts from a configuration snapshot, and the export schema. No Go source, internal documentation or prior context about the tool.
The agent produced correct security reasoning in all five paradigms. That result is about architecture.
The spec as the contract
Each reasoning spec is a YAML file with a fixed structure:
trial:
engine: souffle
question: >
How many assets are anonymously reachable via
self-registration or privilege-escalation paths?
input: input.facts
export_schema: sir-predicates.md
reasoning_steps:
- Load the JSONL facts into Soufflé relations
- Apply the reachability rules from reachability.dl
- Count tuples in the anonymous_reachable relation
expected_output:
anonymous_reachable_count: 12
validation:
method: exact_match
ignore:
- output_ordering
- whitespace
The spec is simultaneously three things: a specification (what the engine should compute), an implementation guide (how to compute it), and a test definition (the correct answer). The golden output in expected_output is committed alongside the spec and diffed against the agent's output.
This means contributing a new security analysis doesn't require reading our Go codebase. A contributor writes a spec, commits the golden output, and the trial framework validates it. The spec is the interface. The source code is an implementation detail behind it.
What the trials found
Five trials. Three passed on first run. Two failed. The failures were more informative than the passes.
Z3 (SMT): pass. The agent translated the JSONL facts into SMT-LIB assertions, ran (check-sat), and produced the correct verdict and witness. The question is a satisfiability problem. Can an unauthenticated principal read an S3 bucket with Public Access Block disabled. Z3 either finds a satisfying assignment (the specific principal and bucket) or proves none exists. The agent found the right one.
Soufflé (Datalog): pass. The agent loaded facts into relations, applied reachability rules, and counted 12 anonymously reachable assets. Byte-identical to the golden output. Datalog's strength here is transitive closure — role assumption chains of arbitrary depth are computed by fixed-point evaluation, not by bounded loops.
Clingo (ASP): fail, then pass. The agent's output didn't match the golden because the spec used mfa_enforced but the exported facts used has_mfa_enforced. This was a spec bug. A naming-convention slip where the spec author forgot the has_ prefix that Stave's fact catalog uses for all boolean predicates.
The fix was two lines: correct the predicate name in the spec and add an explicit note about the naming convention. When we re-ran with a blind agent (fresh context, no knowledge of the fix), the agent picked up the convention note and produced correct output.
This is the kind of defect a trial framework should catch. The spec was wrong. The engine was right. The framework distinguished between the two.
Prolog: fail, then pass. The agent's output was correct. 12 proof chains, but the golden said 6. The spec author had transcribed the golden by hand and missed the DynamoDB action variants that create a cartesian product with the Cognito identity pool paths. The trial framework caught this by comparing the agent's output against the engine's actual output (12) rather than trusting the golden.
Category A failure (Clingo): spec bug — agent couldn't derive engine output from spec. Category C failure (Prolog): golden bug — agent's output matched engine, but golden was wrong. The distinction is foundational. In Category A, you fix the spec. In Category C, you fix the golden. Conflating the two means you can't trust your test suite.
PRISM (probabilistic): pass. The agent computed per-attack-shape exploitation probabilities from the PRISM model. Step probabilities were exact. Aggregate probability was within ±0.005 of the golden. PRISM is the most unusual engine in the set. It doesn't prove safety, it quantifies risk. "Given this configuration, the probability of successful exploitation via the Cognito self-registration path is 0.342." That's a different kind of output than SAT/UNSAT, and the spec format handles it properly.
The blind re-run
The original trials had a methodological weakness: the spec author and the trial runner were in the same session. The agent might have been influenced by context from the authoring process.
So we re-ran the two trials that had spec changes (Clingo and Prolog) with a fresh sub-agent. No prior context, knowledge of the original failures or fixes. Just the corrected spec YAML, the input facts, and the export schema.
Both passed.
The Prolog blind agent derived 12 proof chains via the cartesian product, matching the post-fix golden count—all without seeing the explanation comment in the spec.
It independently discovered the same combinatorial structure the original agent had found.
The Clingo blind agent correctly used has_mfa_enforced with the has_ prefix. The naming-convention note in the spec was sufficient for a context-free agent to recover the convention.
The blind run also surfaced two non-issues: output ordering and indentation width. Both were already in the spec's ignore: list — confirming that the ignore directives are doing their job of preventing false failures on cosmetically different but semantically correct output.
Five paradigms, one contract
Each engine answers a different kind of question about the same configuration snapshot:
| Engine | Paradigm | Question shape | Output |
|---|---|---|---|
| Z3 | SMT | "Is it possible for X?" | SAT/UNSAT + witness |
| Soufflé | Datalog | "What can reach what?" | All reachable tuples |
| Clingo | ASP | "Which assets violate which rules?" | Violation atoms |
| Prolog | Logic | "Prove the chain from A to B" | Proof trees |
| PRISM | Probabilistic | "How likely is exploitation?" | Risk probabilities |
The input to all five is the same: Stave's JSONL fact export from a single configuration snapshot. The export contract — has_action(arn, action), trusts_service(arn, service), has_tag(arn, key, value) — is the stable interface. Each engine consumes the same facts in its native format.
This is the architectural boundary the trials validated: Stave's export contracts are complete for five reasoning paradigms. No engine reported a missing input field. Every engine produced correct output from the exported facts alone. The contract layer is tested, not asserted.
What this means for contributors
The reasoning-specs directory is open. The steps for adding a new security analysis:
- Pick a security question and a reasoning engine.
- Write a spec YAML: the question, the reasoning steps, the expected output.
- Commit the golden output.
- Run the trial. If it passes, the analysis is validated. If it fails, the framework tells you whether the bug is in the spec, the golden, or the engine.
No Go source code required. The spec references the export schema (which predicates are available, what they mean) and the input facts (a JSONL file from any Stave snapshot). A contributor who knows Z3 but not Go can write an SMT-based analysis. A contributor who knows Prolog but not cloud security can implement a proof-chain analysis from a well-written spec.
Several engines don't have trial packages yet; PySAT, TLA+, game theory, STIX, JSON-LD/GraphML, OSCAL/OCSF, and compliance evidence packs are all open for contribution. The spec format is documented. The trial framework is committed. The export facts are stable.
The prerequisite is a working example with a committed, fixture-tied golden output. The spec wraps the example. The trial validates the spec. The blind re-run validates the trial. Each layer adds confidence without requiring access to the layer below it.
Stave is an open-source cloud security reasoning engine. The reasoning-specs trials, input fixtures, and export schemas are at stave.
Top comments (0)