Can Proof Assistants Verify Multi-Agent Systems?
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929751071916032 |
|---|---|
| author | Mendez, Julian Alfredo Kampik, Timotheus |
| author_facet | Mendez, Julian Alfredo Kampik, Timotheus |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_06812 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Can Proof Assistants Verify Multi-Agent Systems? Mendez, Julian Alfredo Kampik, Timotheus Programming Languages Artificial Intelligence Logic in Computer Science Multiagent Systems 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. |
| title | Can Proof Assistants Verify Multi-Agent Systems? |
| topic | Programming Languages Artificial Intelligence Logic in Computer Science Multiagent Systems |
| url | https://arxiv.org/abs/2503.06812 |