List view

The Removal of Recoder

FeatureNew feature or requestNew feature or request

Java Parser

Status: Draft (not ready).

KeYProject/keynumber 3120

#3120 In KeYProject/key;

· wadoon opened on Apr 16, 2023

Proof Scripts in JML

JavaJMLParser

JML (Semantics)

P:HIGH

Proof Scripts

Review RequestWaiting for reviewWaiting for review

Status: Open (in progress).

KeYProject/keynumber 3657

#3657 In KeYProject/key;

· mattulbrich opened on Sep 8, 2025

Update and fix Broad Release Tests

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

Status: Open (in progress).

KeYProject/keynumber 3703

#3703 In KeYProject/key;

· wadoon opened on Dec 30, 2025

Multi Sets

Status: Draft (not ready).

KeYProject/keynumber 3698

#3698 In KeYProject/key;

· lks9 opened on Dec 11, 2025

Fix for #3683: Hiding package prefixes in sequent view

🐞 Bug

GUI

Review RequestWaiting for reviewWaiting for review

Status: Open (in progress).

KeYProject/keynumber 3684

#3684 In KeYProject/key;

· WolframPfeifer opened on Nov 12, 2025

fixes #3670: KeY does not know that enum constants are non-null

Status: Open (in progress).

KeYProject/keynumber 3676

#3676 In KeYProject/key;

· mattulbrich opened on Oct 24, 2025

Make user-defined sorts accessible in "\dl_" escapes

🐞 Bug

JML Parser

RFC"Request for comments" is the appeal for making and expressing your opinion on a topic."Request for comments" is the appeal for making and expressing your opinion on a topic.

Status: Open (in progress).

KeYProject/keynumber 3659

#3659 In KeYProject/key;

· WolframPfeifer opened on Sep 12, 2025

Add Polymorphic Sorts and Functions

FeatureNew feature or requestNew feature or request

KeY Parser

Review RequestWaiting for reviewWaiting for review

Status: Open (in progress).

KeYProject/keynumber 3652

#3652 In KeYProject/key;

· Drodt opened on Aug 13, 2025

Modular Features

Prover Core

Strategy

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

Status: Draft (not ready).

KeYProject/keynumber 3650

#3650 In KeYProject/key;

· Drodt opened on Aug 13, 2025

Improve the SMT translation by translating axiom taclets (mostly for invariants)

FeatureNew feature or requestNew feature or request

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

SMT

Status: Draft (not ready).

KeYProject/keynumber 3564

#3564 In KeYProject/key;

· WolframPfeifer opened on Feb 20, 2025

Fix slicing bug related to Evaluate Query

keyext.slicingModule: keyext.slicingModule: keyext.slicing

Status: Open (in progress).

KeYProject/keynumber 3393

#3393 In KeYProject/key;

· FliegendeWurst opened on Jan 31, 2024

Create a JSON-RPC for KeY

keyext.api

Status: Draft (not ready).

KeYProject/keynumber 3303

#3303 In KeYProject/key;

· wadoon opened on Oct 17, 2023

Solving the FP completeness issues in #1723

Calculus

Completeness

Status: Draft (not ready).

KeYProject/keynumber 3023

#3023 In KeYProject/key;

· mattulbrich opened on Feb 5, 2023

Expand OSS steps when saving a proof for more deterministic Proofs

FeatureNew feature or requestNew feature or request

RFC"Request for comments" is the appeal for making and expressing your opinion on a topic."Request for comments" is the appeal for making and expressing your opinion on a topic.

Status: Open (in progress).

KeYProject/keynumber 3707

#3707 In KeYProject/key;

· Drodt opened on Jan 8, 2026

Save proof independent settings, that are not used by the configuration

FeatureNew feature or requestNew feature or request

JavaPull requests that update Java codePull requests that update Java code

Status: Open (in progress).

KeYProject/keynumber 3700

#3700 In KeYProject/key;

· PiIsRational opened on Dec 15, 2025

Macro <code>auto-infflow</code> breaks UI Proof Tree

GUI

Information Flow Engine

Status: Open.

Bug

#3713 In KeYProject/key;

· wadoon opened on Jan 13, 2026

Information Flow proofs are not re-loadable

GUI

Information Flow Engine

Status: Open.

Bug

#3714 In KeYProject/key;

· wadoon opened on Jan 13, 2026

Recoder must be removed

🐞 Bug

🚀 Performance

Breaks API

FeatureNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

JavaPull requests that update Java codePull requests that update Java code

Java Parser

JavaJMLParser

JML (Semantics)

JML Parser

Status: Open.

Task

#3715 In KeYProject/key;

· wadoon opened on Jan 13, 2026

Ghost variable not properly handled in loop

🐞 Bug

✋ Soundness

Status: Open.

Bug

#3720 In KeYProject/key;

· FliegendeWurst opened on Jan 21, 2026

Add support for Annotation Processors in the Javac Extension

FeatureNew feature or requestNew feature or request

GUI

JavaPull requests that update Java codePull requests that update Java code

Status: Draft (not ready).

KeYProject/keynumber 3686

#3686 In KeYProject/key;

· PiIsRational opened on Nov 18, 2025

Loop scope rule doesn't include implicit conditions on local variables

Calculus

Status: Open.

Bug

#3728 In KeYProject/key;

· FliegendeWurst opened on Jan 28, 2026

Anonymize ghost variables in loop

🐞 Bug

Review RequestWaiting for reviewWaiting for review

✋ Soundness

Status: Open (in progress).

KeYProject/keynumber 3729

#3729 In KeYProject/key;

· Drodt opened on Jan 30, 2026

Taclet definition added to problemHeader

🐞 Bug

Proof Loading/Saving

Status: Open (in progress).

KeYProject/keynumber 3733

#3733 In KeYProject/key;

· wadoon opened on Feb 7, 2026