Binary package “jbmc” in ubuntu noble

bounded model checker for Java programs

 JBMC generates traces that demonstrate how an assertion can be violated, or
 proves that the assertion cannot be violated within a given number of loop
 iterations.