Let's just try to be clear about terminology: KeY is an interactive theorem prover that includes an expansion strategy based on symbolic execution (typically, for unfolding a recursive call of a method). The user experience of writing proofs in KeY is closer to writing a TLA+ proof using TLAPS than calling a model checker or constraint solver, which are fully automatic. In particular, KeY requires inductive invariants, and can prove correctness for arbitrary instances.