JVerify is a program verifier for Java. It lets you specify the intended behavior of Java code using contracts written in regular Java, and proves (or disproves) that the implementation matches.
JVerify is built on top of Strata, a platform for program verification.
JVerify is not yet ready for production use. Java language support, user experience, and reliability are all early. You can still experiment with it today to get a feel for what it can do. See the user guide for a current list of supported features.
See the user guide for installation instructions and a first-verification walkthrough.
Contributions are welcome. See CONTRIBUTING.md.
See CONTRIBUTING for more information.
This project is licensed under the Apache-2.0 License.