Developer Tools
vverify-annotations
Loop invariants and induction measures, written so a verifier can read them.
Released v1.0.0 · 2026-09-28use "stdlib/verify_annotations.ven"Runnable functions that mark a loop invariant or an induction measure in a form the static verifier can find and check. Writing one of these functions is how a program states an invariant.
print loop_invariant(3 >= 0 and 3 <= 5)Reference (2 functions)
API reference
loop_invariant(holds)
Asserts that holds is true, marking the call as a loop invariant.
loop_invariant(3 >= 0 and 3 <= 5)induction_measure(value)
induction_measure(4)