Bmc4j – Prove your Java/Kotlin code correct from jUnit style tests

Hi HN!

I just released bmc4j, a tool that lets you write proofs about 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 <= hi);
      int r = Example.clamp(x, lo, hi);
      Bmc.check(r >= lo && r <= hi);
  }

then you can run it like any other test, you will get a result indicating its verified, refuted (and you get the input and replay test, or unknown (reached a timeout etc).

The repo is full of a bunch of examples and docs on how it works, take a look and feel free to ask any questions!