RebecAI is a project focused on integrating AI and LLM techniques with formal verification methods, particularly within the Rebeca modeling framework. The main goal is to explore how AI,especially large language models, can assist in generating, transforming, or analyzing correctness properties used in formal verification. By combining automated reasoning with actor-based modeling, the project aims to simplify and accelerate the verification process for complex systems. The work demonstrates how intelligent tools can support developers in bridging the gap between high-level specifications and formal models. It highlights both the potential and limitations of AI-assisted verification, showing that while automation can reduce manual effort, careful validation is still required to ensure correctness and reliability. Overall, the project contributes to advancing the usability of formal methods in practical software and system development. In practice, the system takes structured inputs or specifications and leverages AI models to generate corresponding formal properties that can be used within Rebeca for model checking. It helps automate parts of the transformation process, supports experimentation with different prompting strategies, and enables users to evaluate and refine the generated outputs for correctness and completeness.
The implementation and source code related to this project are available at the link provided below, where all relevant materials, models, and transformation scripts can be accessed for further exploration and replication of the results.
LINK
Note that this is a fork of Repo, available at LINK, under the MIT License.
Relevant paper can be found here LINK.