Skip to content

KeY Developer Documentation

Commands

Proof Script Commands¶

This document lists all proof script commands available in the KeY system. The general ideas of scripts, their syntax, and control flow are described in the general documentation files on proof scripts.

Field	Value
Generated on:	Mon Oct 06 15:01:02 CEST 2025
Branch:	jmlScripts
Version:	2.12.4-dev
Commit:	382f4ce88f33ee3eb90e34b05e23451863271d4c

The commands are organised into categories. Each command may have multiple aliases under which it can be invoked. The first alias listed is the primary name of the command. There named and positional arguments. Named arguments need to be prefixed by their name and a colon. Positional arguments are given in the order defined by the command. Optional arguments are enclosed in square brackets.

Category Control¶

Command `activate`¶

Reactivates the first open (not necessarily enabled) goal. This can be useful after a 'leave' command to continue working on a complicated proof where 'tryclose' should not apply on certain branches temporarily, but where one still wants to finish the proof.

Command `assertOpenGoals`¶

The assert command checks if the number of open and enabled goals is equal to the given number. If not, the script is halted with an error message.

Note: This command was called "assert" originally.

Usage:¶

assertOpenGoals goals:⟨Integer⟩

Parameters:¶

goals (named option, type Integer):

Command `assume`¶

The assume command is an unsound taclet rule and adds a formula to the antecedent of the current goal Can be used for debug and proof exploration purposes.

Usage:¶

assume ⟨JTerm (formula)⟩

Parameters:¶

formula (1^st positional argument, type JTerm):
The formula to be assumed.

Command `axiom`¶

Caution! This proof script command is deprecated, and may be removed soon!

This command is deprecated and should not be used in new scripts. Use the equivalent assume command instead.

The assume command is an unsound taclet rule and adds a formula to the antecedent of the current goal Can be used for debug and proof exploration purposes.

Usage:¶

axiom ⟨JTerm (formula)⟩

Parameters:¶

formula (1^st positional argument, type JTerm):
The formula to be assumed.

Command `echo`¶

A simple "print" command for giving progress feedback to the human verfier during lengthy executions.

Usage:¶

echo ⟨String (message)⟩

Parameters:¶

message (1^st positional argument, type String):
The message to be printed.

Command `exit`¶

Exits the currently running script context unconditionally. (In the future, there may try-catch blocks to react to this).

Command `failonclosed`¶

Caution! This proof script command is deprecated, and may be removed soon!

Usage:¶

failonclosed ⟨String (command)⟩

Parameters:¶

command (1^st positional argument, type String):

Command `hide`¶

The hide command hides all formulas of the current proof goal that are in the given sequent. The formulas in the given sequent are hidden using the taclets hide_left and hide_right.

Usage:¶

hide ⟨Sequent (sequent)⟩

Parameters:¶

sequent (1^st positional argument, type Sequent):
The sequent containing the formulas to hide. Placeholders are allowed.

Command `leave`¶

Marks the current goal to be ignored by the macros.

Command `onAll`¶

Executes a given block of script commands on all open goals. The current goal is set to each open goal in turn while executing the block. It expects exactly one positional argument, which is the block to be executed on each goal.

Examples:¶

onAll { smt solver="z3"; }
onAll { auto; }

Command `script`¶

Includes and runs another script file.

Usage:¶

script ⟨String (filename)⟩

Parameters:¶

filename (1^st positional argument, type String):
The filename of the script to include. May be relative to the current script.

Command `select`¶

The select command selects a goal in the current proof. Exactly one of the parameters must be given. The next command will then continue on the selected goal.

Examples:¶

select formula: (x > 0)
select number: -2
select branch: "Loop Invariant"

Usage:¶

select [branch:⟨String⟩] [formula:⟨JTerm⟩] [number:⟨Integer⟩]

Parameters:¶

branch (optional named option, type String):
The name of the branch to select. If there are multiple branches with the same name, the first one is selected.
formula (optional named option, type JTerm):
A formula defining the goal to select. May contain placeholder symbols. If there is a formula matching the given formula in multiple goals, the first one is selected.
number (optional named option, type Integer):
The number of the goal to select, starts with 0. Negative indices are also allowed: -1 is the last goal, -2 the second-to-last, etc.

Command `skip`¶

Does exactly nothing.

Command `unhide`¶

The unhide command re-inserts formulas that have been hidden earlier in the proof using the hide command. It takes a sequent as parameter and re-inserts all formulas in this sequent that have been hidden earlier.

Usage:¶

unhide ⟨Sequent (sequent)⟩

Parameters:¶

sequent (1^st positional argument, type Sequent):
The sequent containing the formulas to be re-inserted. Placeholders are allowed.

Category Fundamental¶

Command `assert`¶

Alias for command → cut

Command `auto`¶

The AutoCommand invokes the automatic strategy "Auto" of KeY (which is also launched by when clicking the "Auto" button in the GUI). It can be used to try to automatically prove the current goal. Use with care, as this command may leave the proof in a incomprehensible state with many open goals.

Use the command with "close" to make sure the command succeeds for fails without changes.

Usage:¶

auto [all] [classAxioms] [dependencies] [expandQueries] [modelsearch] [add:⟨String⟩] [breakpoint:⟨String⟩] [matches:⟨String⟩] [only:⟨String⟩] [steps:⟨int⟩]

Parameters:¶

all (flag):
Deprecated. Apply the strategy on all open goals. There is a better syntax for that now.
classAxioms (flag):
Enable automatic and eager expansion of symbols. This expands class invariants, model methods and fields and invariants quite eagerly. May be an enabler (if a few definitions need to expanded), may be a showstopper (if expansion increases the complexity on the sequent too much).
dependencies (flag):
Enable dependency reasoning. In modular reasoning, the value of symbols may stay the same, without that its definition is known. May be an enabler, may be a showstopper.
expandQueries (flag):
Automatically expand occurrences of query symbols using additional modalities on the sequent.
modelsearch (flag):
Enable model search. Better for some (types of) arithmetic problems. Sometimes a lot worse.
add (optional named option, type String):
Additional rules to be used by the auto strategy. The rules have to be given as a comma-separated list of rule names and rule set names. Each entry can be assigned to a priority (high, low, medium or a natural number) using an equals sign. Cannot be combined with the 'only' parameter.
breakpoint (optional named option, type String):
When doing symbolic execution by auto, this option can be used to set a Java statement at which symbolic execution has to stop.
matches (optional named option, type String):
Run on the formula matching the given regex.
only (optional named option, type String):
Limit the rules to be used by the auto strategy. The rules have to be given as a comma-separated list of rule names and rule set names. Each entry can be assigned to a priority (high, low, medium or a natural number) using an equals sign. All rules application which do not match the given names will be disabled. Cannot be combined with the 'add' parameter.
steps (optional named option, type int):
The maximum number of proof steps to be performed.

Command `cut`¶

The cut command makes a case distinction (a cut) on a formula on the current proof goal. From within JML scripts, the alias 'assert' is more common than using 'cut'. If followed by a \by proof suffix in JML, it refers the sequent where the cut formula is introduced to the succedent (i.e. where it is to be established).

Usage:¶

cut ⟨JTerm (formula)⟩

Parameters:¶

formula (1^st positional argument, type JTerm):
The formula to make the case distinction on.

Aliases:¶

cut, assert

Command `dependency`¶

The dependency command applies a dependency contract to a specified term in the current goal. Dependency contracts allow you to do modular reasoning. If for a heap-dependent function symbol, no changes occur inside the dependency set of this function, the result remains the same. This can be applied to model methods, model fields or invariants.

Usage:¶

dependency on:⟨JTerm⟩ [heap:⟨JTerm⟩]

Parameters:¶

on (named option, type JTerm):
The term to which the dependency contract should be applied. This term must occur in the current goal. And it must be the invocation of a heap-dependent observer function symbol.
heap (optional named option, type JTerm):
The heap term to be compared against. If not given, the default heap is used.

Command `focus`¶

The command "focus" allows you to select formulas from the current sequent to focus verification on. This means that all other formulas are discarded (i.e. hidden using hide_right, hide_left).

Benefits are: The automation is guided into focussing on a relevant set of formulas.

The selected set of sequent formulas can be regarded as an equivalent to a believed "unsat core" of the sequent.

Examples:¶

focus x > 2 ==> x > 1 only keeps the mentioned to formulas in the current goal removing all other formulas that could distract the automation.

Usage:¶

focus ⟨Sequent (toKeep)⟩

Parameters:¶

toKeep (1^st positional argument, type Sequent):
The sequent containing the formulas to keep. It may contain placeholder symbols.

Command `instantiate`¶

Instantiate a universally quantified formula (in the antecedent; or an existentially quantified formula in succedent) by a term. One of var or formula must be specified. If var is given, the formula is determined by looking for a particular occurrence of a quantifier over that variable name. If formula is given, that quantified formula is used directly. with must be specified.

Examples:¶

instantiate var:a occ:2 with:a_8 hide
instantiate formula:"\forall int a; phi(a)" with="a_8"

Usage:¶

instantiate [hide] with:⟨JTerm⟩ [formula:⟨JTerm⟩] [occ:⟨int⟩] [var:⟨String⟩]

Parameters:¶

hide (flag):
If given, the rule used for instantiation is the one that hides the instantiated formula to prevent it from being used for further automatic proof steps.
with (named option, type JTerm):
The term to instantiate the bound variable with. Must be given.
formula (optional named option, type JTerm):
The toplevel quantified formula to instantiate. Placeholder matching symbols can be used.
occ (optional named option, type int):
The occurrence number of the quantifier over 'var' in the sequent starting at 1. Default is 1.
var (optional named option, type String):
The name of the bound variable to instantiate.

Command `macro`¶

The MacroCommand invokes one of KeY's macros. The macro must be registered to KeY's services.

The command takes the name of the macro as first argument, followed by optional parameters to configure the macro.

The macro is applied to the first open automatic goal in the proof.

Examples:¶

macro "prop-split"
macro "auto-pilot"

Usage:¶

macro ⟨String (macroName)⟩ instantiations... [matches:⟨String⟩] [occ:⟨Integer⟩]

Parameters:¶

macroName (1^st positional argument, type String):
Macro name
instantiations...: (options prefixed by arg_, type String):
Macro parameters, given as varargs with prefix 'arg_'. E.g. arg_param1=value1
matches (optional named option, type String):
Run on formula matching the given regex
occ (optional named option, type Integer):
Run on formula number "occ" parameter

Command `oss`¶

The oss command applies the one step simplifier on the current proof goal. This simplifier applies a set of built-in simplification rules to the formulas in the sequent. It can be configured to apply the one step simplifier only on the antecedent or succedent. By default, it is applied on both sides of the sequent.

Usage:¶

oss [antecedent:⟨Boolean⟩] [recentOnly] [succedent:⟨Boolean⟩]

Parameters:¶

antecedent (optional named option, type Boolean):
Application of the one step simplifier can be forbidden on the antecedent side by setting this option to false. Default is true.
recentOnly (flag):
Limit the application to the recently added or changed formulas. Deactivates the antecedent and succedent options.
succedent (optional named option, type Boolean):
Application of the one step simplifier can be forbidden on the succedent side by setting this option to false. Default is true.

Command `rule`¶

This command can be used to apply a calculus rule to the currently active open goal.

Examples:¶

rule cut inst_cutFormula: (a > 0) applies the cut rule on the formula a > 0 like the cut command.
rule and_right on=(__ & __) applies the rule and_right to the second occurrence of a conjunction in the succedent.
rule my_rule on=(f(x)) formula="f\(.*search.*\)" applies the rule my_rule to the term f(x) in a formula matching the regular expression.

Usage:¶

rule ⟨String (rulename)⟩ instantiations... [formula:⟨JTerm⟩] [matches:⟨String⟩] [occ:⟨Integer⟩] [on:⟨JTerm⟩]

Parameters:¶

rulename (1^st positional argument, type String):
Name of the rule to be applied.
instantiations...: (options prefixed by inst_, type JTerm):
Instantiations for term schema variables used in the rule.
formula (optional named option, type JTerm):
Top-level formula in which the term appears. This may contain placeholders.
matches (optional named option, type String):
Instead of giving the toplevl formula completely, a regular expression can be specified to match the toplevel formula.
occ (optional named option, type Integer):
Occurrence number if more than one occurrence matches. The first occurrence is 1. If ommitted, there must be exactly one occurrence.
on (optional named option, type JTerm):
Term on which the rule should be applied to (matching the 'find' clause of the rule). This may contain placeholders.

Command `smt`¶

The smt command invokes an SMT solver on the current goal(s). By default, it uses the Z3 solver on the first open automatic goal. If the option 'all' is given, it runs on all open goals. If the option 'solver' is given, it uses the specified solver(s) instead of Z3. Multiple solvers can be specified by separating their names with commas. The available solvers depend on your system: KeY supports at least z3, cvc5.

Usage:¶

smt [all] solver:⟨String⟩ timeout:⟨int⟩

Parameters:¶

all (flag):
Deprecated! Apply the command on all open goals instead of only the first open automatic goal.
solver (named option, type String):
timeout (named option, type int):

Command `witness`¶

Provides a witness symbol for an existential or universal quantifier. The given formula must be present on the sequent. Placeholders are allowed. The command fails if the formula cannot be uniquely matched on the sequent. The witness symbol as must be a valid identifier and not already used as function, predicate, or program variable name. The new function symbol is created as a Skolem constant.

Example:¶

If the sequent contains the formula \exists int x; x > 0 in the antecedent then the command witness "\exists int x; x > 0" as="x_12" will introduce the witness symbol x_12 for which "x_12 > 0` holds and is added to the antecedent.

Usage:¶

witness ⟨JTerm (formula)⟩ as:⟨String⟩

Parameters:¶

formula (1^st positional argument, type JTerm):
The formula containing the quantifier for which a witness should be provided. Placeholders are allowed.
as (named option, type String):
The name of the witness symbol to be created.

Category Internal¶

Command `@echo`¶

Caution! This proof script command is deprecated, and may be removed soon!

An internal command to switch on/off echoing of executed commands.

Usage:¶

@echo ⟨String (command)⟩

Parameters:¶

command (1^st positional argument, type String):

Command `cheat`¶

Use this to close a goal unconditionally. This is unsound and should only be used for testing and proof debugging purposes. It is similar to 'sorry' in Isabelle or 'admit' in Rocq.

Command `javascript`¶

This command allows to execute arbitrary JavaScript code. The code is executed in a context where the current selected goal is available as goal and a function setVar(v,t) is available to set an abbreviation (where v is the name of the variable including the leading @ and t is either a term or a string that can be parsed as a term).

Example:¶

javascript {
  var x = goal.getAntecedent().get(0).getFormula();
  setVar("@myVar", x);
}

This command is powerful but should be used with care, as it can easily lead to unsound proofs if used incorrectly.

Usage:¶

javascript ⟨String (script)⟩

Parameters:¶

script (1^st positional argument, type String):
The JavaScript code to execute.

Command `saveInst`¶

Command `saveNewName`¶

Special "Let" usually to be applied immediately after a manual rule application. Saves a new name introduced by the last rule which matches certain criteria into an abbreviation for later use. A nice use case is a manual loop invariant rule application, where the newly introduced anonymizing Skolem constants can be saved for later interactive instantiations. As for the let command, it is not allowed to call this command multiple times with the same name argument (all names used for remembering instantiations are "final").

Usage:¶

saveNewName ⟨String (abbreviation)⟩ matches:⟨String⟩

Parameters:¶

abbreviation (1^st positional argument, type String):
The abbreviation to store the new name under, must start with @
matches (named option, type String):
A regular expression to match the new name against, must match exactly one name

Command `schemaVar`¶

Caution! This proof script command is deprecated, and may be removed soon!

Defines a schema variable that can be used in subsequent commands.

Usage:¶

schemaVar ⟨String (type)⟩ ⟨String (var)⟩

Parameters:¶

type (1^st positional argument, type String):
var (2^nd positional argument, type String):

Category JML¶

Command `__obtain`¶

Command that introduces a fresh variable with a given name and sort. Exactly one of such_that, equals, or from_goal must be given.

The command should not be called directly, but is used internally by the JML script support within KeY.

Usage:¶

__obtain var:⟨String⟩ [equals:⟨JTerm⟩] [from_goal:⟨boolean⟩] [such_that:⟨JTerm⟩]

Parameters:¶

var (named option, type String):
Name of the variable to be instantiated.
equals (optional named option, type JTerm):
Represented term for which this is an abbreviation.
from_goal (optional named option, type boolean):
Top-level formula in which the term appears.
such_that (optional named option, type JTerm):
Condition that is to be established for the fresh variable.

Category Uncategorized¶

Command `branches`¶

Usage:¶

branches ⟨String (mode)⟩ [branch:⟨String⟩] [child:⟨Integer⟩]

Parameters:¶

mode (1^st positional argument, type String):
branch (optional named option, type String):
child (optional named option, type Integer):

Command `expand`¶

Usage:¶

expand [formula:⟨JTerm⟩] [occ:⟨Integer⟩] [on:⟨JTerm⟩]

Parameters:¶

formula (optional named option, type JTerm):
occ (optional named option, type Integer):
on (optional named option, type JTerm):

Command `let`¶

Aliases:¶

let, letf

Command `letf`¶

Alias for command → let

Command `rewrite`¶

Usage:¶

rewrite find:⟨JTerm⟩ replace:⟨JTerm⟩ [formula:⟨JTerm⟩]

Parameters:¶

find (named option, type JTerm):
replace (named option, type JTerm):
formula (optional named option, type JTerm):

Command `set`¶

Usage:¶

set settings... [oss:⟨Boolean⟩] [stack:⟨String⟩] [steps:⟨Integer⟩] [userData:⟨String⟩]

Parameters:¶

settings...: (options prefixed by ``, type String):
key-value pairs to set
oss (optional named option, type Boolean):
Enable/disable one-step simplification
stack (optional named option, type String):
Push or pop the current settings to/from a stack of settings (mostly used internally)
steps (optional named option, type Integer):
Maximum number of proof steps
userData (optional named option, type String):
Set user-defined key-value pair (Syntax: userData:"key:value")

Command `tryclose`¶

Usage:¶

tryclose [⟨String (branch)⟩] [assertClosed] [steps:⟨Integer⟩]

Parameters:¶

branch (optional 1^st positional argument, type String):
assertClosed (flag):
steps (optional named option, type Integer):