Strabo: Declarative Specification and Implementatio... | AI Research

Strabo is a research project that bridges the gap between formal academic methods for multiagent systems and practical industry standards for Agentic AI. The authors demonstrate how declarative interaction protocols—which define the rules of engagement between agents—can be used to model and implement real-world e-commerce interactions. By applying these methods to Google’s Universal Commerce Protocol (UCP), the researchers show that formal specifications can bring precision to industry standards without requiring a complete overhaul of existing systems.

Modeling Interactions with Langshaw

The core of the Strabo approach involves using Langshaw, a declarative language designed to specify how agents interact. Unlike traditional code, which often hides interaction rules deep within low-level logic, Langshaw provides a clear, formal blueprint of roles, actions, and dependencies. In this study, the authors modeled the checkout process of the Universal Commerce Protocol as a Langshaw protocol. This formal model clarifies ambiguous aspects of the industry standard, such as the specific order of operations and the data dependencies required to complete a transaction successfully.

Implementing Agents with Peach

To turn these protocols into working software, the authors use Peach, a programming model that simplifies agent development. Peach allows developers to focus on high-level domain decisions—such as what items to buy or how to handle payment—while an underlying "adapter" manages the technical requirements of the protocol. This adapter automatically tracks which actions are valid at any given moment, enforces rules, and ensures that agents remain compliant with the protocol. By separating protocol compliance from business logic, developers can build more robust agents that are easier to maintain and adapt to changing requirements.

Bridging to Industry Standards

A key contribution of Strabo is its ability to interoperate with existing industry agents. The researchers created a "proxy" layer that acts as a translator between the formal Langshaw protocol and the standard REST API calls used by Google’s UCP agents. When a Peach-based agent performs an action, the proxy intercepts it, translates it into the necessary HTTP requests, and handles the responses. This architecture allows new, formally verified agents to participate in existing e-commerce ecosystems, providing a practical pathway for organizations to adopt more rigorous, declarative protocols incrementally.

Insights from the Exercise

The process of modeling UCP in Langshaw revealed several implicit assumptions in the original industry protocol, such as the need for a strictly synchronous sequence of operations to prevent state conflicts. By formalizing these interactions, the authors were able to identify potential pitfalls that might otherwise remain hidden in informal documentation. This exercise demonstrates that formal, declarative specifications are not just academic exercises; they are practical tools that can improve the reliability and clarity of the complex, agent-driven systems currently being developed for industry use.