u/Gc13__

Hi! I just released bmc4j, a tool that lets you write and run proofs (via bounded model checking) on your Java/Kotlin code as ordinary JUnit 5 tests.

For example:

  @BmcProof
  void clamp_result_is_always_within_bounds() {
      int x = Bmc.anyInt(), lo = Bmc.anyInt(), hi = Bmc.anyInt();
      Bmc.assume(lo &lt;= hi);
      int r = Example.clamp(x, lo, hi);
      Bmc.check(r &gt;= lo &amp;&amp; r &lt;= hi);
  }

Its packed with a bunch of features to make bounded model easier to adopt/write (contracts, custom models you can write, assumptions from jarkata validation annotations to list a few!)

Kotlin has a bunch of modelling and examples too.

take a look and feel free to ask any questions!

Bmc4j – Prove your Java/Kotlin code sound and correct with jUnit style tests