I have looked into it and OpenJML as well.
Both look promising, with KeY being “more formal” (as I understood it) and OpenJML a lower entry point to the layman.
Have you used it at your projects?
Would you mind to share your experience?
I haven’t used it. Ran across it when I was researching something related to stack machines.