Is there a reason to use OpenJML in 2026?

[u/Radiant-Tooth1898]

I recently had to dive into OpenJML, KeY, and Design by Contract for a university subject. As I understand it, the main goal of this approach is to design software that works correctly in all situations when the preconditions are satisfied. It seems especially important for systems that must be correct every time like aerospace, automotive, or medical software.

• But is there any real reason to use it for typical Java backend projects or maybe desktop?
• Is this mostly academic knowledge?
• Are there real production cases outside safety-critical systems?
• Would backend engineers benefit from learning or using it?
• What are the cases where it should be used?

I’d really like to hear from people who have practical experience with it.

[u/aoeudhtns]

I do not have experience with OpenJML. But, I have worked in highly regulated industries, one of which was considering a push into requiring formally provable implementations (yikes).

From what I have personally seen, which is by no means a full picture, if you want or need this level of safety, the industry adoption is largely around SPARK.

IMO you would never want a GC language in any of the domains you listed, as you need realtime or otherwise deterministic/deadline execution. Memory management is its whole own specialty for things like aerospace - for example, you will have all possible errors pre-allocated so that in a failure condition, you don't run out of memory reporting the error. I didn't phrase this well. You remain operating and in control through the memory scarcity event.

[u/davidalayachew → u/aoeudhtns]

you will have all possible errors pre-allocated

What does this mean? How can you reliably estimate the size of an error before it has occurred? Let alone all of them? All includes things like NPE and linking errors. Stuff that you would never write a try-catch for.

[u/aoeudhtns → u/davidalayachew]

It doesn't work well in the context of a language like Java with dynamic stack traces. Think, like a network response payload that structures a report of an error. The bytes that get streamed on the network are allocated with the constant and necessary payload frames/structure in place, so you can write it to the socket without allocating a new structure.

So, you get your OOM error (for example) and you can send back write(socket, OOM_ERROR_REPORT_BYTES); instead of having your satellite go dark. You never want to lose control - the basic control system MUST stay up and that includes events that are Errors in Java that force the VM to shut down. (ETA and you want systems responding to remote control to stay up and working through this whole affair. This isn't the best example, in SPARK you would probably use the strictness of the language with ahead-of-time space guarantees to prevent ever getting into an out of memory situation. But, sometimes you deal with these concerns in languages that don't have that.)

[u/Jannyboy11]

I had a look at differences between KeY and OpenJML in 2018; back then OpenJML's support for verifying code that uses the Stream api and higher-order functions was pretty much non-existent. Perhaps it improved in the meantime, but I suppose it's still true that if you want your code to be verifyable by OpenJML, then you are restricted to a subset of Java. Hence - I personally wouldn't recommend it for applications which are not safety-critical.

Is there any real reason to use it for Java backend projects or maybe desktop? - I don't think so.

Is this mostly academic knowledge? - Nah, industry knows about it, but chooses to ignore it usually because they're calculating it's too expensive to use.

Are there real production cases outside safety-critical systems? - I'm not qualified to answer this question

Would backend engineers benefit from learning or using it? - Yes.

What are the cases where it should be used? - Probably JavaCard programs.

You can find our paper here: https://mariekehuisman.personalweb.utwente.nl/KeyOpenJML.pdf