Readers enjoying this might also find Java Pathfinder interesting. It was NASA’s tool for model-checking Java apps. It looks like it’s been extended quite a bit since I last checked.

https://lobste.rs/s/0yovvx/java_pathfinder_nasas_model_checker_for