TRIEL
TRIEL is an open language for norms: obligations, permissions and prohibitions with deadlines, breaches and invariants. The core of the language is formalised in Isabelle/HOL, and its proofs are machine-checked.
Current version: TRIEL 2.5.1, released in October 2026. The grammar is frozen. Version 2.5.1 corrects errors in the semantics of 2.5; the grammar does not change.
The problem
A specification and the software that implements it often stop matching over time. The specification is written once, while the software is built, maintained and changed separately, and the two slowly diverge. This gap often causes costly failures, compliance problems and audit findings.
The approach
TRIEL gives each rule one precise meaning. The core of the language is formalised in Isabelle/HOL. A program called the evaluator is exported from these Isabelle theories. It takes a specification and a recorded sequence of events and computes a verdict for each rule. This works for the part of the language that the formal core covers.
Example
Example: the rules for issuing and presenting a driving license in the EU Digital Identity Wallet (EUDI Wallet). The formal core accepts this file.
1-- TRIEL example: EUDI Wallet driving license — issuance and presentation policy2-- Demonstrates: conditional obligations, ZK age predicate, prohibition on stale credentials34SPECIFICATION eudi_driving_license VERSION 1.0.05 STANDARD "ISO-18013-5", "eIDAS-2.0"6 JURISDICTION "EU"7 PROOF_SYSTEM: GROTH168 CURVE: "BN254"910SUBJECTS {11 applicant : PARTY DID "did:web:eudi-wallet.example.eu:applicant",12 issuer : REGULATOR,13 verifier : PARTY14}1516TERMS {17 applicant MUST submit_proof(age) BY DATETIME("2026-09-01T00:00:00Z");1819 IF vision_correction_needed THEN20 issuer MUST attach_restriction("corrective_lenses")21 ELSE22 issuer MAY issue_unrestricted_category;2324 verifier MUST_NOT accept_presentation25 WHEN NOT PRESENT(license_valid) OR license_valid == false26}2728FACTORS {29 age : ZK<Integer> PROVES(self >= 18) WITHOUT REVEALING self30 BOUND_TO(applicant, presentation_nonce)31 METADATA SOURCE applicant,32 age_proof_valid : Boolean METADATA SOURCE verifier,33 presentation_accepted : Boolean METADATA SOURCE verifier,34 presentation_nonce : Hash METADATA SOURCE verifier,35 vision_correction_needed : Boolean METADATA SOURCE issuer,36 license_category : String METADATA SOURCE issuer,37 license_valid : Boolean METADATA SOURCE issuer MAX_AGE 24 HOURS ON_STALE BLOCK38}3940INVARIANTS {41 license_requires_adult_holder : SAFETY :42 ALWAYS(presentation_accepted IMPLIES age_proof_valid == true);43 presentation_requires_valid_license : SAFETY :44 ALWAYS(presentation_accepted IMPLIES (PRESENT(license_valid) AND license_valid == true))45}Where it fits
Compared with OPA/Rego
Rego checks requests at the entry point of a system, for example in admission control and API gateways. It checks a single request against a snapshot of data, not a sequence of events over time. TRIEL checks sequences of events over time and can set constraints on individual data fields, including fields that are only proved and never revealed.
Compared with Wysteria and Wys*
Wysteria and Wys* are rigorous languages for secure multiparty computation. They are built for cryptographers who already understand type theory and how a program is split between its participants. TRIEL is written for people who are not cryptographers: compliance officers and analysts state what must hold. A zero-knowledge field states what a proof must show. An external proof system creates and checks the proof, and the rules use only the result of that check.
Why this matters now
Digital identity, verifiable credentials and privacy-preserving proofs are moving from research into law and regulation. A readable specification language that is designed to be checked lets compliance teams and engineers work from one shared document.