verus-verification
Installation
SKILL.md
Contains Shell Commands
This skill contains shell command directives (!`command`) that may execute system commands. Review carefully before installing.
Regorus Verus Verification
Use this workflow for proof-oriented changes in Regorus, especially Number,
BigInt, arithmetic, conversions, and policy-critical value semantics.
The objective is not merely to make Verus pass. The objective is to establish an exact, useful contract for the real executable implementation with the smallest honest trusted boundary.
Core Rules
- Specify executable semantics exactly.
- Model every meaningful result variant and error path.
- Preserve distinctions such as integer versus float representation.
- For floating-point operations, specify IEEE-754 behavior rather than ideal real arithmetic.
- Do not weaken a contract just because the stronger proof is inconvenient.