For loops already worked but might not have been documented correctly. I just shipped the functionality for `while` loops now, auto-infer works for common cases of invariants:

  let mut i = 0;
  while i < 5 {
    arr[i] = val;
    i += 1;
  }

So in that case, the compiler detects `i < N` with monotonic increment and synthesizes `i >= 0 && i < N` automatically.

(Works with `<`, `<=`, `i += 1`, and `i = i + 1` via the same mechanism as for-loop induction variables.)

Complex loops (`while i + j < n`, `while p.addr() != 0`) require syntax that I have slopped together an explicit `invariant` keyword that I am not 100% happy with, but will refine later. Z3 checks base case + inductive step via Hoare logic and reports counterexamples on failure.

---

RE: "gnarliest invariant"

`ensures(result != 0)` on the SYN cookie in the kernel contract for the OS project in the monorepo.