Skip to content

Release Notes

3.0.0 (2026-07-23)

Here, we are only describing the top of the patch iceberg which this release brings. All in all

6589 files changed, 306142 insertions(+), 435285 deletions(-)

Please see here, for the autogenerated full-detailed lists:

Release: Full Changelog

Exciting New Features 🎉

Java 25

Internally, KeY used recoder to parse Java which got stucked in the year 2009. With the transition to JavaParser, we can finally look into the future. The current fork which supports ProofJava, SchemaJava, and Java 21+ in a unified grammar is here wadoon/key-javaparser. PR 3120 enables support for newer Java syntax: We support for var variable declarations), e.g., var x = 0;. Java Records) are will automatically reduced to regular Java classes with generated methods and contracts, incl. support for compact constructors. TextBlockLiterals) ("""..."""), multi-catch-clauses in try-statements and try-with-resources are similar handled.

Proof Scripts

Proof Scripts got a larger update for 3.0 extending their capabilities. A new parser replaced the hand-written proof script parser, resulting in the earlier detection of syntax errors. It also makes proof scripts first-class citizens in KeY files - instead of embedding scripts in string literals. User can now write them directly: \proofscript { andLeft; andRight; rule a ==> b; }. The introduction of higher-order commands allows to easily extend the proof scripts with complex behavior easily. Proof commands can receive blocks of sub-commands like integer-split "<0" : { auto; } "=0" : { instantiate; } ">0" : { tryclose; } or even if "cond" { .. then ..} {.. else ..}. A simplie AST is now available for proof scripts (see ScriptCommandAst class) abstracting the script sources into a simple record containing command name, positional/keyword arguments, sub-commands, and location information enabling JML script integration. Finally, JML scripts have landed in KeY, bringing proof scripts into JML comments, allowing scripts to be written directly alongside specifications and executed during automatic verification—for example, embedding proof guidance within /*@ ... @*/ JML annotations so that proof node localization becomes natural and users can leverage JML expressions without leaving the specification language. Together, these changes transform proof scripts from an afterthought into an integrated, type-safe, and expressive component of the KeY verification workflow.

Modularity and Extensibility

Our efforts of a modular KeY reshaped internal sturctures: Proof objects, like sequents, proof objects, goals, rules, and the prover main loop—into are now in new modules *.ncore.*. The calucli for InfFlow and WD are push into separate modules) witnessing the modularization capabailities of key.core and key.ncore. As these calculi are not weaved into the Core, users must now activate these calculus by selected the profiles (i.e., java-infflow, java-wd). The loading dialog received an option panel for the profile selection.

Parametric Sorts

We fitted KeY's type system to the upcoming generics support. Add Polymorphic Sorts and Functions were introduced using a syntax like PSeq<[E]> and select<[int]>, along with matching logic, support for polymorphic datatypes, and co- and contravariance. Sort depending functions were purged, e.g., int::select, in favor of parametric functions with parametric function syntax (select<[int]>). Sort aliases are helping to avoid long sort names inthe logic, e.g., \alias IntSet = Set<[int]>;.

Not exciting but changes with impact

Changed defaults

We made \sameUpdateLevel default in all Taclets. This prevents a common user error, and increase the user experience.

The immutability of final fields is now handled via a "secondary" immutable heap. For example, specifiying the invariance of final fields in loop invariants

Performance

ImmutableList got an extensive overhaul and many operations are now non-copying in O(1). ImmutableArray is deprecated.

Performance improvements in cost computation and proof related algorithms and data structures.

Development

KeY uses a semantic versioning scheme now with major.minor.patch. Development version has the addition -dev. The old scheme: odd versions are development, and even version are releases, are dropped. 3.0.0 is the current version, 3.1.0-dev the current development, and this branch will become 3.1.0 on release.

KeY is built and tested w.r.t. to Java 21 Modules are not supported yet, blocked package uniqueness and stringtemplate4.

The classes Triple<A,B,C> and Quadruple<A,B,C,D> are gone for maintainability and readability. Please use Java records instead.

KeY uses Path now internally. Path is more plattform sensitive, you can experience difference on your code between Windows/Linux.

The key.api package was deleted. This package was started once for a clear interface for the ProofScriptDebugger, but never reached the maturity and usefulness. Useful parts have been into the other classes.

The problem header in problem files are now correctly treated.

MetaSpace is the companion of the namespaces, catching and gathering proof irrelevant information like documentation and origin of KeY entities.

Revivals

The test case generation was overlooked and refreshed to modern standard. For example, build files (pom.xml, build.gradle) are now generated for compiling and running the tests. Only JUnit 5 is support. TestNG and JUnit 4 are removed.

Configuration

Configurations are now versioned (e.g., ~/.key/v3.0/) with read-only fallback to previous versions.

The configuration SMT solvers got more structured using JSON. Also the look-up folder for the smt-solver configuration was changed allowing project-local configuration.

Features

Dependencies

Over 180 other Pull Requests for minor features, 🐛 bug fixes and other changes are not mentioned, but not forgotten. Please consult the generated changelog for a full view..

2.13.0 (2025-08-XX)

This is the last release with recoder backend!

2.12.3 (2024-09-08)

Highlights of this release (see the GitHub release notes for the complete list of changes):

Language and calculus

  • Support for user-defined algebraic data types (ADTs) in .key files, including destructors.
  • New function symbol seqUpd for sequence updates.
  • JML: immutable and valid set statements, support for \TYPE, configurable enabled keys for JML condition evaluation (with a status line indicator).
  • Problem statements in .key files can also be given as a (semi-)sequent.

User interface

  • Heap/memory indicator in the status bar.
  • Help buttons for extension settings; extension actions in context submenus are sorted consistently.
  • Improved error reporting and nicer parse error messages.
  • The coarse "experimental" flag was replaced by fine-grained feature flags.

Performance and SMT

  • Proof caching uses a dependency graph to increase the hit rate; dependency tracking for proof slicing is optional.
  • New Z3_QF solver variant; fixes to the SMT translation (bound variables, dependency issues) and to solver paths on Windows.

Infrastructure

  • Java 21 runtime used for testing; JSR305 annotations replaced by JSpecify; nullness checking activated for key.ncore.
  • Various bug fixes (proof tree updates, node selection between proofs, taclet pretty printing, startup crash with missing ~/.key/colors.json, …).

2.12.2 (2023-11-10)

This release contains bug fixes and performance enhancements.

Performance:

  • Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers.

Bug Fixes:

  • The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type.
  • Nullable and non-null modifiers attached to model methods are no longer lost.
  • Term rule indices are now always up-to-date, preventing potential prover crashes.
  • The counter-example dialog no longer freezes the GUI, if the example generation fails.
  • The actual proof status and proof status icon in the task overview are now consistent after pruning without requiring a manual refresh.

2.12.1 (2023-10-13)

Bug fixes

  • SMT solvers are properly terminated on timeout
  • Proof Macro statistics are kept visible and only count the newly applied rules
  • Stop button is disabled after use, re-enabled after stop completes (this is to avoid double activation)
  • Fully disable origin tracking if it is disabled
  • Proof slicing works even if a cut introduced no new formulas in any branch
  • When marking goal(s) as interactive/automatic, proof tree no longer loses expansion state
  • Fix proof tree behaviour when toggling goals
  • Fix branch selection in caching
  • Fix gradle detection of git branch
  • Fix unit test
  • Fix environments not disposed in tests, keep strategy info visible after applying
  • Proof macro: record statistics correctly
  • Fix: KeY files with errors cannot be edited

2.12.0 (2023-08-18)

Breaking changes

  • The minimum required JDK version is set to 11.
  • This release contains breaking changes for the reloading of older proofs:
    • Integers in specifications are now considered as unbounded (i.e. \bigint, math mode specifiers can be used to deviate from the default).
    • The list of rule sets used by the One-Step-Simplifier has changed.
    • JML assertions are handled as a standalone construct and not as a block contract anymore.

Highlights

Features

UI/UX Improvements

🛠 Maintenance/Internal Changes

🐛 Bug Fixes

We like to thank our contributors for this release, namely:

Alicia Appelhagen, Richard Bubel, Lukas Grätz, Christian Hein, Arne Keller, Michael Kirsten, Florian Lanzinger, Wolfram Pfeifer, Mike Schwörer, Benjamin Takacs, Samuel Teuber, Mattias Ulbrich, Alexander Weigl, Julian Wiesler

2.10.0 (2021-12-23)

Core

  • IMP: New SMT translation (!312), rework of the SMT communication (!381), and smaller fixes (!394)
  • IMP: Renovating the KeY parser (!278)
  • IMP: Rewrite of the JML parser in ANTLR (!306) with better exception message (!376)
  • IMP: JML-Extension: Assert/Assume and *_free for block contracts (!342)
  • FIX: Comment attachment in recoder (!399, !401)
  • FIX: Collision of auxiliary contract (!396)
  • FIX: Path handling of key files (!395)
  • FIX: Pruning in closed branches looses rules (!388, #1480)
  • FIX: Repaired file information if a directory is opened in KeY (!386, #1530)
  • FIX: Proof loading in the CLI (!385)
  • FIX: Invalid URLs under Windows (#1504, !264)
  • FIX: lost error messages due to MalformedURLException (!290, #1529)
  • FIX: catch headless to make key --auto runnable again (!382)
  • FIX: \singleton of a non-location (e.g., \singleton(3)) now raises an error (!377)
  • FIX: Completeness gap for array types (!367, #1566)
  • FIX: add loop scope unwind (!326)

UI

  • IMP: A better dialog for warnings (!374)
  • IMP: Performance tuning and fixes for ProofTree (!391)
  • IMP: Enables selection of proof in Proof Differences view (!256)
  • IMP: Better SourceView Tooltip (!379)
  • IMP: Add setting to disable load examples dialog window (!368)
  • IMP: Enable syntax highlighting for JML starting with annotation markers (!325)
  • FIX: make proof to load from bundle selectable (!237)
  • FIX: Escaping comma when saving bookmarked filenames of KeYFileChooser (!387, #1551)
  • FIX: make exception dialog able to show files in Jar files (!383)
  • FIX: Resolve "SMT Option GUI throws NPE on startup" (!373)

Development

  • Enabling of SonarQube in Merge Requests (!323, !378)
  • Dependency fixes for Gradle 7 (!372)

We like to thank all the contributor to this release:

Alexander Weigl, Alicia Appelhagen, Benjamin Takacs, Florian Lanzinger, Jonas Schiffl, Julian Wiesler, Lukas Grätz, Mattias Ulbrich, Michael Kirsten, Richard Bubel, Wolfram Pfeifer

2.8.0 (2020-12-01)

Logic

  • NEW: bsum taclets (!96)
  • NEW: Taclets for more flexible handling of observer depency (!177)
  • NEW: Loop contracts improvements (!188)
  • NEW: Loop scopes: a new rule for proving loop invaraints (!313, !326)
  • NEW: Support for Annotation Marker in JML (!308)
  • NEW: created new file intDiv.key for newly added taclets concerning (!182, !171, !180, !157, !152, !144, !141, !135, !98)
  • NEW: SMT preparation macro (!165)
  • NEW: Completion Scopes (!305)
  • FIX: Bugfixing handling of program variables of type "any" and parsing (!133)
  • NEW: \infinite_uniton(int x; x >= 0; this[x]) is now available in binder syntax: (\infinite_uniton int x; x >= 0; this[x]). Old form is deprecated and will be removed in later versions. (!132)
  • NEW: Adding "System.arraycopy" with contract to JavaRedux (!137)
  • NEW: Explizit excption for nested updates (allowed in the KeY book, unsupported by implementation) (!319)
  • FIX: Speed up in saving proofs (!120)
  • FIX: Incompleteness issue when rewite taclet was applied and the goaltemplate… (!119)
  • NEW: Loop contract (!?, !73)
  • NEW: Loading and Storing proofs with compression (gzip) (!12)
  • NEW: Saving of proofs (incl. dependening resources) into one file (zip) called "proof bundle" (!237)
  • FIX: Fix of inner blocks (!82)
  • FIX: KeY read files character-wise, now the file content is cached (!XXX)
  • More jml synonyms (!85)
  • FIX: user-provided notes are saved within the proof file (!304)
  • FIX: Origin labels for user interactions could not be parsed
  • FIX: Method signature resolve in JML expressions (!309)

UI

  • NEW: Unifying and polishing the user interface (!123):
  • KeY uses a docking framework, including storable/loadable layouts (!189)
  • The settings are concentrated inside one dialog (!189, !266)
  • Adaptable colors and key strokes (!189, !236, !254)
  • Adaptable clutter rules (!7)
  • Key based navigation within the proof tree view (!198)
  • FIX: Handling of regex in search (!199)
  • NEW: Icons !227
  • NEW: Heatmaps: Coloring formulae on the sequent based on their change activity (!38, !140)
  • NEW: Saving of proof bundles (!148, !310)
  • NEW: View of the current source code marking executed parts. (!99, !260, !263, !267, !325)
  • NEW: GUI Extension inferface: You can easily plugin new GUI elements.
  • NEW: Origin labels tracks the origin of formulae within a sequence (!122, !248)
  • NEW: Intraction logging (HacKeYthon'18) brings logging of user interaction with exports to Proof Scripts (!84)
  • NEW: Proof exploration
  • NEW: Favourites in file dialogs (!252)
  • NEW: License dialog (!253)
  • NEW: View for proof differences based on formula distance matching (!255)
  • NEW: Schiffl's search filter (!4)
  • NEW: Pre-select previous selected contract in ProofManagementDialog (!287)
  • FIX: Parsing of char, integer and long literals (!9, #1446, !214, !196)
  • FIX: Collision of heatmap and search colors (!178)
  • FIX: Slightly less confusing presentation of SMT solver results (!160)
  • FIX: Cluttering with the status line (!244)
  • NEW: Allow macro application via keyboard shortcut from tree (!268)
  • NEW: Open Java files without considering a classpath (!243)

Scripts

  • NEW: Rewrite command (!51)
  • FIX: Several fixes and breaking changes: (!153, !146, !145)
  • NEW: Improvements to the proof scripts (!314)

Environment

  • NEW: Gradle became build tool (!179, !205, !208, !209, !280)
  • Changes to the test infrastructure (!196)
  • Export of maven dependecies
  • New distribution formats: either a FatJar or zip file
  • NEW: Quality assessment via sonarqube and sonarcloud (!323)
  • Java 11 ready (!47)
  • remove of JavaFX dependencies (!95)
  • Integrate tests for well-definedness checks (!87 )

Eclipse

  • Support of Eclipse PHOTON (!74)

Seveal small and large bug fixes:

(!331, !297, !296, !293,!290, !288, !286, !284, !277, !276, !273, !272, !271, !270, !265, !264, !234, !228, !227, !225, !224, !222, !219, !213, !212, !209, !208, !205, !203, !201, !200, !199, !192, !190, !173, !170, !167, !163, !162, !158, !156, !154, !153, !151, !146, !145, !139, !136, !133, !131, !119, !117, !108, !99, !92, !83, !82, !81, !78, !77, !75, !73, !71, !70, !69, !68, !67, !66, !65, !58, !52, !47, !46, !45, !40, !39, !37, !33, !31, !30, !24, !23, !22, !14, !13, !10, !9, !8, !7, !3, !2)

We like to thank all the contributor to this release:

Alexander Weigl, Carsten Csiky, Dominic Steinhöfel, Florian Lanzinger, Hans-Dieter Hiep, Jelle Kübler, Jonas Schiffl, Lukas Grätz, Lulu Luong, Mattias Ulbrich, Michael Kirsten, Mihai Herda, Peter Schmitt, Richard Bubel, Sarah Grebing, Wolfram Pfeifer

2.6.3 (2017-10-11)

2.6.2 (2017-04-13)

2.6.1 (2017-01-31)

2.6.0 (2016-12-22)

2.4.1 (2015-02-18)

2.4.0 (2015-02-17)

  • Information flow reasoning
  • Full support for symbolic execution with bitwise operations
  • Improved test case generation
  • Improved user interface
  • Support for CVC4 SMT solver backend

2.2.3 (2014-10-06)

  • Fix concurrency issue introduced in 2.2.2

2.2.2 (2014-07-11)

  • Support for CVC3 version 2.4.1 SMT backend
  • Bug fixes

2.2.1 (2014-05-27)

  • Test case generation using bounded SMT (requires Z3, OpenJML)
  • Bug fixes

2.2.0 (2014-04-29)

  • Counter example generation using bounded SMT (requires Z3)
  • Increased JML support / JML extensions
  • block contracts (extension) / assert statements
  • \min and \max numerical quantifiers
  • changed default semantics of signals_only to include unchecked exceptions
  • model methods (new implementation)
  • old clause (variable binder in contract)
  • nearly everything parseable
  • Verification of a large class of recursive methods
  • generalized variants to all ordered sets
  • Proof obligations for specification well-definedness
  • Term labels
  • Rule triggers (extended taclet syntax)
  • More efficient handling of heap disjointness and heap selects
  • Improved reasoning about bounded sums/products
  • User Interfaces
  • rule focus for inner nodes
  • improved search
  • detailed proof statistics
  • auto save and quick save features
  • keyboard shortcuts
  • Reduced memory footprint
  • A lot of bug fixes
  • Java 8 compatibility
  • Re-implemented .key parser

2.0.2 (2013-09-19)

  • Support for latest versions of Z3 and CVC3
  • Windows 8 compatibility
  • Fix a soundness issue with types and heap access
  • Various bug fixes

2.0.1 (2013-06-19)

  • Bug fixes
  • Incompleteness with Java integer arithmetics
  • Command line mode fixes
  • various other

2.0.0 (2013-04-18)

  • New explicit heap modeling
  • Data types for location sets and heaps
  • The heap is now a special (local) variable
  • Dynamic frames
  • JML extension for dynamic frame specification
  • Re-implementation of JavaCard transactions
  • Verification of (primitive) recursive methods
  • Sequence ADT
  • Nearly complete JML support
  • model fields and methods
  • initially clauses and class axioms
  • measured_by clauses
  • accessible clauses
  • sum and product comprehension
  • the \bigint type, mixed integer semantics
  • weak purity by default
  • reachability predicate
  • \index and \values keywords for enhanced for-loops
  • Escape to dynamic logic from within JML
  • MonKeY batch mode
  • GUI changes
  • new dialog to enter invariants interactively
  • search in sequents and proof trees
  • logical symbols in Unicode
  • Runnable from command line without windowing system
  • Improved integration of SMT solvers
  • SMT-LIB 2.0 backend interface
  • possible to run multiple solvers in parallel
  • support for integer division (Z3 only)

  • 150 bug fixes

  • Discontinued features
  • RTSJ support
  • Test case generation
  • OCL
  • Proof reuse

1.6.5 (2013-01-23)

  • Minor bugfixes
  • Java 7 compatibility

1.6.0 (2010-10-06)

  • Support for Strings
  • Enhanced JML support
  • Improved integration of external SMT solvers
  • Improved "verification-based testing" mechanism
  • Real Time Java (RTSJ) calculus
  • GUI improvements
  • Various bugfixes

1.4.0 (2009-03-25)

  • Unified proof obligation framework
  • sharing of proof obligations across different specification languages
  • unified API for adding new proof obligations
  • same GUI elements used for all specification languages
  • more elegant translation of \old, @pre-like constructs
  • Improved JavaCard DL Specification interface
  • specification of DL invariants
  • Rewrite of JML front-end
  • ghost variables/fields and JML set statement
  • non_null by default
  • \old in loop invariants supported
  • \object_creation(type) in JML assignable clauses
  • New standalone OCL front-end
  • discontinued support for Borland Together integration
  • Java language support enhancements:
  • enum types (partially)
  • inner and anonymous classes
  • enhanced for loop
  • variable method arguments
  • covariant method signature
  • Generation of JML specifications
  • Strictly pure queries can be pushed directly into an update
  • Stable proof loading and saving
  • Classpath directive
  • various bugfixes

1.2.0 (2007-11-30)

  • significantly improved proof strategies wrt. quantifier treatment and arithmetics
  • improved proof tree view, i.e.
  • hiding of closed subtrees
  • hiding of intermediate proof steps
  • search in proof tree
  • improved proof saving and loading
  • includes alpha version of the visual debugger
  • various bugfixes

1.0.1:

  • fixed an installation problem when KeY had not been installed before

1.0.0:

  • KeY-Book examples are based on this version (except Schorr-Waite, which provides a developer version on the book example site)
  • new proof-obligation generation framework
  • used currently only by the OCL translation; adaption of JML translation is underway
  • new method lemma rule
  • considerable improvements concerning arithmetics
  • lots of bugfixes and improved stability

1.0pre1a:

  • bug fixes and improvements
  • polynomial integer simplification

1.0pre1:

  • pre-release of upcoming 1.0
  • several improvements and fixes

0.99.2 (?)

  • fixed: Initialisation procedure of the KeY prover (KeY did not work properly if installed on a fresh system without a working KeY configuration file)
  • fixed: Source Code Distribution 0.99.1 was way too big

0.99.1 (?)

  • bug fixes concerning JML front-end

0.99 (?)

  • first version with the JML front-end
  • support of loop invariants
  • lots of new stuff
✓ This page was checked by aw.