Find the cases your rules don't decide.
Guardrail Calculus is a typed language and analysis system for domain rules. It proves what follows from your rules, refutes what contradicts them, and — the part that matters — hands back the exact input that no rule decides, along with the reasoning behind every verdict.
See a worked example · How the analysis works
An independent engineering project by Ellis Breen — source, architecture notes and API reference below.
A worked example
Four subjects, four checks, three different verdicts — all produced by a solve during this site's own build, not typed into this page.
Given:
- Avery departs at 06:20.
- Drew departs eight hours before 17:30.
- Blake departs one hour before Drew.
- Casey's departure is not stated.
| Check | Proposition | Verdict |
|---|---|---|
| B | Blake departs when Avery does | FALSIFIED |
| C | Blake departs at 08:30 | VERIFIED |
| D | Blake departs after Avery | VERIFIED |
| E | Casey's 8-hour journey ends by 15:20 | UNKNOWN |
E is the one to look at closely. Casey carries no given, so the rule set
genuinely does not decide it — that is UNKNOWN
(contingent: both the claim and its opposite are consistent with what's known),
not UNDECIDED (the backend gave up). The two read
the same in English; the system keeps them apart.
Drew departs eight hours before 17:30, therefore Drew departs at 09:30. Blake departs one hour before Drew, therefore Blake departs at 08:30. Every verdict above keeps the givens and derivation steps that justify it.
The excerpt below is the real authoring surface — @ is symbolic equality, not
Python's ==:
blake = (
subject()
.given(
(_.departure @ (r.drew.own.departure - duration_hours(1))).annotate(
"Blake departs one hour before Drew."
)
)
.check("C", (_.departure @ clock_from_hhmm(830)).annotate("Blake departs at 08:30."))
.block()
)
See the complete executable example →
Rules are scattered across code, prose and tests
The rules that matter most in a system rarely live in one place. A transaction must not exceed its limit. A workflow may advance only when its prerequisites hold. Two states must never coexist. These end up spread across conditionals, validation functions, database constraints, policy documents and tests — each of which checks its own corner and none of which can answer for the whole.
Tests exercise selected cases. Types exclude some invalid representations. Runtime checks reject individual operations. None of the three establishes that the rule set, taken as a whole, is coherent or complete.
Guardrail Calculus asks the question directly: are the assumptions consistent? Does this conclusion follow? Is its opposite also possible? Is some input region left unhandled? And why did the system decide as it did?
More precise than pass or fail
For any proposed conclusion, Guardrail Calculus distinguishes:
VERIFIED— the conclusion follows from the facts.FALSIFIED— the conclusion contradicts the facts.UNKNOWN— both the conclusion and its negation remain possible. A genuine gap, not a failure.INCONSISTENT_BASE— the premises contradict each other, so no reliable conclusion can be drawn.UNDECIDED— the current reasoning backend could not determine the result. Reported honestly, not guessed.
These are four semantically distinct outcomes and one honest abstention. Collapsing them into a Boolean throws away the distinction between a conclusion that holds, a wrong rule, an incomplete rule set, contradictory inputs and an unsupported analysis.
A check is classified by asking two questions against the base facts: is the check satisfiable, and is its negation satisfiable (refutable)?
| Satisfiable | Refutable | Verdict |
|---|---|---|
| yes | no | VERIFIED |
| no | yes | FALSIFIED |
| yes | yes | UNKNOWN |
| no | no | INCONSISTENT_BASE |
If the solver cannot decide either question, the verdict is
UNDECIDED — see
how reasoning works for the full classification model.
Guardrails over a whole rule set
This is not a puzzle solver. Three analyses run over the same solver primitive, each returning a counterexample rather than a bare verdict:
| Analysis | Question | Returns |
|---|---|---|
| Coverage | Does every input route somewhere? | total, plus a witness input inside any gap |
| Decision | Can two guards in an ordered table both fire, and can any never fire? | overlapping pairs with the input that fires both; unreachable guard indices |
| Invariant | Does this transition preserve its obligation? | preserved, plus a violating state when it does not |
A concrete case: a triage table routes tickets on amount and on intent. A £15,000 refund matches both the escalation guard (amount) and the billing guard (intent) — the decision analysis returns that exact ticket as an overlap. This is what makes the case for agent-generated software concrete: an LLM picks the next node non-deterministically, and the guardrail is a separately verified symbolic layer proving the routing stays total, unambiguous and state-safe regardless of what the model chose.
The aim is not a more trustworthy agent. It is a smaller trusted surface — constraints authored and analysed independently of whatever implementation produces the behaviour. Guardrail Calculus does not today check generated code against the model; that connection is intent, not a shipped capability.
See the coverage, decision and invariant analyses worked in full →
Analyse with a solver. Run without one.
Analysis uses an SMT solver to detect contradictions, prove and refute propositions, find undecided regions, and produce provenance-backed explanations. The intended runtime is ordinary deterministic guards — no solver service, no solver latency, no solver dependency in the deployed application.
Typed authoring API
↓
Constraint and provenance IR
↓
Analysis and derivation
↓
Verdicts + explanation graph
↓
Deterministic runtime guards [planned — not built]
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 |
| Textual (Python-subset) authoring surface | Proposed |
| Deterministic guard generation | Planned |
| Agent-tooling integration | Proposed |
Not goals. Verdicts are relative to the declared model, not to whatever the deployed system actually does — nothing here checks that the two match. There is no attempt at real set or bag reasoning. This project does not claim to beat established policy or verification systems on their own ground.
Full status, direction and non-goals →
About
Guardrail Calculus is an independent engineering project by Ellis Breen: language tooling, cross-language systems, type-safe APIs, constraint solving, static analysis, formal verification (Kani, Verus, Lean), Python and Rust, property-based testing.