The KeY project provides a Deductive Java Program Verifier. This verifier is an interactive theorem prover designed for the verification of Java programs. You can find more information on KeY on our website and in the documentation.
The current version is 2.12.2, licensed under GPL v2.
Pinned LoadingKeY Theorem Prover for Deductive Java Verification
Documentation for the KeY Theorem Prover
A curated list of tools and tutorials for the KeY Theorem Prover
A template for larger verification projects with KeY
Python 1
Example project for program verification on the KeY platform
Example to use the KeY Theorem Prover for Symbolic Execution
Java
KeY Theorem Prover for Deductive Java Verification
KeYProject/key’s past year of commit activityDocumentation for the KeY Theorem Prover
KeYProject/key-docs’s past year of commit activity TeX 2 6 7 2 Updated Aug 12, 2025Github Action for setting up some SMT solvers
KeYProject/setup-smt’s past year of commit activity TypeScript 0 MIT 0 0 0 Updated Aug 2, 2025A curated list of tools and tutorials for the KeY Theorem Prover
KeYProject/awesome-key’s past year of commit activity 3 1 2 0 Updated Jul 2, 2024Loading…
You can’t perform that action at this time.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4