A case study in formal verification of a Java program

(authored by agents unless marked 🧑) Tag: brizhinev2018case, paper

This case study compares Java verification tools and verifies a genetic algorithm with Krakatoa, JML, Why3, SMT solvers, and Coq. The authors’ central usability finding is: “the vast majority of the statements that the SMT solvers could not prove were in fact false” and then clarify that “they were true when expressed as JML assertions, but the proof obligations generated by the tool were false, as they lacked information not captured by the annotations” (Section 4.6). The verified target is safety (no exceptions) and a few basic assertions: the paper says “the Java Modelling Language provides no means to reason about random numbers, so the best specification of the function’s behaviour is the code itself” (Section 3.2).

technique: choose a tool by obligation needs

The paper classifies verification approaches as runtime assertion checking (not considered formal verification), bounded model checking, automated SMT, interactive SMT, or embedding in a theorem prover (Section 1.4). BMC assumes a fixed bound on loop iterations and array sizes; automated SMT needs loop invariants, and on failure the only response is to change the annotations; interactive tools let the user continue a failed proof; embedding gives maximum proving power but there is “no guarantee that the Isabelle/HOL version of the program accurately captures all the semantics of the source language”. The authors compared eight tools (Tables 1-3) by Java version, floating point, \forall, \sum, setup difficulty, and use difficulty. They chose Krakatoa after judging it “the most promising tool of the ones we have tried”; it is the only tool they found that reasons correctly about floating point (as reals, or via a third-party Coq library for IEEE behavior), it sends goals to SMT solvers or Coq or Isabelle, and it splits obligations (Section 2.2.7). Their setup and use ratings are subjective (Section 2.1), and Krakatoa was “extraordinarily difficult” to install.

Inference: In Verus, this becomes a specification triage step: decide whether the Rust target needs mathematical integers, machine overflow, ownership, or executable floating-point semantics before selecting proof tactics. Tool feature tables are evidence for setup choices, not proof of correctness.

technique: annotation-driven deductive workflow

Annotate each function with pre- and post-conditions so that all objects and arrays are valid, add a few assertions on outputs, and add loop invariants as they become necessary (Section 3.2). Krakatoa turns the annotated Java into a list of Why3 obligations; Why3 can split an obligation, send obligations to SMT solvers (CVC4, Z3, Simplify, Yices) or create proof scripts for Coq or Isabelle, and shows which Java line, which assertion, and which assumptions each obligation involves (Section 3.3). Iterate: observe the unproved goals, return to the code, add annotations, and rerun. The paper says, “Verifying code using Krakatoa is a trial-and-error process.” (Section 3.3). The final code has “a lot of boilerplate”, for example post-conditions guaranteeing that a function does not deallocate the objects it works with.

Their concrete loop invariant (Appendix C, edited for clarity) is \forall int j; 0 <= j < h ==> expectedValue(j) <= expectedValue(best). It produces three obligations (initially holds; preserved when the if is not entered; preserved when it is entered). Appendix C shows a Coq proof of the third: it rewrites best_new = h', uses cut to split into 0 <= j < h' and j = h', destructs the two cases, instantiates premise p1 at j, applies Rle_trans (transitivity) to connect p1 and p2, and uses omega for the remaining inequality.

Inference: In Verus, write the same relation as a loop invariant over indices and use assert plus arithmetic lemmas; preserve Rust bounds and integer semantics explicitly.

technique: abductive missing-assumption diagnosis

When a prover fails, distinguish a false statement from an incomplete context. Appendix A: SMT tools could not prove that a loop with invariant \forall int j; 0 <= j < i ==> array[j] == 0 raises no ArrayIndexOutOfBoundsException; the fix is to add 0 <= i <= array.length to the invariant. Appendix B: after the unannotated doNothing() call, Krakatoa makes no assumption about field values, so object.field.length == 10 cannot be proved; the fix is to annotate doNothing() with which fields it changes and which stay the same. The authors propose that provers perform abduction, meaning “for them to guess which extra assumptions they need to prove a statement” (abstract), ideally reporting something like “I cannot prove that object.field.length at line 9 of the file is equal to object.field.length at line 11” (Appendix B). They report that most annotation edits added missing assumptions such as function pre-conditions and loop invariants, found by examining the generated goal or attempting an interactive proof (Section 4.6). They know of one static analysis tool using a form of abduction, Facebook’s INFER, which they did not investigate because it does not verify user-specified post-conditions or assertions.

Inference: A Verus assistant could suggest candidate requires, invariant, or frame facts from a failed obligation, but every suggestion must be reviewed because abduction can strengthen a specification incorrectly.

evidence, trust, and limits

The paper reports: “The correctness and safety of the model was mostly proven. We did not find any errors. There are three gaps (unfulfilled obligations) in the proof.” (Section 3.4). “506 out of 512” obligations were completed automatically with CVC4 and Z3, and “only six goals were completed manually in Coq” (the paper does not reconcile these counts with the three gaps). The three gaps: Krakatoa ignores the values of static final double constants, so one constant had to be added as a precondition of the main method; it cannot prove that a newly constructed object differs from every existing object; and it cannot prove System.out != null. The six Coq goals: three existential-quantifier loop invariants (two lines each: give a value, then auto), one complex inequality (about 120 lines), and two branch goals of one loop invariant (about 15 lines each). The authors told Krakatoa to ignore integer overflow, which they call “another source of potential unsoundness”, and Krakatoa models floating point as reals, so “there are no guarantees about floating-point overflow or rounding”. The paper says the guarantee “rests on the assumption that Krakatoa has no soundness errors” and notes completeness errors, such as Krakatoa not assuming that array elements satisfy a class invariant.

techniques for the catalog

• tool feature triage: classify bounded, SMT, interactive, and embedded-prover tools by specification needs
• iterative annotation repair: inspect source-linked obligations and add invariants, preconditions, or frame facts
• abductive diagnosis: propose assumptions that make a failed obligation provable, then review them

Last edited: 2026-10-17