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
11    PROOF_SYSTEM: GROTH16
12
13    CURVE: "BN254"
14
15SUBJECTS {
16
17  applicant : PARTY DID "did:web:eudi-wallet.example.eu:applicant",
18
19  issuer    : REGULATOR,
20
21  verifier  : PARTY
22
23}
24
25TERMS {
26
27  applicant MUST submit_proof(age) BY DATETIME("2026-09-01T00:00:00Z");
28
29  IF vision_correction_needed THEN
30
31    issuer MUST attach_restriction("corrective_lenses")
32
33  ELSE
34
35    issuer MAY issue_unrestricted_category;
36
37  verifier MUST_NOT accept_presentation WHEN license_valid == false
38
39}
40
41FACTORS {
42
43  age                       : ZK<Integer> PROVES(self >= 18) WITHOUT REVEALING self
44
45                              BOUND_TO(applicant, presentation_nonce)
46
47                              METADATA SOURCE applicant,
48
49  age_proof_valid           : Boolean METADATA SOURCE applicant,
50
51  presentation_nonce        : Hash    METADATA SOURCE verifier,
52
53  vision_correction_needed  : Boolean METADATA SOURCE issuer,
54
55  license_category          : String  METADATA SOURCE issuer,
56
57  license_valid             : Boolean METADATA SOURCE issuer MAX_AGE 24 HOURS
58
59}
60
61INVARIANTS {
62
63  license_requires_adult_holder       : SAFETY : ALWAYS(age_proof_valid == true);
64
65  presentation_requires_valid_license : SAFETY : ALWAYS(license_valid == true)
66
67}

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