Guide

Verify a function

1. Choose an Example to load it immediately.
2. Edit playground.py.
3. Set Function selector to a function name, or * for all annotated functions.
4. Click Verify. Cancel stops the current run.

Editing the source or selector clears the results. Loading an example replaces the source and undo history; reloading the page restores the initial example. The editor is read-only during verification.

Use EN / JP to switch languages. Opening Guide or Reference and switching languages preserve your work. Drag the panel dividers to resize the workspace; focused dividers also accept arrow keys. The browser accepts one module up to 1 MiB and verifies it without executing Python.

Use #/playground, #/guide or #/reference for page links. A section link uses #/reference/value-contracts. Existing .html links also work. Sample selection updates the URL; #/playground/division loads signed division directly.

Write a contract

Use Annotated and Refine to constrain a value. The first lambda parameter receives that value; additional return-predicate parameters name function inputs.

from refinepy import Refine
from typing import Annotated

Nat = Annotated[int, Refine(lambda v: v >= 0)]

def increment(x: Nat) -> Annotated[int, Refine(lambda result, x: result == x + 1)]:
    return x + 1

This requires a nonnegative input and a result one greater than that input. Change x + 1 to x - 1 to try a failing contract.

Add a function precondition

Use @requires for a condition on function inputs.

from refinepy import requires

@requires(
    lambda xs, i: 0 <= i < len(xs)
)
def read_at(xs: list[int], i: int) -> int:
    return xs[i]

The verifier checks this condition at every call.

Write a return contract with ensures

Use @ensures with a base return type. Its first binder receives the result; remaining binders name entry inputs. A None result omits the result binder.

from refinepy import ensures

@ensures(lambda result, n: result == n + 1)
def increment(n: int) -> int:
    return n + 1

@ensures(lambda n: n + 0 == n)
def identity_lemma(n: int) -> None:
    return None

Verify string contents

Prove that an index is in bounds before reading a character. Strings support content equality, length, concatenation and step-1 slicing.

from typing import Annotated
from refinepy import Refine, requires

@requires(lambda text: len(text) > 0)
def first(text: str) -> Annotated[str, Refine(lambda result: len(result) == 1)]:
    return text[0]

def append(left: str, right: str) -> Annotated[str, Refine(lambda result, left, right: len(result) == len(left) + len(right))]:
    return left + right

Negative indices count from the end. String methods and f-strings are unsupported.

Divide by an integer input

Establish a nonzero divisor with a precondition or branch. Division and remainder follow Python’s floor-rounding and sign rules.

from refinepy import requires, ensures

@requires(lambda d: d != 0)
@ensures(lambda r, a, d: a == r[0] * d + r[1] and
    (0 <= r[1] < d if d > 0 else d < r[1] <= 0))
def divide(a: int, d: int) -> tuple[int, int]:
    return a // d, a % d

An unguarded divisor that can be zero fails verification. Nonlinear arithmetic and variable-divisor proofs may return unknown.

Build and update a local list

Build a fresh list under one local name to update it while preserving input contents.

from refinepy import requires, ensures

@requires(lambda xs, i: -len(xs) <= i < len(xs))
@ensures(lambda r, xs, i, value:
    len(r) == len(xs) and r[i] == value
    and r == xs[:i if i >= 0 else len(xs) + i] + [value]
        + xs[(i if i >= 0 else len(xs) + i) + 1:])
def replace(xs: list[int], i: int, value: int) -> list[int]:
    out = xs[:]
    out[i] = value
    return out

append, extend, += and integer item assignment are supported. Empty lists need a type such as out: list[int] = []. Element and whole-list contracts are checked after writes. Input lists, shared aliases and extracted nested lists cannot be written. See Reference for helper-result ownership and container limits.

Check recursive termination

Use @decreases to prove that a direct recursive call reduces a measure.

import refinepy
from refinepy import Refine
from typing import Annotated

Nat = Annotated[int, Refine(lambda v: v >= 0)]

@refinepy.decreases(lambda n: n)
def count(n: Nat) -> Annotated[int, Refine(lambda r, n: r == n)]:
    return 0 if n == 0 else 1 + count(n - 1)

Each recursive step must satisfy 0 <= next < entry. A tuple of integers can express lexicographic descent. All called functions must terminate too.

Check loop termination

Place invariant and decreases marker calls immediately before the loop. The invariant must hold initially and after each iteration; the measure must remain nonnegative and strictly decrease on every back edge.

from typing import Annotated
from refinepy import Refine, invariant, decreases

Nat = Annotated[int, Refine(lambda v: v >= 0)]

def count_to(n: Nat) -> Annotated[int, Refine(lambda r, n: r == n)]:
    i = 0
    invariant(lambda i, n: 0 <= i <= n)
    decreases(lambda i, n: n - i)
    while i < n:
        i += 1
        if i % 2 == 0:
            continue
    return i

Every nested loop needs its own measure. Without termination evidence, verification applies only when the function returns normally.

Prove an equation about a function

Use @reflect to make a checked definition available in predicates. A lemma states the equation as its return contract.

from __future__ import annotations
import refinepy
from refinepy import Refine
from typing import Annotated

@refinepy.reflect
def inc(x: int) -> int:
    return x + 1

def lemma(x: int) -> Annotated[None, Refine(lambda _, x: inc(inc(x)) == x + 2)]:
    return None

Select lemma and verify; changing x + 2 to x + 3 fails the proof. Reflected functions cannot have preconditions, refined annotations, loops or container writes. Recursive definitions and inductive lemmas have additional Reference restrictions.

Use a lemma without executing it

Add this to the preceding example. Assert checks a proposition at a bound local variable; using supplies a checked, independently terminating lemma. Python does not execute these local annotations.

from typing import Annotated
from refinepy import Assert

def use_lemma(x: int) -> int:
    x: Annotated[int, Assert(
        lambda value: inc(inc(value)) == value + 2,
        using=lambda arg: lemma(arg),
    )]
    return x

Without using, the proposition must follow from current facts. Later assignments are not constrained by Assert; use Refine for a lasting value contract. See Reference for binding rules.

Read the results

Each function has a status and a separate termination summary. Verification details shows diagnostics and proof evidence; Full JSON report shows the complete report.

verified applies to inputs satisfying the contracts and the modeled runtime. It does not establish termination by itself or enforce contracts in Python. Recursion-depth and resource limits remain outside the guarantee. See Reference for supported syntax.