KeY Enhancement Proposals (KEPs)

A KeY Enhancement Proposal describes a larger, still-evolving change to KeY — a new mechanism, a shift in an established workflow, or an experiment whose design is worth discussing before it settles. KEPs are deliberately more speculative than the rest of this documentation: a KEP may describe a feature that lives on a branch or in an open pull request, that is still being refined, or that may ultimately be reshaped or dropped.

Each KEP page states, at the top, its current status and the pull request (or branch) it corresponds to, so readers can tell how finished the described feature is and where to follow the discussion.

Index

• KEP-1: Taclet-Generating Transformers — capture aggregated proof steps (starting with the One Step Simplifier) as generated, separately provable taclets instead of opaque built-in steps.