How a jurisdiction-neutral identity runtime hosts EUDI and other national identity schemes without collapsing their trust or legal semantics.
Architecture
Separation of concerns is a security control.
The wallet is a sans-IO Rust behaviour core driven by thin native shells. Responsibility boundaries — not frameworks — are the design: protocol logic cannot touch the network, the shell cannot make trust decisions, and keys cannot leave secure hardware. Assessed against the pinned EUDI specification register: ARF v2.9.0 · PID Rulebook v1.7 · FCAF v0.0.7 (snapshot 2026-07-17) — never an unversioned "latest ARF".
Sans-IO protocol core
The core is a pure state machine: events in, effects out. No network, clock, radio, or disk access exists inside protocol logic — the shell executes effects and feeds results back.
Why it matters Protocol decisions are deterministic and testable without mocking the world; the same core binary logic runs under tests, fuzzing, oracle replay, and on device.
Deterministic, exhaustively-matched state machines
Each protocol (presentation, issuance, proximity, payment, QES, transfer) is an explicit state machine with exhaustive matches; every guard maps 1:1 to a named abort reason.
Why it matters Same state + same event ⇒ same effects. This is what makes the Lean models faithful and the oracle-replay conformance suites meaningful.
All cryptography goes through the crypto-traits interface; the production backend is aws-lc-rs. Protocol crates cannot reach a crypto library directly.
Why it matters Cryptographic agility: the backend can be swapped or FIPS-pinned without touching protocol logic; the allow-list of algorithms is auditable in one place.
crates/crypto-traits/ · crates/crypto-backend/
Device keys never cross the FFI
Signing is an effect carrying bytes-to-sign and a key reference. The Secure Enclave (non-exportable, biometric-gated) fulfils it on device.
Why it matters A compromised UI process cannot exfiltrate key material it never holds.
The core renders fully-resolved screens (exact claims, amount, payee, document) and records a committing consent hash in the tamper-evident audit log.
Why it matters What the user approved is cryptographically bound to what is signed — the basis of the dynamic-linking and WYSIWYS proofs.
crates/presenter/ · crates/txnlog/
Trust decisions are core decisions
RP registration and issuer trust are decided in-core by X.509 path validation against operator-signed trusted lists; status lists gate presentation fail-closed. The shell only fetches bytes.
Why it matters A buggy or malicious shell cannot inject 'trusted: true'.
crates/trust/ · crates/x509/ · crates/status/
Memory-safe by construction
All 21 workspace crates are #![forbid(unsafe_code)]; the pinned toolchain is Rust 1.97.1.
Why it matters Entire vulnerability classes (spatial/temporal memory errors) are excluded at compile time in wallet code.
crates/*/src/lib.rs · rust-toolchain.toml
iOS and Android, one core
Android is a supported platform alongside iOS: both shells use the same Rust core, with Swift/UniFFI on iOS and Kotlin/Android bindings around the platform-specific shell. The reference shell-io crate drives the identical core over real sockets.
Why it matters Protocol behaviour is reviewed and verified once, while Android and iOS keep keys, storage, and effect execution in thin, auditable native layers. Android-specific formal modelling and exhaustive Kotlin conformance are still required for first-class parity.
Select any component (click or keyboard) to open its evidence panel — responsibilities, trust assumptions, threats, proofs, tests, and source path. Static SVG artifacts: ecosystem-context.svg · wallet-components.svg