A paid task

In this section, we develop an executable model of a paid agent task in Lean. We specify wallet authorization and settlement conditions, then compose payment and task execution into a state transition system.

The model combines the components introduced in Modules and interactions. It uses native ETH accounting and models only the transfer value; gas fees and network execution are omitted. It is a local composition model, not an x402 EVM payment implementation.

Bind payment to a task #

Agent A asks Agent B to echo hello for 0.003 ETH. A starts with 0.01 ETH and B with 0.002 ETH. A's wallet permits this amount and recipient. After the modeled transfer, A has 0.007 ETH, B has 0.005 ETH, and B returns hello.

The requested service and input belong to the task. Payment terms bind the whole request to an asset, amount, payer, recipient, and deadline:

structure PaymentTerms where
  task : TaskRequest
  payer : AccountId
  payee : AccountId
  asset : AssetId
  amount : Amount asset
  expiresAt : Nat
  deriving DecidableEq, Repr

The accounts use eip155:1, and Ethereum.ether identifies native ETH. Ethereum.milliEther 3 supplies the payment amount in wei. The account addresses are local fixtures; this example sends no transaction.

CanAuthorize applies the wallet policy and requires the authenticated actor to be the task's caller. authorize records approval without changing balances or producing a cryptographic signature.

Transfer, then complete #

The ledger records balances and used (payer, nonce) pairs. Settlement requires enough funds, a fresh authorization, matching task and provider details, and now < expiresAt. Time and nonces are local model values, not Ethereum transaction fields.

def CanSettle (wallet : Wallet) (provider : Agent) (task : Task)
    (ledger : Ledger) (authorization : Authorization) (now : Nat) : Prop :=
  CanAuthorize wallet authorization.actor authorization.terms ∧
  MatchesTask provider task authorization.terms ∧
  task.phase = .requested ∧
  now < authorization.terms.expiresAt ∧
  (authorization.terms.payer, authorization.nonce) ∉ ledger.spent ∧
  authorization.terms.amount.units ≤
    ledger.balances authorization.terms.payer authorization.terms.asset

An accepted settlement debits A, credits B, consumes the authorization, and marks the task paid in one model transition. Other accounts and assets retain their balances. The provider then returns the requested input.

def demo : Option Report := do
  let (ledger, paidTask) ← paid
  if paidTask.request.service ≠ "echo" then none else do
    let finished ← complete provider.id paidTask paidTask.request.input
    pure ⟨ledger.balances buyerAccount ether,
      ledger.balances providerAccount ether,
      ledger.balances otherAccount otherAsset, finished.phase⟩

The local phases requested, paid, and completed describe this example's ordering. They are separate from A2A's task states. Recording a result also does not establish the quality of an arbitrary service; the echo example computes its result directly from the input.

Connect the modules #

Config pairs A's wallet with B and the echo service. The service takes a name and an input, returning some result on success or none on failure.

structure Config where
  wallet : Wallet
  provider : Agent
  service : String → String → Option String

State records the task, balances, and any pending payment approval. It starts with the requested task, the initial balances, and no approval.

structure State where
  task : Task
  ledger : Ledger
  approval : Option Authorization := none

The example runs three actions: A authorizes the payment, the ledger settles it, and B executes the task.

inductive Action where
  | authorize (actor : AgentId) (terms : PaymentTerms) (nonce : Nat)
  | settle (now : Nat)
  | execute (actor : AgentId)
  deriving Repr

step applies one action to the current state. Authorization stores the approval. Settlement transfers the funds, marks the task paid, and clears the approval. Execution calls the service and records its result. A rejected action returns none.

def step (config : Config) (state : State) : Action → Option State
  | .authorize actor terms nonce => do
    if state.approval.isSome ∨ state.task.phase ≠ .requested then none else do
      if ¬ MatchesTask config.provider state.task terms then none else do
        let approval ← PaidTask.authorize config.wallet actor terms nonce
        pure { state with approval := some approval }
  | .settle now => do
    let approval ← state.approval
    let (ledger, task) ← PaidTask.settle config.wallet config.provider
      state.task state.ledger approval now
    pure { task, ledger, approval := none }
  | .execute actor => do
    if actor ≠ config.provider.id ∨ state.task.phase ≠ .paid then none else do
      let result ← config.service state.task.request.service state.task.request.input
      let task ← PaidTask.complete actor state.task result
      pure { state with task }

Run #

lake build
lake exe demo

The system trace records one execution of this example. The table displays ETH; lake exe demo prints the same balances as integers in wei.

The final balances are 7,000,000,000,000,000 wei for A and 5,000,000,000,000,000 wei for B. The result is completed "hello". A separate test-network balance of 7 base units is unchanged.

The build checks rejection of excessive spending, wrong actors, recipients or networks, expired authorizations, insufficient funds, changed tasks, replayed payments, and execution before payment.

Payment and service success are separate: if the service fails after settlement, the preceding paid state still represents the completed transfer. trace returning none reports a rejected sequence; it does not reverse earlier state transitions.

One paid call studies reservation and refund in a separate accounting model.