Soda

@misc{Mendez-Kampik-2025-SodaMas,
      title = { {Can Proof Assistants Verify Multi-Agent Systems?} },
      author = {Mendez, Julian Alfredo and Kampik, Timotheus},
      year = {2025},
      month = {March},
      eprint = {2503.06812},
      archivePrefix = {arXiv},
      doi = {10.48550/arXiv:2503.06812},
      url = {https://doi.org/10.48550/arXiv.2503.06812},
      note = { \url{https://doi.org/10.48550/arXiv.2503.06812} },
      primaryClass = {cs.PL},
      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.
      },
      keywords = {Engineering Multi-Agent Systems, Formal Verification, Proof Automation}
}