Description

Umbrella issue tracking formal verification of Vyper safety properties.

Goals

Prove that Vyper programs, when executed according to our semantics, satisfy key safety properties that prevent common smart contract vulnerabilities.

Safety Properties

Memory Safety

• Prove: Array bounds safety #83 - Array bounds safety (no OOB access)
• Prove: String/bytes length bounds #89 - String/bytes length bounds
• Prove: Storage variables never alias #92 - Storage variables never alias

Arithmetic Safety

• Prove: Arithmetic safety (no silent overflow) #84 - Arithmetic safety (no silent overflow)
• Prove: Division by zero protection #86 - Division by zero protection

Control Flow Safety

• Prove: For-loops are bounded (guaranteed termination) #87 - For-loops bounded (guaranteed termination)
• Prove: @nonreentrant functions cannot be reentered #85 - @nonreentrant prevents reentry (depends on Non-reentrancy checking #40)

Type Safety

• Prove: Type preservation (type safety) #88 - Type preservation

Approach

Each property follows a similar pattern:

1. Define the property - What invariant should hold?
2. Identify the mechanism - How does the semantics enforce it?
3. Prove base cases - Default values, initial states
4. Prove preservation - Each operation maintains the invariant
5. Compose - Full program satisfies the property

Priority

Properties are roughly ordered by:

1. Security impact (reentrancy, overflow)
2. Proof difficulty (some are straightforward case analysis)
3. Dependencies (type safety may depend on type-checking implementation)

Non-Goals (for now)

• Gas consumption bounds (requires EVM integration)
• Cross-contract call correctness (external calls still WIP)
• Optimizer correctness (separate work in Venom passes)