v3.1.0

New issue

Open

Due by December 1, 2026

•Last updated Oct 5, 2026

e.g., v3.1.0

45% complete

Migrate to JMLtk
Unread
#3966 opened Aug 15, 2026 · Updated Oct 2, 2026
20
Not all KeY files in repo are parsable.
Bug
KeYProject/key#3602 · opened on May 10, 2025 · v3.1.0
5
Nullness checker not working Windows
Bug
KeYProject/key#3635 · opened on Jul 15, 2025 · v3.1.0
Rewriter of old to new settings format.
Unread
#3590 opened Apr 6, 2025 · Updated Aug 13, 2026Draft
1
Aftermath: Renovation of Test generation
Bug
KeYProject/key#3665 · opened on Sep 25, 2025 · v3.1.0
Draft: Add definition taclets for binaryAnd, binaryOr, and binaryXOr
Unread
#3174 opened Jun 19, 2023 · Updated Sep 15, 2026Draft
RunAllProofs disrespects JAVA_HOME
Bug
KeYProject/key#3630 · opened on Jul 9, 2025 · v3.1.0
Rewriting the settings in KeY files to the new format.
Unread
#3688 opened Nov 22, 2025 · Updated Aug 13, 2026Draft
Universe Type Rules
Unread
#3724 opened Jan 26, 2026 · Updated Sep 23, 2026Draft
2
Java 25 Features for KeY
Feature
KeYProject/key#3774 · opened on Mar 17, 2026 · v3.1.0
Migrate from ST4 to Apache Freemarker in keyext.proofmanagement
Unread
#3621 opened Jun 16, 2025 · Updated Jul 18, 2026
9
Proof reordering (WIP)
Unread
#3141 opened May 15, 2023 · Updated Jun 19, 2026Draft
3
LLM support in KeY UI
Unread
#3687 opened Nov 19, 2025 · Updated Oct 3, 2026Draft
Soundness: Invariants, model methods and model fields need not be well-founded
Bug
KeYProject/key#3155 · opened on Jun 5, 2023 · v3.1.0
1
Update to LocationVariable is ignored after pruning
Bug
KeYProject/key#3206 · opened on Jul 17, 2023 · v3.1.0
4
Font scaling issues
Bug
KeYProject/key#3240 · opened on Aug 4, 2023 · v3.1.0
2
JML ghost declarations should behave like set statements
Task
KeYProject/key#3466 · opened on Apr 29, 2024 · v3.1.0
Renovations for SMT solvers
Task
KeYProject/key#3575 · opened on Feb 28, 2025 · v3.1.0
JML should receive an Abstract Syntax Tree
Feature
KeYProject/key#3716 · opened on Jan 14, 2026 · v3.1.0
Lambda support by transformation
Unread
#3759 opened Mar 11, 2026 · Updated Jul 6, 2026Draft
Implement Switch-to-If Without Transformation
Feature
KeYProject/key#3765 · opened on Mar 14, 2026 · v3.1.0
1
Generation of Java AST classes
Unread
#3809 opened Apr 19, 2026 · Updated Oct 2, 2026Draft
Improve the SMT translation by translating axiom taclets (mostly for invariants)
Unread
#3564 opened Feb 20, 2025 · Updated Sep 19, 2026Draft
2
Solving the FP completeness issues in #1723
Unread
#3023 opened Feb 5, 2023 · Updated Jun 19, 2026Draft
12
Handle Switch in Taclets w/o Transformer
Unread
#3761 opened Mar 13, 2026 · Updated Jul 14, 2026Draft
3

Navigation Menu

v3.1.0

Migrate to JMLtk

Not all KeY files in repo are parsable.

Nullness checker not working Windows

Rewriter of old to new settings format.

Aftermath: Renovation of Test generation

Draft: Add definition taclets for `binaryAnd`, `binaryOr`, and `binaryXOr`

RunAllProofs disrespects JAVA_HOME

Rewriting the settings in KeY files to the new format.

Universe Type Rules

Java 25 Features for KeY

Migrate from ST4 to Apache Freemarker in keyext.proofmanagement

Proof reordering (WIP)

LLM support in KeY UI

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

Update to LocationVariable is ignored after pruning

Font scaling issues

JML ghost declarations should behave like set statements

Renovations for SMT solvers

JML should receive an Abstract Syntax Tree

Lambda support by transformation

Implement Switch-to-If Without Transformation

Generation of Java AST classes

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

Solving the FP completeness issues in #1723

Handle Switch in Taclets w/o Transformer

Issues