Docs · Running

Agent wallets

A wallet gives a Vertep identity verifiable credentials: it receives them, keeps them sealed, presents them only with consent, and issues and verifies them for other agents. Every exchange is a statechart run, every protocol and format is a plugin, and the exchange protocol is proven in Lean, with every plugin's runs checked against the proof.

Why a wallet is built from charts

Wallet protocols are where agents fail dangerously: an LLM agent discloses more than it should, a presentation is replayed to a second verifier, a credential is issued to a key nobody proved they hold. Vertep already handles protocols like these: it models them as statecharts, journals every step and proves its distributed protocols in Lean. The wallet uses the same machinery.

• Protocol-based. A wallet is the actor wallet/<DID>. Each exchange runs a role chart, issuer, holder or verifier, as a journaled agent actor, so it survives restarts, replays without its peers and is certified by vt certify like any chart.
• Pluggable. Protocols, formats, stores, consent policies and status resolvers are interfaces registered by IRI. Applications add their own or replace the built-ins.
• Verified. Every protocol reports its steps in one vocabulary. A Lean model of that vocabulary proves the safety properties, and a Lean checker judges what every plugin does under an adversarial network.

Plugins

let registry = WalletRegistry::with_builtins();
registry.register_format(Arc::new(MyFormat));                      // a new format under its own IRI
registry.register_store(vocab::STORE_SEALED, Arc::new(my_store));   // replace a built-in

Consent

Before any presentation the holder's chart reaches a vt:decide state. Its candidates are computed by the consent policy: the requested claims that the policy allows for this verifier and that a live credential holds. A rule decider, a person or an LLM picks one, or refuses. A choice outside the candidates fails the transition's guard and is never taken; the decision is journaled as out of bounds and nothing is presented. That is the decider-safety theorem of the agent model at work, and an LLM decider sees claim names, the verifier and the purpose, never claim values.

Protocols

The Vertep Credential Exchange carries offers, credential requests (with a possession proof over the issuer's nonce), credentials, presentation requests and presentations as TSP messages between DIDs: direct inside a TSP relationship, or routed through a mediator that only ever sees sealed bytes. OpenID4VCI issuers serve metadata, token, nonce and credential endpoints; holders redeem openid-credential-offer:// URIs, with transaction codes. OpenID4VP verifiers send DCQL queries in requests signed by their DID (decentralized_identifier:) or by value (redirect_uri:), and receive presentations by direct_post. The key manager signs with Ed25519, so OpenID4VC interoperates with wallets and verifiers that accept EdDSA.

The exchange model in Lean

VertepLean/Wallet.lean models issuers, holders and verifiers over a network the adversary controls: it sees every message, delivers any of them to anyone any number of times, drops and reorders them, and builds new messages from what it knows, but signs only with compromised keys. These theorems hold in every reachable state:

A second model drops the verifier's audience check, and Lean exhibits a run in which a presentation made for one verifier is accepted by another: the check is necessary, not decoration.

Conformance

The conformance kit owns the network between the parties. A seeded scheduler duplicates, reorders, drops, replays messages to other parties and injects garbage; every step lands in an exchange history, and the Lean checker vertep-wallet replays it against the model. A protocol plugin is conformant when the checker accepts every history, so third-party plugins inherit the theorems for the runs tested without writing any Lean. The kit catches a deliberately faulty plugin whose verifier accepts a duplicate presentation.

$ vt wallet conformance --seeds 4
vce: 9 histories, 6 presentations accepted, 9 of 9 accepted by the Lean checker
oid4vc: 9 histories, 6 presentations accepted, 9 of 9 accepted by the Lean checker

vt wallet

A wallet on disk is a directory with a file key manager, the sealed records and wallet.json (DID, trusted issuers, consent policy). A recorded session: the verifier asks for nationality and name, and the holder's policy lets it have nationality only.

$ vt wallet create --dir holder
did: did:key:z6MkhQ4mKxGrrKcdCbtUpRT6CLHyvYYfXsgjjqu3866g7kMB
$ vt wallet issue --dir issuer --to <holder> --type https://example.org/IdentityCredential \
    --claims '{"name":"Olena","nationality":"UA"}' --out cred.json
issued: sha256:aff2cad12de34d2d208307ee1a39d3888ef34ac7d1851b4215f3b3c830d6436d
$ vt wallet accept --dir holder cred.json
stored: sha256:aff2cad12de34d2d208307ee1a39d3888ef34ac7d1851b4215f3b3c830d6436d
issuer: did:key:z6MktPXykAZNrjumiFLcDuJXd759osRJ6oUXE7ZJQ3DESwLS
$ vt wallet request --dir verifier --claims nationality,name --out req.json
$ vt wallet present --dir holder req.json --out pres.json
presented: sha256:aff2cad12de34d2d208307ee1a39d3888ef34ac7d1851b4215f3b3c830d6436d
disclosed: nationality
$ vt wallet verify --dir verifier req.json pres.json
valid
issuer: did:key:z6MktPXykAZNrjumiFLcDuJXd759osRJ6oUXE7ZJQ3DESwLS
disclosed: {"nationality":"UA"}

vt wallet offer serves an OpenID4VCI issuer and prints the offer URI; accept and present also take openid-credential-offer:// and openid4vp:// URIs; revoke sets a status entry and republishes the list under public/. Grant credentials are ordinary wallet credentials: presented over any protocol, they become grants the federation enforces before the journal.

The design notes are in tg.md/views/wallet.md; the requirements in openspec/changes/m9-agent-wallet (capabilities agent-wallet, credential-exchange and oid4vc); the history format in crates/vertep-wallet/docs/exchange-history.md.