TRIEL

An open specification language for deterministic, verifiable compilation.

The problem

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

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

Example

EUDI Wallet driving license — issuance and presentation policy.

eudi_driving_license.tri

1-- TRIEL example: EUDI Wallet driving license — issuance and presentation policy
2
3-- Demonstrates: conditional obligations, ZK age predicate, prohibition on stale credentials
4
5SPECIFICATION eudi_driving_license VERSION 1.0.0
6
7    STANDARD "ISO-18013-5", "eIDAS-2.0"
8
9    JURISDICTION "EU"
10
11SUBJECTS {
12
13  applicant : PARTY,
14
15  issuer    : REGULATOR,
16
17  verifier  : PARTY
18
19}
20
21FACTORS {
22
23  age                       : ZK<Integer> PROVES(self >= 18) WITHOUT REVEALING self
24
25                              METADATA SOURCE applicant,
26
27  vision_correction_needed  : Boolean METADATA SOURCE issuer,
28
29  license_category          : String  METADATA SOURCE issuer,
30
31  license_valid             : Boolean METADATA SOURCE issuer MAX_AGE 24 HOURS
32
33}
34
35TERMS {
36
37  applicant MUST submit_proof(age) BY DATETIME("2026-09-01T00:00:00Z");
38
39  IF vision_correction_needed THEN
40
41    issuer MUST attach_restriction("corrective_lenses")
42
43  ELSE
44
45    issuer MAY issue_unrestricted_category;
46
47  verifier MUST_NOT accept_presentation WHEN license_valid == false
48
49}
50
51INVARIANTS {
52
53  license_requires_adult_holder       : SAFETY : ALWAYS(age >= 18);
54
55  presentation_requires_valid_license : SAFETY : ALWAYS(license_valid == true)
56
57}

Where it fits

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.

Why this matters now

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.

Contact

Questions or feedback? Open an issue on GitHub →Or email: dchis@triel.dev