# Can Proof Assistants Verify Multi-Agent Systems?

arXiv: https://arxiv.org/abs/2503.06812 · HTML: https://mlsanity.com/paper/2503.06812/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 23 references that are in the map.
- First posted on arXiv 10 Mar 2025.

## Builds on (most cited first, 1 of 1)

- [Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems](https://mlsanity.com/paper/2310.01961/) (2023)

## Built on by (most cited first, 3 of 3)

- [From Glue-Code to Protocols: A Critical Analysis of A2A and MCP Integration for Scalable Agent Systems](https://mlsanity.com/paper/2505.03864/) (2025)
- [Composable Verification Pipelines for Multi-Agent Systems](https://mlsanity.com/paper/2607.16266/) (2026)
- [The AR Fairness Metamodel: A Structured Framework for Fairness Measures](https://mlsanity.com/paper/2609.19234/) (2026)

## Abstract (arXiv)

This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level programming language, but also to Lean, a proof assistant and programming language. Given these capabilities, Soda can implement multi-agent systems, or parts thereof, that can then be integrated into a mainstream software ecosystem on the one hand and formally verified with state-of-the-art tools on the other hand. We provide a brief and informal introduction to Soda and the aforementioned interoperability capabilities, as well as a simple demonstration of how interaction protocols can be designed and verified with Soda. In the course of the demonstration, we highlight challenges with respect to real-world applicability.