JBMC
Bounded model-checker for Java (bytecode), verifies user-defined assertions, standard assertions, several coverage metric analyses.
Workflow integration:
cli
https://github.com/peterschrammel/cbmc/releases/tag/jbmc-5.8-cav18
BSD-4-Clause-UC (original text)
Maintained