Loop invariants: prove the result one iteration at a time

01 / The claim at the loop head

What is a loop invariant, and when is it useful?

An invariant describes a relationship that survives iteration. Variables can change while that relationship stays true: an index advances, for example, while every element before it remains examined and acceptable. Useful subjects include completed prefixes, accumulated results, partitions and conserved resources.

Name the exact observation point. For the ordinary guard-controlled loop used here, let P be the entry assumptions, I the invariant, G the guard and Q the required result:

These are the standard inductive obligations described in the Dafny tutorial. They establish a result conditional on reaching the justified exit. A separate progress argument addresses termination. A break, early return or error path needs its own exit reasoning.

Keep the property and its evidence distinct

02 / Start with the artifact

Free loop proof and evidence worksheet

Copy the record into an issue or repository document. Obtain the required behavior, actual source and an intent authority. Record the manual argument and reviewer, or the verifier's exact translation and results. Leave unperformed work visible.

Blank record

Copy LOOP PROOF AND EVIDENCE RECORD

IDENTITY AND INTENT
Record name and revision:
Requirement/postcondition Q, including normal and error outcomes:
Authoritative intent source and revision:
Person authorized to approve intended behavior:
Approval decision, date and reference, or NOT APPROVED:
Implementation owner; evidence executor; reviewer; acceptance authority:

SOURCE AND CALL PATH
Repository/revision, dirty state, source/build/dependency fingerprints:
Function, file and exact loop location:
Caller -> adapter/harness -> implementation path:
Verifier goal -> actual host/helper/loop path, if applicable:
Relevant helpers, their definitions/contracts and source identities:

DOMAIN, STATE AND FRAME
Allowed input values, types, lengths and representations:
Entry state and caller/environment assumptions P:
Preconditions assumed versus validations actually executed:
Allowed mutation/write set; state that must remain unchanged:
Aliasing/interference assumptions and observable completion point:
Normal result; error/exception/early-return behavior; excluded outcomes:

LOOP ARGUMENT
Loop-head observation point:
Guard G and exact invariant I, including index bounds:
Meaning and domain of each quantified/recursive predicate:
Establishment: initialization and why P establishes I:
Preservation premises: I, G, helper contracts and frame assumptions:
One body execution plus post-step, including evaluation order:
Why the resulting state satisfies I:
Each exit condition and its required result Q:
Why I plus the relevant exit condition is strong enough for Q:

NON-VACUITY AND INDEPENDENT EXPECTATIONS
Reachable entry satisfying P:
Reachable state allowing a real iteration:
Zero-iteration and nonempty exit witnesses:
Independent expected behavior and its authority:
Oracle implementation/identity; required observed values and state:
Positive control and known-failure control:
Weak-goal or vacuity control; expected distinction; actual run status:

TERMINATION, SEPARATE FROM RESULT CORRECTNESS
Variant/measure, domain and well-founded bound:
Strict decrease for every permitted iteration/recursive call:
Break/continue/recursion treatment:
Mathematical argument and reviewer:
Actual checked termination obligations, tool/result, or NOT CHECKED:
Finite observed completion, recorded separately:

MACHINE SEMANTICS AND MODEL CORRESPONDENCE
Language/version/target integer widths, indexing and evaluation rules:
Solver arithmetic/state abstraction, if used:
Bounds needed to relate model operations to executable operations:
Overflow, underflow, nil/empty, aliasing and unmodeled effects:
Correspondence argument and remaining gaps:

METHOD AND REPRODUCTION
Selected method and supported loop/directive shape:
Exact annotations, build tags and enabled/disabled assumptions:
Tool/binary/compiler/runtime/solver versions and identities:
Resource budgets, environment, cache and unknown-result policies:
Prerequisites; working directory; exact commands/argv:
Source, harness, oracle, corpus and emitted VC/query identities:
Portable reproduction steps; output location; exit-code meaning:
Archived run versus new replay identity:

RESULTS AND DISPOSITION
Raw stdout/stderr, query, model, observations and manifest locations:
Intended lemmas found; per-lemma verdicts; obligation counting unit:
PROVED / COUNTEREXAMPLE / TIMEOUT / UNKNOWN / TRANSLATION_ERROR:
Unsupported, skipped, missing or zero-result work:
Finite cases scheduled/executed/accepted, by implementation:
Frame observations and integration results, separately:
Literal failure or model counterexample and interpretation:
Implemented correction and replay on the same claim:
Unfulfilled capture expectations and metadata amendments:
Exclusions, unresolved claims and unperformed checks:
Decision and its exact scope, or NOT ACCEPTED:
Next action -> named accountable owner -> required closing evidence:
Stale-evidence triggers and person responsible for reassessment:

Initial evidence status: NOT RUN / NOT REVIEWED.
Initial acceptance status: NOT ACCEPTED.

The filled record shows how to retain a useful correction while leaving the strong symbolic result open.

03 / A failure and correction you can inspect

Worked example: find the first negative without skipping it

The teaching contract requires FirstNegative(items []int) int to return the first negative element’s index, or len(items) if none is negative. Inputs have length 0–32, including nil and nonnil empty slices, with arbitrary Go int values. Preserve the input’s values, length and nilness. This is fictional teaching intent, without customer or product approval.

The length bound is assumed by the source claim, not checked by a runtime validator. A negative element is ordinary data. The function has one integer return and no error-return API.

The actual defect and implemented correction

The baseline starts at zero for empty input and at one for nonempty input:

Copy i := 0
if len(items) > 0 {
    i = 1
}

That skips the first sign check. On [-1, 2], the required index is 0, but the baseline returns 2. The implemented correction removes the conditional assignment and starts every scan at zero. The strong result goal stays the same.

Inspect the raw observations · Download the source and evidence kit · Checksum

Here is the complete corrected source. The comments are verification annotations; ordinary Go execution does not evaluate them or call PrefixOK from the scan.

Copy package corrected

// FirstNegative returns the first negative index, or len(items).
// Authored teaching contract: len(items) <= 32; input is not mutated.
//
// reqproof:requires 0 <= len(items) && len(items) <= 32
//
//	reqproof:lemma scan_contract func(items []int) bool {
//	  result := FirstNegative(items)
//	  return 0 <= result && result <= len(items) && PrefixOK(result, items) && (result == len(items) || items[result] < 0)
//	}
//
//go:noinline
func FirstNegative(items []int) int {
	i := 0
	// reqproof:invariant 0 <= i && i <= len(items)
	// reqproof:invariant PrefixOK(i, items)
	for i < len(items) && items[i] >= 0 {
		i++
	}
	return i
}

// PrefixOK is a recursive expression of the completed-prefix claim.
// Its call precondition is 0 <= end <= len(items) <= 32.
// The decreases directive is syntactic support, not a solver-proved
// total-correctness guarantee. No element arithmetic is performed.
//
// reqproof:requires 0 <= end && end <= len(items) && len(items) <= 32
// reqproof:decreases end
func PrefixOK(end int, items []int) bool {
	if end <= 0 {
		return true
	}
	return items[end-1] >= 0 && PrefixOK(end-1, items)
}

Expected values and recorded returns

The literal cases were written before execution. The independent Python oracle checks exact integer results and complete input snapshots, including nilness. It does not derive expectations from either scan or the prefix helper.

All 21 selected input-value and nilness comparisons match. The selected lengths are zero through three; length 32 and integer extremes were not executed. See the complete assessment.

The solver results answer different claims

One primary campaign used Go 1.26.3 on darwin/arm64, Z3 4.15.4 and a freshly built current-worktree Proof executable. Each of the three first source-verifier invocations returned exactly one lemma result with a complete query. Commands and environment and build identity identify the execution.

The weak source keeps the baseline’s faulty body, removes the semantic prefix invariant and changes the lemma goal to returned-index bounds only. Read PROVED against that changed claim.

Both strong claims remain unproved. The timeouts do not disprove them, identify a timeout cause or supply a model counterexample. The literal [-1, 2] failure is concrete runtime evidence. No solver retry, cache hit or fallback marker was observed, and the commands did not use --allow-unknown.

Read the complete queries and raw results: baseline query, baseline result, corrected query, corrected result, weak query, weak result.

Why the corrected invariant supports the result

This is a mathematical argument over the stated domain, separate from the unresolved strong solver verdicts. Let n = len(items). For 0 <= end <= n <= 32, PrefixOK(end, items) means every element at an index below end is nonnegative. Its definition reaches the empty prefix at zero; the recursive step adds the check at end - 1.

The baseline fails establishment when items[0] < 0; bounds alone miss this omission.

The empty-prefix case is legitimate, not a substitute for a reachable iteration. [0] permits one iteration; [2, -1, 3] reaches a negative after an accepted prefix; [-1, 2] makes the corrected loop exit immediately on a nonempty input. These path explanations follow from the source and selected returns, not an independently captured iteration trace. A contradictory-precondition control would test a different vacuity risk; none was run here.

Termination, arithmetic and input preservation

For the corrected loop, n - i is nonnegative at the loop head and decreases by one on each permitted iteration. For PrefixOK, end decreases to zero within its stated domain. These are separate mathematical termination arguments. The helper’s reqproof:decreases end receives best-effort syntactic validation in the inspected implementation; the captured queries contain no separate solver-backed termination proof. Termination method · Executed source and query basis

Go uses finite-width integers and checked indexing; its && guard evaluates the index bound before the element access. The inspected Proof path maps Go integer widths to mathematical SMT Int. Here i, end, increments and decrements remain within 0–32 under the authored bounds; element values are only compared with zero. That is a correspondence argument for these operations, not a general overflow certificate. The emitted wrapper asserts len <= 32, while quantified loop obligations range over arbitrary Seq Int states. This is not bounded unrolling. Go semantics · Translation identity · Actual query

The source is read-only on inspection, but the result lemma contains no input-frame or nilness clause. Seq Int also merges nil and empty representations. The 21 matching snapshots remain finite input-preservation observations; caller integration is unperformed.

A capture expectation that was not fulfilled

The primary build attempted compiler count coverage, but the export was empty and reported warning: no applicable files found in input directories. Its zero exit code did not establish coverage. The retained records identify harness calls and returns through runtime.FuncForPC; they are not independent entry counters or a branch-coverage report.

The original observer’s metadata overstated that intended capture. The public observer corrects only that metadata string, with the original source and output preserved. No behavior, JSON key, scan, helper or goal changed, and no primary rerun followed the amendment. A later replay therefore has its own identity. Capture warning · Exact amendment · Patch

Filled record: retain the correction and the open claim

Copy LOOP PROOF AND EVIDENCE RECORD
Name: FirstNegative teaching contract; baseline/corrected/weak comparison.
Authority: fictional teaching requirement in CONTRACT.md. No customer or
product intent approval, named project approver or release acceptance.
Named intent approver, implementation owner, evidence executor and technical
reviewer: not supplied for this fictional teaching record.
For reuse: the receiving engineering lead must assign actual implementation,
execution, review and intent-approval owners before accepting project work.

ARTIFACT BASIS
Public base: https://reqproof.com/assets/loop-invariant/research-rerun/
Relative paths below are exact kit members under that base.
ZIP: https://reqproof.com/assets/loop-invariant/loop-invariant-evidence-kit.zip
ZIP bytes: 37810; regular members: 42.
ZIP SHA-256:
d1b3f3b8c80a2f6ea3bd7cabf69a449d8d4bdaac03cb203ae7055026bf8f6dd1
Member identities: MANIFEST.json and SHA256SUMS.
History and capture amendment: PROVENANCE.json;
OBSERVER-METADATA-AMENDMENT.json.

REQUIREMENT, DOMAIN, OUTCOMES AND FRAME
Q: return the smallest r with items[r] < 0; if no such r, return len(items).
Also preserve all input values, length and nilness.
Domain: caller-supplied Go []int; 0 <= len(items) <= 32;
nil and nonnil empty allowed; arbitrary Go int element values.
Length bound: caller precondition, not an executed validator.
Normal outcomes: first-negative index or length; negatives are ordinary data.
Error outcomes: no error-return API. Resource/panic recovery is not tested.
State: one stable input slice during a local call; concurrent interference
and caller integration are excluded. Allowed mutation: local scan index;
no writes to input elements or slice length/nilness.

SOURCE AND CALL PATH
Module: example.org/loop-invariant-teaching; go.mod declares go 1.26.3.
Functions: baseline.FirstNegative, corrected.FirstNegative, weak.FirstNegative.
Files and SHA-256:
baseline/scan.go
05d5666ad352c9557093af77d20fbad8c6847466eb96ba4bd46a163cd8e06f4b
corrected/scan.go
18ab4f04b9cee28abde011553c567e70807c95428e8644c271f438d040f9f6db
weak/scan.go
b108c27ecfad25d1154e947395dc74f970a9918ddef70662ae5acdea1378d449
Runtime: cmd/observe/main.go -> Variant.Call -> exported FirstNegative.
Recorded function declaration line: 14 in each variant; source identity
comes from runtime.FuncForPC. These are callsite/result records, not counters.
Exact loops: baseline/scan.go:21; corrected/scan.go:18; weak/scan.go:20.
The harness copies each case per variant, preserving nilness, and snapshots
all values plus a separate nil flag before and after the call.
Primary harness: observed/primary-observer-original.go.txt.
Public harness: cmd/observe/main.go; only its method metadata changed.
Primary harness SHA-256:
5b28c72aa0faef855bbb95373caabd28c5832e1f7eca66cb7742c2465f53bbba
Public harness SHA-256:
95f81f290187f3788df6d2abd821ee16a1ef12191f488ea3e8d94594dac79693
Symbolic path: host-calling lemma -> FirstNegative -> FirstNegative_loop_0;
strong queries also define PrefixOK. Runtime scan does not call PrefixOK.

INVARIANT AND ARGUMENT
Loop head: immediately before for i < len(items) && items[i] >= 0.
I1: 0 <= i && i <= len(items).
I2: PrefixOK(i, items).
PrefixOK(end, items), on 0 <= end <= len(items) <= 32:
  if end <= 0, true;
  otherwise items[end-1] >= 0 && PrefixOK(end-1, items).
Meaning: every element at 0 <= k < end is nonnegative.
Corrected initialization: i := 0; entry has bounds and an empty prefix.
Preservation premises: I1, I2, true guard and unchanged input.
Body/post-step: i++; no separate for-post clause.
Then i' = i + 1 <= len(items), and the newly included item is nonnegative.
Exit: ordinary guard false, no break or early return in this loop.
I1 plus the false guard gives either i = len(items), or i < len(items)
with items[i] < 0.
I2 excludes an earlier negative, so i meets the required index condition.
Frame/nilness evidence is recorded separately below.
Status: mathematical argument; strong source-verifier result unresolved.

INDEPENDENT EXPECTATIONS AND NON-VACUITY
cases.json contains prewritten literal expected indices:
  nil -> 0; nonnil [] -> 0; [-1,2] -> 0; [2,-1,3] -> 1;
  [2,0,-1] -> 2; [0] -> 1; [1,0,3] -> 3.
cases.json SHA-256:
0830d152a0f700e8256bc3e1aaa49653c17b6b8651a225379ed42d5405fd1ef0
oracle.py SHA-256:
8981c4a6ee342a2941fcc2064484768a3e46fab94658047c3de280c5899096e0
Oracle: exact integer type/value plus complete input snapshots/nilness;
expectations do not come from PrefixOK or any scan implementation.
Corrected-loop witnesses by source reasoning and selected return observations:
  [0] permits an iteration; [2,-1,3] exits after a nonempty accepted prefix;
  [-1,2] makes corrected exit without iteration; empty input also exits.
No independently instrumented iteration trace is claimed.
Positive contrasts: [2,-1,3] -> 1 and [1,0,3] -> 3 match the literal
oracle for all three variants.
Weak control: actual faulty body with I2 removed AND goal narrowed to bounds.
It is meaningful but insufficient, not a logically vacuous theorem.
Contradictory-premise/host-independent vacuity controls: proposed, NOT RUN.

FAILURE AND IMPLEMENTED CORRECTION
Baseline sets i = 1 when len(items) > 0, otherwise keeps i = 0.
On literal [-1,2]: required 0; baseline 2; weak 2; corrected 0.
Correction: remove conditional skip-first assignment; initialize at 0.
Baseline and corrected retain the same scan_contract goal:
  result := FirstNegative(items)
  0 <= result && result <= len(items) && PrefixOK(result, items) &&
  (result == len(items) || items[result] < 0)
Weak scan_bounds goal: 0 <= result && result <= len(items).
No solver counterexample was obtained. [-1,2] is a literal runtime witness.

TERMINATION AND ARITHMETIC
Loop measure: len(items)-i, nonnegative at the head and decreased by 1.
PrefixOK measure: end; recursive calls reduce it by 1 until zero.
Status: separate mathematical arguments, not solver-checked termination.
Actual reqproof:decreases end is on PrefixOK only; current validation is
best-effort syntactic. No separate termination VC appears in the queries.
Finite completion: all 21 recorded calls returned.
Go: finite-width int, checked indexing, left-to-right short-circuit &&.
Model: mathematical Int and Seq Int.
Correspondence: under the authored bounds, scan/helper index arithmetic
stays within 0..32; end-1 is used only when end > 0; elements are only
sign-compared. This reasoning is not a general overflow certificate.
Wrapper length <= 32 is asserted; quantified loop obligations still range
over arbitrary Seq Int states. No bounded-unrolling or timeout-cause claim.
The result goal has no frame/nilness clause; Seq Int cannot distinguish
nil from empty. Read-only inspection and finite snapshots are separate.

TOOL AND RUN IDENTITY
Primary campaign UTC:
2026-10-28T21:36:13.534132+00:00 to 2026-10-28T21:37:13.350790+00:00.
Go: go1.26.3 darwin/arm64. Z3: 4.15.4, 64 bit.
Proof: freshly built current-worktree executable, not the old installed one.
Proof binary SHA-256:
89c2dfbe34ab2d228b9847a3eca326644d2acce02e614b8dbab630baf83759d2
Revision: b566a01085f0233c0be2c71508a2d3caac0cf47a; trackedDirty=true.
No tracked Go/go.mod/go.sum source difference reported.
Selected-source/dependency fingerprints and buildinfo:
observed/build-identity-summary.json; observed/proof-buildinfo.stdout.txt.
No stable Proof release version is substituted for this build identity.
Fixture has no build constraints; FirstNegative uses //go:noinline.
No extra --tags supplied; current CLI includes reqproof_proof by default.
Annotations: reqproof:requires, host-calling reqproof:lemma,
the two reqproof:invariant directives, helper reqproof:decreases end.
Source-verifier settings: z3; 15s per lemma; no downloads; no cache;
JSON plus complete query; no --allow-unknown; no solver retry.
Selected environment: GOPROXY=off, GOSUMDB=off, REQPROOF_NO_DOWNLOAD=1.
Captured memory watchdog ceiling: 16000000000 bytes. No timeout cause known.

SOURCE COMMANDS
Run from the fixture/extracted module root. Here "proof" denotes the
identified executable; the exact original absolute argv[0], cwd and all
arguments are retained in observed/commands.json.
proof verify-lemma --solver z3 --no-download --no-cache --format json --show-query --timeout 15s ./baseline
proof verify-lemma --solver z3 --no-download --no-cache --format json --show-query --timeout 15s ./corrected
proof verify-lemma --solver z3 --no-download --no-cache --format json --show-query --timeout 15s ./weak

RAW RESULTS AND VERIFICATION CONDITIONS
Each invocation: exactly one nonempty lemma result, not three separately
reported establishment/preservation/exit verdicts.
baseline scan_contract: TIMEOUT, 15012 ms, CLI exit 1.
corrected scan_contract: TIMEOUT, 15021 ms, CLI exit 1.
weak scan_bounds: PROVED, 11 ms, CLI exit 0; returned bounds only.
Queries: observed/baseline.smt2; observed/corrected.smt2; observed/weak.smt2.
Corrected query SHA-256:
616c4767d031d0d554d22466925535a8dadaff5f6e21d831f2dee5c34d51c5e9
All query/result hashes: MANIFEST.json and SHA256SUMS.
Raw source results, including queries, and diagnostics:
observed/verify-baseline.stdout.txt; observed/verify-baseline.stderr.txt;
observed/verify-corrected.stdout.txt; observed/verify-corrected.stderr.txt;
observed/verify-weak.stdout.txt; observed/verify-weak.stderr.txt.
No source counterexample, UNKNOWN, translation error, cache hit or observed
fallback marker in this campaign. Other runs must preserve their actual
unsupported/unknown/timeout/skipped/missing status rather than claim proof.
Primary finite observations: observed/observe.stdout.txt.
Literal assessment: observed/oracle-assessment.json.
Seven selected representations, six distinct element sequences, three
variants, 21 callsite/results; baseline 6/7, corrected 7/7, weak 6/7 accepted.
All 21 selected input-value/length/nilness comparisons match.
Caller/environment integration: NOT PERFORMED.

CAPTURE LIMIT AND AMENDMENT
Compiler count coverage attempted; directory/export empty.
observed/coverage.txt is empty; observed/coverage-export.stderr.txt says:
warning: no applicable files found in input directories
Original metadata overstated coverage; no independent entry/branch count.
Public observer changes only the method string; exact amendment and patch:
OBSERVER-METADATA-AMENDMENT.json; observed/observer-metadata-only.patch.
No primary rerun after this metadata correction; archived bytes unchanged.

PORTABLE FINITE REPRODUCTION
Prerequisites: normal CPython 3.12+ and already installed Go 1.26.3+.
No pip, Proof, Z3 or network required for this finite path.
Extract the ZIP, open its root, read README.md, choose a nonexistent output:
python3 -B reproduce.py --output /tmp/loop-invariant-new-run
The script refuses an existing output directory. It builds the supplied
Go variants, records new calls and applies the literal Python oracle.
Inspect new commands.json, observe.stdout.txt, oracle-assessment.json and
replay-report.json in that output directory. It has a separate run identity.
Wrapper exit 0 means the expected finite 6/7, 7/7, 6/7 contrasts reproduced;
it neither accepts faulty sources nor establishes a universal proof.

OPTIONAL, SEPARATE REPLAY PATHS
Installed Z3, exact retained query bytes; also runs the finite path:
python3 -B reproduce.py --output /tmp/loop-invariant-query-replay --replay-smt --z3 /path/to/z3
This is a new query replay, not a new Go translation; keep actual outcomes.
Queries include get-model: UNSAT followed by model-unavailable is not a
counterexample. UNKNOWN/TIMEOUT/errors still do not establish proof.
Existing caller-supplied Proof binary and configured Z3, plus finite path:
python3 -B reproduce.py --output /tmp/loop-invariant-source-replay --proof /path/to/proof
The new binary hash, nonempty results and actual verdicts are recorded.
The primary Proof binary/repository is not bundled. Wrapper success does
not require PROVED results; inspect the per-lemma outcomes yourself.

DECISION, OWNERS AND NEXT WORK
Disposition: observed functional correction on selected cases; both strong
symbolic claims unresolved. No production acceptance or certification.
Unperformed: length-32/extreme-value tests, vacuity-control execution,
solver-checked termination, source-proved frame/nilness, caller integration,
second-solver comparison and any proof retry.
Next actions for a real project, NOT assigned or executed by this record:
  Intent owner: approve exact result/domain/frame and excluded outcomes.
  Verification engineer: investigate the strong claim/query without silently
  weakening it; retain any new result under a new source/tool identity.
  Implementation owner: add required boundary and caller checks.
  Reviewer: assess correspondence and remaining evidence before acceptance.
Names, approvals and deadlines: receiving project must supply them.
Stale triggers: changed requirement, bound, guard, initialization, body,
helper, frame/aliasing assumptions, source/build/dependency, annotations,
translator/solver/settings, harness, oracle or caller environment.
The assigned evidence owner must assess affected claims and renew evidence.

04 / The working method

How to build a loop correctness argument

1. Approve the result and domain. Specify outputs, error outcomes, relevant state and allowed mutation. Resolve whether an input bound is a caller obligation or an executed check. Name the person who can approve that decision.
2. Identify the real loop. Freeze the source, helpers, build and call path. Enumerate every exit and every update, including a for post-step, guard side effects and calls that can alter state.
3. Work backward from the postcondition. Ask what must already be true when the loop stops. Express that relationship at a changing index or progress boundary, then add the bounds needed to make its expressions valid.
4. Discharge the three reasoning obligations. Substitute the actual initialization; reason through one permitted iteration; justify each exit separately. Record any missing premise instead of assuming the desired conclusion.
5. Check reachability, progress and correspondence. Supply witnesses that satisfy the preconditions and enter the body. Justify termination independently. Check machine arithmetic, indexing, frames and abstractions against the implementation.
6. Collect evidence with the chosen method. For a verifier, inspect the host-dependent query and nonempty results. For runtime checks, use independent expectations and retain concrete inputs and state. Run the caller checks the local model leaves open.
7. Repair and renew the same claim. Preserve the failure, implementation change and subsequent observations. If intended behavior changes, record its authorization. Give unresolved work an owner and decide what evidence must be renewed after future changes.

05 / Verification gates

Loop invariant review checklist

• The postcondition, domain, frame and intent authority are explicit.
• The invariant has one precise loop-head scope and well-defined expressions.
• Actual initialization establishes it, including zero-iteration entry.
• One permitted body execution and post-step preserve it.
• Every exit establishes its required result; guard-false reasoning is used only where applicable.
• Reachable witnesses and an independently expected failure challenge vacuity and weak claims.
• Termination and machine/model correspondence have their own evidence status.
• The source, harness and any symbolic goal reach the intended implementation.
• Required lemmas are present; verdicts, diagnostics, queries and counting units are inspectable.
• Missing, unsupported, skipped, unknown, timed-out and unperformed work remains visible.
• The reviewer can reproduce the observations and identify their source basis.
• Acceptance, next actions and evidence-refresh ownership are recorded.

06 / Mistakes and repairs

Where loop reasoning goes wrong

07 / Proof workflow and limits

Use Proof on the claim its source path actually checks

For this fixture, the inspected path collects the invariant comments, translates the while-form for into a recursive helper and includes establishment and preservation obligations with the host-calling lemma. Its use projection is guarded by those obligations. The emitted queries provide the inspectable connection between scan_contract, FirstNegative and FirstNegative_loop_0. Source identities · Corrected query

Start with the exact annotations and commands in the filled record. Check support for your actual shape against the current translator and diagnostics. The inspected help contains older blanket limits that conflict with current shape-specific implementation paths. Adding a comment does not establish analyzability, and this example does not establish support for every loop construct or combination.

The inspected cmd/proof/verifylemma.go policy can return success for zero lemmas; --allow-unknown can also accept UNKNOWN or TIMEOUT at the command-policy level. Neither is a proof. Require the intended lemma, source linkage, assumptions, query and per-lemma verdict. TRANSLATION_ERROR or unsupported syntax leaves the affected claim unchecked. The retained results use neither an empty lemma set nor --allow-unknown.

The exact catalog obligation invariant_preservation has Go-only eligibility for genuine universally quantified data or state consistency properties. Ordinary CRUD, persistence and route-dispatch scenarios do not qualify merely because their requirements use the word “always.” This is a catalog restriction, not a restriction on the general reasoning method or a claim that every Proof lemma target is Go-only. Other language paths need their own support assessment. The catalog and CLI sources are identified in the build record.

If the uncertainty is a written decision rule, Spec Lab can help review its predicate and proposed cases. It does not execute repository tests or prove this loop. Keep source verification and runtime execution in their recorded environments.

08 / Choose a workflow

Which method should you use for this loop?

The recorded campaign used Go and Proof with Z3; no Dafny program or second solver was executed.

10 / Two more examples

Two edge cases that need different reasoning

Both examples below are unexecuted mathematical illustrations. They add no Proof support claim or recorded result.

A break needs its own exit condition

Suppose a loop with guard i < n stops early when a sentinel is found. At that break, the guard may still be true. “The loop ended, therefore i = n” is invalid. Retain the sentinel condition and facts preserved up to the break, then prove the required result for that exit separately. If the body changes state before breaking, even the loop-head invariant may need re-establishing. Dafny reference section 8.14 explains this distinction.

An in-place transformation needs an entry snapshot

Suppose a loop must zero an array prefix of length m, where 0 <= m <= n, while preserving the suffix. Start at i = 0 and iterate while i < m, writing A[i] = 0 before incrementing. Let A0 denote the entry contents. A useful head invariant is 0 <= i <= m, all A[k] = 0 for 0 <= k < i, and all A[k] = A0[k] for i <= k < n.

Writing zero at i and incrementing extends the completed prefix while preserving the remaining suffix. At guard-false exit, i = m, giving the required transformation and unchanged suffix. The permitted write set is the target prefix; an “entire input unchanged” claim would contradict the task. State that no other writer changes the array during the argument. This is an application of framing, not an executed mutation example.

12 / Continue with the evidence

Related guides

• k-induction: compare this loop argument with base-and-step reasoning over system behavior.
• Formal specification to source: inspect whether a formal claim actually depends on the implementation you intend to assess.
• Property-based testing: extend finite input exploration while keeping the property, oracle and replayable failure explicit.
• Differential testing: compare implementations without treating agreement as an independent correctness oracle.
• Software verification plan: assign the additional obligations that remain after a local loop check.