Status
What's built, what's still shaping, and what this project deliberately does not attempt — stated plainly rather than left to be inferred from the rest of the site.
What exists today
| Capability | Status |
|---|---|
| Typed fact and proposition model | Available |
| SMT-backed classification (five verdicts) | Available |
| Coverage, decision, and invariant analyses | Available |
| Counterexamples, witnesses, unsat cores | Available |
| Explanation DAG + rendering | Available |
| Rust derivation and explanation backends | Available |
| Cross-language wire IR (Python + Rust clients) | Available |
| User-authored dimension families | Available |
| Numeric, string, and bool carriers (all four) | Available |
| Machine-checked core arithmetic (Kani + Verus, full domain; independent Lean cross-check, 2 of 4 branches) | Available |
| Mechanically enforced Z3 solver boundary | Available |
Builder/orchestration surface (agent/graph/subgraph/subject) |
Experimental |
| Framework dialect analysis — LangGraph, pydantic-graph | Experimental |
| Framework dialect analysis — LlamaIndex, Burr, Haystack | Proposed |
| Textual (Python-subset) authoring surface | Proposed |
| Deterministic guard generation | Planned |
| Agent-tooling integration | Proposed |
Available means shipped, tested, and exercised by this site's own examples —
the verdict table and provenance graph on the front page and every
result block on the guardrails page are generated by running
the real analyses during this site's build, and each is independently pinned by
a test, so none of them can drift from the implementation without failing the
suite. Experimental means the mechanism works but its surface (naming,
exact method shapes) is still expected to change — and, for the framework
dialects, that the coverage is narrower than the idea: two frameworks are
read today, and a file from any other is reported unrecognised rather than
clean. Proposed and Planned
are not yet built; nothing on this site describes them in the present tense.
Direction
Two threads are moving in parallel. The first is deepening the typed authoring
surface itself — the agent/graph/subgraph/subject builders are
functionally complete but still being reshaped, and a textual, Python-subset
authoring surface is proposed on top of the same underlying IR, not a
replacement for it. The second is runtime independence: the long-term goal is
to compile analysed, validated rules into deterministic guards that carry no
solver dependency at all, so the SMT solver's role stays confined to analysis
time. Neither thread is complete; both are visible in the status table above
rather than described as finished.
Non-goals
- Verdicts are relative to the declared model, not to the deployed system.
Nothing here checks that a
VERIFIEDconclusion about the rule model matches what a running application actually does. That connection — checking generated or hand-written implementation code against the model — is intent, not a shipped capability. - No attempt at real set or bag reasoning. The string carrier's vocabulary checking is a finite disjunction of equalities, not general membership or multiset arithmetic; nothing here reasons about unbounded collections symbolically.
- No claim to beat established policy or verification systems on their own ground. This project sits closer to typed embedded authoring with dimensional units and provenance-preserving explanation than to a general policy engine or a general-purpose theorem prover, and it does not claim superiority over either category — only a different combination of properties.
- No install or quickstart path yet. There is no package published for installation; working with this project today means cloning the source.
See also
The front page for the worked example and the five-verdict model · Guardrails for coverage, decision and invariant analysis · How reasoning works for the explanation graph and classification model.