We can finally, officially announce the open-source release of AProVE! Github: aprove-open-source. Over the years, AProVE has evolved into one of the leading tools for automated reasoning about termination and complexity of programs and rewrite systems. By making the project openly available, we hope to make formal verification research more accessible, encourage community contributions, and enable easier experimentation for external researchers.
Designed for Accessibility and Reproducibility
One of the main goals of this release was to significantly improve the usability of AProVE. The repository wiki provides comprehensive documentation to help users understand AProVE’s core architecture and workflows. To simplify testing and benchmarking, we also provide an official Docker container that enables users to run AProVE in a fully reproducible environment without complicated setup steps. An up-to-date image will soon be available on Docker Hub, and we plan to cover its full capabilities in a future blog post. For now, the Docker image can already be found in the GitHub repository, and the wiki includes detailed instructions on how to use it, see here.
New Capability: Confluence Proofs
Beyond the open-source release itself, the newest release introduces a new verification capability: AProVE can now automatically analyze Confluence.
Confluence is a fundamental property in rewriting systems and formal verification. Informally, it guarantees that different evaluations eventually lead to the same result. Tools for analyzing confluence automatically compete in the annual confluence competition, where AProVE participated last year for the first time.
Looking Ahead
The open-source release is only the beginning. We have many exciting ideas planned for the year 2026, including:
- Graphical visualization of the strategies used within AProVE for easier development
- Performance optimizations for all verification goals
- Expanded educational material and tutorials for new users
- Further improvements to automated confluence analysis
- Integration of techniques for analysing reachability in (probabilistic) term rewriting
- Integration of new termination techniques for (probabilistic) term rewriting
We are looking forward to collaboration and seeing how researchers and developers build upon AProVE in the future.
Explore the Project
Visit the official project page to learn more about AProVE, its features, and upcoming updates: aprove-open-source
— The AProVE Team