List view

Soundness: Invariants, model methods and model fields need not be well-founded

🐞 Bug

P:HIGH

✋ Soundness

Status: Open.

#3155 In KeYProject/key;

· mattulbrich opened on Jun 5, 2023

Proof reordering (WIP)

FeatureNew feature or requestNew feature or request

GUI

Status: Draft (not ready).

KeYProject/keynumber 3141

#3141 In KeYProject/key;

· FliegendeWurst opened on May 15, 2023

Font scaling issues

🐞 Bug

GUI

Status: Open.

#3240 In KeYProject/key;

· FliegendeWurst opened on Aug 4, 2023

Update to LocationVariable is ignored after pruning

🐞 Bug

Calculus

Status: Open.

#3206 In KeYProject/key;

· gewitternacht opened on Jul 17, 2023

Cleanup: Making the build script fit for the future.

🛠 MaintenanceCode quality and related things w/o functional changesCode quality and related things w/o functional changes

Status: Draft (not ready).

KeYProject/keynumber 3552

#3552 In KeYProject/key;

· wadoon opened on Feb 15, 2025

Renovations for SMT solvers

External SolversAdditional Solvers such as (SMT, Isabelle, ...Additional Solvers such as (SMT, Isabelle, ...

SMT

Status: Open.

Task

#3575 In KeYProject/key;

· wadoon opened on Feb 28, 2025

Reactivate Checkstyle

github_actionsPull requests that update GitHub Actions codePull requests that update GitHub Actions code

🛠 MaintenanceCode quality and related things w/o functional changesCode quality and related things w/o functional changes

Status: Open (in progress).

KeYProject/keynumber 3539

#3539 In KeYProject/key;

· wadoon opened on Jan 22, 2025

Cleanup: Removal of the write and read settings using Properties

🛠 MaintenanceCode quality and related things w/o functional changesCode quality and related things w/o functional changes

Status: Draft (not ready).

KeYProject/keynumber 3549

#3549 In KeYProject/key;

· wadoon opened on Feb 15, 2025

Nullness Type System for key.core

HacKeYthonCandidate Issue for HacKeYthon '25Candidate Issue for HacKeYthon '25

🛠 MaintenanceCode quality and related things w/o functional changesCode quality and related things w/o functional changes

Status: Draft (not ready).

KeYProject/keynumber 3470

#3470 In KeYProject/key;

· wadoon opened on May 3, 2024

LLM support in KeY UI

Status: Draft (not ready).

KeYProject/keynumber 3687

#3687 In KeYProject/key;

· wadoon opened on Nov 19, 2025

module-info.java, 2nd attempt

Breaks API

Status: Open (in progress).

KeYProject/keynumber 3623

#3623 In KeYProject/key;

· wadoon opened on Jun 19, 2025

Migrate from ST4 to Apache Freemarker in keyext.proofmanagement

keyext.proofmanagementModule: keyext.proofmanagementModule: keyext.proofmanagement

🛠 MaintenanceCode quality and related things w/o functional changesCode quality and related things w/o functional changes

Status: Open (in progress).

KeYProject/keynumber 3621

#3621 In KeYProject/key;

· wadoon opened on Jun 16, 2025

JML ghost declarations should behave like set statements

JavaJMLParser

JML Parser

Status: Open.

Task

#3466 In KeYProject/key;

· wadoon opened on Apr 29, 2024

JML should receive an Abstract Syntax Tree

JavaJMLParser

JML (Semantics)

JML Parser

Status: Open.

Feature

#3716 In KeYProject/key;

· wadoon opened on Jan 14, 2026

Pfeifer/proof mgmt includes fix

FeatureNew feature or requestNew feature or request

keyext.proofmanagementModule: keyext.proofmanagementModule: keyext.proofmanagement

Status: Open (in progress).

KeYProject/keynumber 3757

#3757 In KeYProject/key;

· WolframPfeifer opened on Mar 11, 2026