TRIEL: a specification language where compliance rules compile into cryptographic artifacts

Software specifications and their implementations tend to drift apart over time. A specification is written once; the implementation is built, maintained, and modified separately — and the two slowly diverge. This gap is a routine source of costly failures, compliance issues, and audit findings, not just a documentation nuisance.

TRIEL is an open specification language that treats specification-to-implementation translation as the point where correctness evidence should be generated — not recovered afterward through separate testing or review.

What it looks like

Here's the actual hello_triel.triel from the repository — not a simplified stand-in:

SPECIFICATION hello_triel VERSION 1.0.0

SUBJECTS {
  alice : PARTY,
  bob   : PARTY
}

TERMS {
  alice MUST send_greeting
}

FACTORS {
  greeting_sent : Boolean METADATA SOURCE alice
}

INVARIANTS {
  greeting_happens : LIVENESS : EVENTUALLY(greeting_sent == true)
}

Subjects, obligations (MUST / MAY / MUST_NOT), factors, and invariants — that's the core vocabulary. Invariants can express both safety properties (ALWAYS) and liveness properties (EVENTUALLY, with an optional WITHIN deadline), backed by full LTL/CTL temporal logic underneath.

Where it gets more interesting: zero-knowledge constraints

TRIEL has native zero-knowledge predicates built into the type system. Here's a real example from the repo — an EUDI Wallet–style driving license credential:

-- TRIEL example: EUDI Wallet driving license — issuance and presentation policy
-- Demonstrates: conditional obligations, ZK age predicate, prohibition on stale credentials
SPECIFICATION eudi_driving_license VERSION 1.0.0
    STANDARD "ISO-18013-5", "eIDAS-2.0"
    JURISDICTION "EU"
SUBJECTS {
  applicant : PARTY,
  issuer    : REGULATOR,
  verifier  : PARTY
}
FACTORS {
  age                       : ZK<Integer> PROVES(self >= 18) WITHOUT REVEALING self
                              METADATA SOURCE applicant,
  vision_correction_needed  : Boolean METADATA SOURCE issuer,
  license_category          : String  METADATA SOURCE issuer,
  license_valid             : Boolean METADATA SOURCE issuer MAX_AGE 24 HOURS
}
TERMS {
  applicant MUST submit_proof(age) BY DATETIME("2026-09-01T00:00:00Z");
  IF vision_correction_needed THEN
    issuer MUST attach_restriction("corrective_lenses")
  ELSE
    issuer MAY issue_unrestricted_category;
  verifier MUST_NOT accept_presentation WHEN license_valid == false
}
INVARIANTS {
  license_requires_adult_holder       : SAFETY : ALWAYS(age >= 18);
  presentation_requires_valid_license : SAFETY : ALWAYS(license_valid == true)
}

age : ZK<Integer> PROVES(self >= 18) WITHOUT REVEALING self declares a field where the predicate ("at least 18") is checkable without exposing the underlying value. Combined with conditional obligations and a prohibition on stale credentials, this one spec captures a fairly realistic identity-verification policy — the kind of thing that today usually lives split across legal text, a compliance checklist, and application code that may or may not match either.

Where it sits relative to existing tools

vs. OPA/Rego: Rego evaluates structured queries at a perimeter — admission control, gateways. It's decoupled from the cryptographic execution layer and can't reach into an MPC circuit or a ZK pipeline. TRIEL expresses compliance constraints at the data-field level, so they can compile into the cryptographic artifacts themselves, not be enforced from outside.

vs. Wysteria/Wys*: these are rigorous languages for secure multiparty computation, built for cryptographers who already understand type theory and principal-splitting. TRIEL is aimed the other direction — non-cryptographers (compliance officers, analysts) writing and auditing declarative invariants, with low-level cryptographic targeting handled at compilation time.

Current state

The current grammar version is v2.4 (the previous v2.3.3 is kept in the repo for reference). v2.4 added three backward-compatible extensions:

• REPLACES in the declaration block, for chaining specification versions
• an optional WITHIN deadline on EVENTUALLY(...) invariants, for bounded liveness properties
• a Progress<T> composite type, for expressing graduated status instead of just boolean done/not-done

The grammar is published under the Open Web Foundation Agreement 1.0 (OWFa 1.0). It's a work in progress — feedback on the primitive set, the ZK syntax, or prior art I should know about is welcome.

• Repo: https://github.com/triel-lang/grammar
• Site: https://triel.dev

Comments

[Dimitr Chis]

One thing I'm still not settled on: the grammar reserves 8 single-letter tokens (A, E, F, G, R, U, W, X) as LTL/CTL temporal operators, which means no bare single uppercase letter can be used as an identifier anywhere in a spec. It's noted as a deliberate tradeoff in the grammar comments, with the fully-spelled forms (ALWAYS/EVENTUALLY/NEXT) as the fallback if it proves too restrictive.

Curious if anyone here has hit this kind of collision in practice with other DSLs — is it worth the terseness, or does it just become a footgun once specs get bigger?