Can Proof Assistants Verify Multi-Agent Systems?

Julian Alfredo Mendez, Timotheus Kampik
3/10/2025
cs.PLcs.AIcs.LO

No official code found. Best implementation: julianmendez/soda (6 stars, last commit 2026-04-22).

Abstract

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.

View on arXivView PDF

Code Implementations(1)

julianmendez/sodaCommunity100%

Object-oriented functional language to describe, analyze, and model human-centered problems

61Lean, ScalaAug 2, 20226 months ago
functional-languagehuman-centeredobject-orientedsoda-languagetransparent

Similar Papers

Toolsuite for Implementing Multiagent Systems Based on Communication Protocols

86% match2025

StackPilot: Autonomous Function Agents for Scalable and Environment-Free Code Execution

85% match2025

Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

83% match2026

TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

82% match2026

Collaboration Dynamics and Reliability Challenges of Multi-Agent LLM Systems in Finite Element Analysis

82% match2024

The Impact of Strategies and Information in Model Checking for Multi-Agent Systems

82% match2023

Cite this paper

@article{mendez2025proof,
  title  = {Can Proof Assistants Verify Multi-Agent Systems?},
  author = {Julian Alfredo Mendez and Timotheus Kampik},
  year   = {2025},
  eprint = {2503.06812},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2503.06812v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2503.06812.svg)](https://codeofpaper.com/paper/2503.06812)

Discussion