TRIEL — An open specification language
TRIEL<br>An open specification language for deterministic, verifiable compilation.<br>View on GitHubRead the grammar
The problem<br>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 common source of costly failures, compliance issues, and audit findings.
The approach<br>TRIEL treats specification-to-implementation translation as the point where correctness evidence should be generated — not recovered afterward through separate testing or review.
Example<br>EUDI Wallet driving license — issuance and presentation policy.
eudi_driving_license.tri<br>1-- TRIEL example: EUDI Wallet driving license — issuance and presentation policy<br>3-- Demonstrates: conditional obligations, ZK age predicate, prohibition on stale credentials<br>5SPECIFICATION eudi_driving_license VERSION 1.0.0<br>7 STANDARD "ISO-18013-5", "eIDAS-2.0"<br>9 JURISDICTION "EU"<br>10<br>11SUBJECTS {<br>12<br>13 applicant : PARTY,<br>14<br>15 issuer : REGULATOR,<br>16<br>17 verifier : PARTY<br>18<br>19}<br>20<br>21FACTORS {<br>22<br>23 age : ZKInteger> PROVES(self >= 18) WITHOUT REVEALING self<br>24<br>25 METADATA SOURCE applicant,<br>26<br>27 vision_correction_needed : Boolean METADATA SOURCE issuer,<br>28<br>29 license_category : String METADATA SOURCE issuer,<br>30<br>31 license_valid : Boolean METADATA SOURCE issuer MAX_AGE 24 HOURS<br>32<br>33}<br>34<br>35TERMS {<br>36<br>37 applicant MUST submit_proof(age) BY DATETIME("2026-09-01T00:00:00Z");<br>38<br>39 IF vision_correction_needed THEN<br>40<br>41 issuer MUST attach_restriction("corrective_lenses")<br>42<br>43 ELSE<br>44<br>45 issuer MAY issue_unrestricted_category;<br>46<br>47 verifier MUST_NOT accept_presentation WHEN license_valid == false<br>48<br>49}<br>50<br>51INVARIANTS {<br>52<br>53 license_requires_adult_holder : SAFETY : ALWAYS(age >= 18);<br>54<br>55 presentation_requires_valid_license : SAFETY : ALWAYS(license_valid == true)<br>56<br>57}
Where it fits<br>vs. OPA/Rego<br>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*<br>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.
Why this matters now<br>Digital identity, verifiable credentials, and privacy-preserving proofs are moving from research into regulation. A readable, compilable spec language lets compliance and engineering share one artifact.
Edit with