Agent communication

In this section, we review agent communication through the A2A protocol. We use Lean to model Agent Cards and task states and implement interface selection.

Our main references are the A2A specification and its protocol schema.

In A2A #

A2A defines communication between agents. Its a2a.proto at 12e9d2f defines the objects used for discovery and interaction:

• AgentCard describes the agent and lists supported interfaces and skills.
• AgentInterface gives an endpoint URL, protocol binding, and protocol version. The card orders interfaces by preference.
• AgentSkill describes an advertised capability, with an ID, name, description, and tags.
• TaskState distinguishes work in progress, interrupted work, and terminal outcomes. input-required and auth-required are interrupted states; completed, failed, canceled, and rejected are terminal.

The A2A specification also defines messages and task artifacts. An Agent Card describes how to interact with an agent; these discovery fields do not establish payment authorization.

For the economic model, shared quantities give types for a task's duration (Duration), energy use (Energy), and price (Amount asset). These belong to service accounting around a task; the card and task-state definitions below describe the interaction.

Cards and task states #

Our card projection keeps the fields needed for capability discovery:

structure AgentCard where
  name : String
  description : String
  version : String
  supportedInterfaces : List AgentInterface
  skills : List AgentSkill
  deriving DecidableEq, Repr

Each supported interface carries its protocol version. The agent's own version is a separate field; it is not the protocol version.

structure AgentInterface where
  url : String
  protocolBinding : String
  protocolVersion : String
  deriving DecidableEq, Repr

The selection function returns the first interface matching the client's binding and protocol version:

def selectInterface (card : AgentCard) (binding version : String) : Option AgentInterface :=
  card.supportedInterfaces.find? fun endpoint =>
    endpoint.protocolBinding == binding && endpoint.protocolVersion == version

The example Agent Card advertises JSON-RPC and HTTP+JSON endpoints. Selecting JSON-RPC 1.0 returns https://echo.example/a2a. gRPC 1.0 and JSON-RPC 0.3 return none. These are local card fixtures; no network request is sent.

The task states are represented by TaskState:

inductive TaskState where
  | unspecified | submitted | working | completed | failed | canceled
  | inputRequired | rejected | authRequired
  deriving DecidableEq, Repr

isTerminal classifies the four terminal states. This is a classification of states, not a task-transition implementation. The card projection omits security schemes, media modes, signatures, and other schema fields; it is not a complete Agent Card validator.