Market

@inproceedings{Mendez.Kampik-2025-EUMAS,
    author = {Mendez, Julian Alfredo and Kampik, Timotheus},
    title = { {Can Proof Assistants Verify Multi-agent Systems?} },
    booktitle = {Multi-Agent Systems},
    year = {2025},
    month = {June},
    pages = {323--339},
    editor = {Collier, Rem and Ricci, Alessandro and Nallur, Vivek and Burattini, Samuele and Omicini, Andrea},
    publisher = {Springer Nature Switzerland},
    address = {Cham},
    doi = {10.1007/978-3-031-93930-3_19},
    url = {https://doi.org/10.1007/978-3-031-93930-3_19},
    note = { \url{https://doi.org/10.1007/978-3-031-93930-3_19} },
    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}
}