TRIEL

Specifications are compilable. Invariants are provable.

LTL/CTL as language primitives. Not library calls.

TRIEL v2.4

1SPECIFICATION agent_budget_guard VERSION 1.0.0
2    JURISDICTION "INTERNAL"
3
4SUBJECTS {
5    AI_Agent : SYSTEM
6}
7
8TERMS {
9    ON api_call(cost) DO
10        AI_Agent MUST_NOT exceed_budget WHEN cumulative_spend > budget_cap
11}
12
13FACTORS {
14    cumulative_spend : Decimal POLARITY 1.0 SOURCE agent_ledger,
15    budget_cap : Decimal POLARITY -1.0 METADATA
16}
17
18INVARIANTS {
19    budget_never_breached : SAFETY : ALWAYS (cumulative_spend <= budget_cap)
20}

LINES: 20 | INVARIANTS: 1 | JURISDICTION: INTERNAL

SCENARIO PARAMETERS

budget_cap:

METADATA factors receive values from outside the specification. State switching here is a static lookup over precomputed results, not a live compile.

VERIFICATION OUTPUTSATISFIED

INVARIANT HOLDS

sha256:9f2c41b8e0a7d35c6b1e84f097aa2d3e5c7b90d1f4a62e8c03b57d9ae14c6b28

SATISFIED | Proof size: 6 nodes | Time: 12ms

Timings, proof sizes and hashes shown here are illustrative example values, not measured benchmarks.

English leaves loopholes. TRIEL leaves proofs.

NATURAL LANGUAGE SPECIFICATION

The agent shall promptlyNo bound. One second or one quarter both satisfy this word. halt spending once a significantNo threshold, no unit, no comparison operator. portion of the budget is consumed, provided the amount remains within reasonableUndefined predicate. Resolved by argument, not by evaluation. operating limits.

Hover the underlined terms. Each one is a place where two implementations can disagree and both remain compliant.

TRIEL FRAGMENT

✓INVARIANTS {
✓    budget_never_breached : SAFETY : ALWAYS (cumulative_spend <= budget_cap)
✓}

Every clause is a checkable predicate over states and paths. Disagreement becomes a counterexample, not a discussion.

TEMPORAL LOGIC (LTL/CTL)

ALWAYS, EVENTUALLY — first-class invariants, not assertion libraries

EVENT-DRIVEN MODEL

Subjects, obligations (MUST/MAY/MUST_NOT), factors — a specification ontology

ZERO-KNOWLEDGE NATIVE

PROVES ... WITHOUT REVEALING — a language construct, not an external framework

OPEN SOURCE

Open Web Foundation Agreement 1.0. Grammar at github.com/triel-lang/grammar

Star us on GitHub →—Questions or feedback? Open an issue on GitHub →