Issues

• Missing JLS §5.6.2 binary numeric promotion: mixed byte/short/char/long vs. int fails Core type check

  strata-org/jverify#463 · Filter by author olivier-aws opened on Jul 23, 2026

• Verification status is Verified-by-default, not by positive confirmation (silent false-positive risk)

  bugsoundness
  strata-org/jverify#455 · Filter by author fabiomadge opened on Jun 17, 2026
  1

• @Nat/@Unbounded return-type violation reported at 1:1 instead of the return statement

  strata-org/jverify#450 · Filter by author olivier-aws opened on Jun 15, 2026

• Enable Math.abs / Math.min / Math.max in verified code via built-in contracts

  java-support
  strata-org/jverify#422 · Filter by author fabiomadge opened on Jun 3, 2026

• Non-static methods skipped by translator are silently counted as Verified

  strata-org/jverify#420 · Filter by author fabiomadge opened on May 26, 2026

• Laurel compiler: char primitive type support

  strata-org/jverify#414 · Filter by author fabiomadge opened on May 19, 2026
  

• Laurel compiler: enum type support

  java-support
  strata-org/jverify#412 · Filter by author fabiomadge opened on May 11, 2026

• Test engine: updateTestAnnotation regexes reference non-existent field names

  bugdev speed
  strata-org/jverify#411 · Filter by author fabiomadge opened on May 11, 2026

• Laurel compiler: pure/impure type distinction and @Impure enforcement

  java-supportverification-support
  strata-org/jverify#410 · Filter by author fabiomadge opened on May 11, 2026

• Frontend diagnostics for unsupported Java constructs

  user-experience
  strata-org/jverify#409 · Filter by author fabiomadge opened on May 11, 2026

• Laurel compiler: qualified naming for cross-file procedure references

  java-support
  strata-org/jverify#408 · Filter by author fabiomadge opened on May 11, 2026

• Laurel compiler: @Nullable type support

  java-supportverification-support
  strata-org/jverify#406 · Filter by author fabiomadge opened on May 11, 2026

• Try out the new Strata Ion framework

  strata-org/jverify#404 · Filter by author keyboardDrummer opened on May 1, 2026
  3

  

• Strata: Fix error message and source location accuracy (subset constraints, source ranges)

  strata-org/jverify#403 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026

• Laurel compiler: Array type support

  strata-org/jverify#400 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  1

• Laurel compiler: Switch expression support

  strata-org/jverify#401 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  

• Laurel compiler: Graceful skip of unsupported methods (catch JavaViolationException)

  strata-org/jverify#398 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  

• Laurel compiler: float/double type support

  strata-org/jverify#397 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026

• Laurel compiler: Bitwise, shift, ++, and compound assignment operators

  strata-org/jverify#396 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  1

• Laurel compiler: Generics / type variable support

  strata-org/jverify#395 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026

• Laurel compiler: @Verify, @Contract, @Pure annotation support

  strata-org/jverify#394 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  1

• Laurel compiler: Reference type support (classes, interfaces, new, field access)

  strata-org/jverify#393 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026

• Laurel compiler: Instance method support

  strata-org/jverify#392 · Filter by author keyboardDrummer-bot opened on Apr 23, 2026
  1

• Investigate how much work it is to use the Laurel/Strata back-end to get all the Dafny based tests to pass

  strata-org/jverify#384 · Filter by author keyboardDrummer opened on Apr 10, 2026
  4

  

• Enable bounded verification of JVerify through Strata

  strata-org/jverify#378 · Filter by author keyboardDrummer opened on Feb 3, 2026