Can Proof Assistants Verify Multi-Agent Systems?

TL;DR

Can Proof Assistants Verify Multi-Agent Systems? presents Soda, a language that compiles to Scala for deployment and to Lean for formal verification, and demonstrates how MAS components can be executed and formally analyzed. Through a simple mediated marketplace protocol, the authors prove invariants such as length preservation under item updates, illustrating end-to-end executability and formal proofs within one framework. Experiments show the approach scales linearly with problem size, achieving around 4000 transactions per second, suggesting practical viability alongside rigorous verification. The work advocates for integrating proof assistants with mainstream software ecosystems to improve the reliability and safety of MAS, while outlining avenues for extending abstractions and evaluating real-world applicability.

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.

Figures (9)

• Figure 1: The function _tailrec_foldl is a tail-recursive auxiliary function of foldl, which is a left fold (foldl) function for parameterized types. length_fl, length_tr, and length_def syntactically different but semantically equivalent ways of defining the length of a list of an arbitrary type $A$ in Soda. The tail-recursive definitions (length_fl, length_tr) outperform the naive definition (length_def).
• Figure 2: This table shows the Soda definition of Nat, to be translated to Scala and to Lean.
• Figure 3: This table shows the definition of monus1, which for a positive number, it returns the previous number, and for other numbers, it returns 0.
• Figure 4: The function get retrieves an element safely, without throwing an exception if the index is out of range. This is necessary to ensure that the retrieved element is well defined.
• Figure 5: The function set_def is a tail recursive function that creates a new list with an element updated at a given index.