Issue trusted credentials.Prove every decision.
A from-scratch German PID and attestation issuer with a small Rust decision kernel, machine-checked safety invariants, and wallet-ready SD-JWT VC and mdoc issuance.
Live issuer
Choose a credential
Each QR code is generated by the running issuer as a short-lived OpenID4VCI credential offer. Nothing below is a static demo token.
Machine-checked assurance
The signing gate is the proof boundary
The pure Rust authorization kernel mirrors the Lean transition model. Network adapters may prepare a request; only the kernel can authorize a signing command.
Checked with the repository-pinned Lean toolchain. Proofs cover the model and its explicit assumptions—not arbitrary adapter code.
Protocol security
Tamarin verifies matching authorization, matching evidence, and credential-ID injectivity.
Executable checks
Seven default and two explicit Keychain integration tests pass; clippy is clean at -D warnings.
Non-exportable signing
Distinct P-256 keys are used through Security.framework; raw private keys do not enter the process.
Traceable scope
Normative rules, semantic proofs, protocol analysis, and implementation checks stay distinct.
German EUDI profile
Conformance is an evidence chain
Implemented behavior targets the European Architecture and Reference Framework and German issuer roles. External certification remains a separate legal and assessment milestone.
Implemented now
- OpenID4VCI issuer + authorization metadata
- PAR, PKCE S256, DPoP and proof JWT
- SD-JWT VC selective disclosure
- ISO mdoc MSO + COSE Sign1
Verified evidence
- Lean signing-gate invariants
- Tamarin issuance properties
- Closed credential profile allow-list
- Replay and one-shot nonce defenses
Certification gates
- Official conformance test suites
- German authority and CAB assessment
- Production trust lists and certificates
- HSM/qualified signing deployment
Accurate status: this is a formally analysed, conformance-targeted development issuer. It is not yet a certified German PID Provider, Attestation Provider, or QEAA Provider, and local Keychain certificates are not production trust anchors.
Inspect the live protocol surface