Skip to content

KeY Project

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.3, licensed under GPL v2.

Pinned Loading

  1. key key Public

    KeY Theorem Prover for Deductive Java Verification

    Java 88 46

  2. key-docs key-docs Public

    Documentation for the KeY Theorem Prover

    TeX 4 6

  3. awesome-key awesome-key Public

    A curated list of tools and tutorials for the KeY Theorem Prover

    3 1

  4. verification-project-template verification-project-template Public template

    A template for larger verification projects with KeY

    Python 1

  5. key-java-example key-java-example Public template

    Example project for program verification on the KeY platform

    Java 1 1

  6. symbex-java-example symbex-java-example Public template

    Example to use the KeY Theorem Prover for Symbolic Execution

    Java

Repositories

Showing 10 of 26 repositories
  • key-rpc Public

    The JSON-RPC interface for the KeY theorem prover

    KeYProject/key-rpc's past year of commit activity
    Java 0 GPL-2.0 0 0 5 Updated Sep 28, 2026
  • key Public

    KeY Theorem Prover for Deductive Java Verification

    KeYProject/key's past year of commit activity
    Java 88 46 337 (2 issues need help) 45 Updated Sep 26, 2026
  • key-docs Public

    Documentation for the KeY Theorem Prover

    KeYProject/key-docs's past year of commit activity
    TeX 4 6 8 2 Updated Sep 8, 2026
  • setup-smt Public

    Github Action for setting up some SMT solvers

    KeYProject/setup-smt's past year of commit activity
    TypeScript 0 MIT 0 0 1 Updated Sep 2, 2026
  • TauKeY Public Forked from MrGunflame/keyui

    A tauri based UI for KeY Prover backends

    KeYProject/TauKeY's past year of commit activity
    Svelte 0 GPL-3.0 3 0 0 Updated Aug 19, 2026
  • KeYProject/Jerboa-KeY-case-study's past year of commit activity
    Java 0 1 0 0 Updated Jul 6, 2026
  • key-javadoc Public
    KeYProject/key-javadoc's past year of commit activity
    HTML 0 0 0 1 Updated Jul 1, 2026
  • nonull-rac Public
    KeYProject/nonull-rac's past year of commit activity
    Java 0 0 0 2 Updated Jun 3, 2026
  • .github Public
    KeYProject/.github's past year of commit activity
    0 1 0 0 Updated Jan 13, 2026
  • ips4o-verify Public Forked from jwiesler/ips4o-verify

    Case Study of the Verification of In-Place Parallel Super Scalar Samplesort Algorithm in Java

    KeYProject/ips4o-verify's past year of commit activity
    Java 2 BSD-2-Clause 2 0 0 Updated Oct 6, 2025