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 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 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 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