Arbiter

Inspiration

Multi-agent AI systems fail in ways single-agent systems don't: two agents grab the same task, a handoff acknowledgment never arrives, one agent silently duplicates work another already finished. These are coordination bugs, and they hide across whatever transport each agent happens to use — gRPC, a queue, a shared blackboard, a webhook, or stdout. A verifier that only watches one transport is blind to the rest. We wanted to build a seatbelt for multi-agent systems, grounded in real distributed-systems theory instead of hand-written if/else checks.

What it does

ARBITER watches agent coordination events across multiple simulated transports and stamps each one with a Hybrid Logical Clock timestamp, so events from agents that share no clock can still be causally ordered. It specifies the coordination protocol as an explicit state machine with safety and liveness properties. It structurally prevents hard-invariant violations — like two agents executing the same task — using fencing tokens, so a stale agent's write is rejected outright, not just logged. It detects soft-invariant anomalies, like duplicated work nobody thought to spec, by building a dependency graph over claim/read/write operations and searching for cycles — the same technique databases use to catch transactional isolation bugs. And the moment a violation is confirmed, it revokes the offending agent's capability token, gating its next real-world tool call without needing to interrupt an LLM mid-generation.

How we built it

• Causal capture: a Hybrid Logical Clock (physical + logical counter) stamps every event on ingestion into an in-memory event bus, fed by four toy agents running as asyncio tasks across simulated gRPC, queue, blackboard, webhook, and stdout transports.
• Hard prevention: a LeaseManager issues strictly increasing fencing tokens per resource; a ProtectedResource rejects any write carrying a token lower than the highest one it's already accepted.
• Spec layer: a small state-machine engine, inspired by Microsoft's P/Coyote lineage, loads a protocol spec as data (not code) and tracks Idle → Claimed → InProgress → AwaitingAck → Acked/Escalated transitions per resource.
• Soft detection: a dependency-graph builder records WW/WR/RW edges — following Adya's Direct Serialization Graph formalism, the same approach Kyle Kingsbury's Elle checker uses for Jepsen — and a cycle detector flags any history no valid ordering could explain.
• Circuit breaker: a capability-token store revokes an agent's token the instant either detection path confirms a violation; a tool-call boundary checks every action against it.
• Dashboard: a FastAPI + WebSocket service streams the live event feed, per-resource state, the dependency graph (rendered with D3), and violations to a browser dashboard in real time.

Challenges we ran into

Designing an event schema flexible enough to support both the state-machine spec and the dependency-graph builder was trickier than it looked — we had to be deliberate about which fields were structural (kind, transport, resource_id) versus which were carried in payload, so the two detection layers could consume the same event stream without stepping on each other. Keeping the fencing-lease and timeout logic deterministic (event-count based rather than wall-clock) took care, since a demo can't afford real-timing flakiness in front of judges. And scoping the predicate-detection language down to conjunctive and stable predicates — rather than trying to support arbitrary boolean expressions, which is NP-complete to detect in general — meant resisting the urge to over-engineer the spec DSL.

Accomplishments that we're proud of

We implemented four separate, real pieces of distributed-systems literature — Hybrid Logical Clocks, fencing tokens, P/Coyote-style runtime verification, and Elle-style cycle detection — as working, tested code in a single weekend, and wired them into one coherent pipeline instead of four disconnected demos. The three-act scenario genuinely demonstrates all of it end to end: a clean run, a structurally rejected stale write, and a write-skew anomaly caught by cycle detection that no explicit spec ever named.

What we learned

That the hardest part of building a verifier isn't the algorithms — HLCs, fencing tokens, and cycle detection are all well-understood, citable techniques — it's the event schema and interface boundaries that let independently-designed components (a state machine, a dependency graph, a lease service) all agree on what an "event" means without becoming tightly coupled to each other.

What's next for Arbiter

Swapping the simulated transport adapters for real capture — eBPF-based tracing in the style of Cilium Tetragon or Pixie — would make ARBITER agent-code-agnostic instead of requiring instrumentation calls. We'd also want to implement Garg & Mittal's predicate-slicing decomposition for real, so most pairwise checks run at the edge between two agents instead of all funneling through one central verifier, and back the lease service with a real distributed coordination service (Raft/etcd) instead of a single in-process manager.

Built With

• asyncio
• d3.js
• fastapi
• networkx
• pydantic
• python
• websockets