Practical guide
Connect a formal claim to the source it describes
A precise specification can describe the wrong program. The connection from intended behavior to production source deserves its own evidence and review.
State a claim that rules out a defect
“The returned retry count is between 1 and 10” is more useful than “the result is valid.” It still allows a function that always returns 1. If valid requested counts must be preserved, state that obligation too. Read the whole requirement before treating one proved property as sufficient evidence.
Illustrative source and claim
// Illustrative lemma; no solver result is asserted.
// reqproof:lemma retry_count_bounded func(n int) bool {
// return ClampRetries(n) >= 1 && ClampRetries(n) <= 10
// }
func ClampRetries(n int) int {
if n < 1 { return 1 }
if n > 10 { return 10 }
return n
}
The example uses comparisons and fixed bounds. Review preservation within the valid range as well as the bounds. Test the public configuration path to establish that it invokes this function with the intended value.
Understand the binding mechanism
Proof supports source-attached lemmas and separate-file binds-to claims. Translation can analyze supported production bodies invoked by a lemma. A separate-file function literal can instead act as a trusted summary whose correspondence to production requires review. Persisted target and lemma hashes detect later changes; they do not establish semantic equivalence.
proof verify-lemma ./internal/retry
proof bindings
proof audit --check lemma_binding_freshness --verbose
Read the proof boundary
Inspect preconditions, assumed callees, supported language constructs and the actual verdict. A proof under positive-input assumptions does not establish rejection of negative inputs. Unknown, translation error and timeout leave the claim undecided. Translation branch coverage reveals visited source structure; it is separate from observed runtime coverage and MC/DC independence.
Review both directions of change
A requirement edit can weaken the theorem without changing source. A code edit can invalidate the old claim. Review both, rerun affected analysis and execute boundary tests on the new revision. Preserve excluded behavior and assumptions needing other evidence. The deliverable is a bounded claim about identified source, rather than an unqualified label that survives every later edit.
Follow the evidence
Review one important pure function together with its requirement, theorem and callers.
Review one claim against its source. Bring the requirement, lemma and implementation so we can assess the assumptions, source correspondence and remaining test obligations.