# Proof-scope review worksheet

An araNET writing and review aid. Completing this sheet does not verify software.

## Artifact

- Component and owner:
- Exact source revision / binary digest:
- Build toolchain and operating environment:
- Where the artifact can be inspected:

## Claim

- Property in plain language:
- Formal statement or linked definition:
- Inputs included in the statement:
- Accepted outcome:
- An outcome that must violate it:

## Assumptions and exclusions

- Components treated as contracts rather than proved here:
- Environmental / resource assumptions:
- Behavior explicitly outside the claim:
- Who reviewed the statement and when:

## Evidence and changes

- Proof/check artifacts and tool versions:
- Which checks were actually replayed, by whom, and with what result:
- Changes that require a new statement, proof or review:

## Fictional worked example

Assume a subtotal of USD 100 and tax of USD 8, with no other adjustments.

Weak property: output is nonnegative. Outputs of 0, 100 and 108 all satisfy it.
Stronger amount property: total equals subtotal plus tax, so 108 is required here.
Still unspecified: currency representation, rounding and duplicate-charge behavior.

This is a conceptual arithmetic example, not a formal proof or payment implementation.