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.

翻译：本文提出用于验证多智能体系统的Soda语言。Soda是一种高级函数式与面向对象语言，其代码不仅可编译为强静态类型的高级编程语言Scala，还可编译为证明助手兼编程语言Lean。基于这些能力，Soda既能实现可集成至主流软件生态的多智能体系统（或其组成部分），又能借助前沿工具进行形式化验证。本文简要非正式地介绍了Soda及其互操作性能力，并通过简单案例演示如何用Soda设计与验证交互协议。演示过程中，我们重点探讨了实际应用场景中面临的挑战。