Learning CVL Language (Part 3)

Key Formal Verification Concepts for Smart Contracts

1. Logical Implications and Direction

The direction of logical implications is crucial. Consider a rule restricting actions to owners:

// Incorrect: Only checks if owners can change supply
assert ownerAddress == msg.sender => totalSupplyChanged;

// Correct: Ensures ONLY owners can change supply
assert totalSupplyChanged => ownerAddress == msg.sender;

The correct implication verifies that whenever a restricted action occurs, the actor must have appropriate permissions.

2. Complete Function Coverage

All functions affecting a verified property must be included. For token balances:

// Missing transferFrom() creates a security vulnerability
assert balanceChanged => (
    calledFunction == transfer() ||
    calledFunction == mint() ||
    calledFunction == burn()
);

Missing even one function that can modify balances creates a potential exploit path.

3. Edge Cases and Boundary Conditions

Special cases must be explicitly addressed:

// Handle zero-value transfers
require amount > 0;

// Handle self-transfers
require sender != recipient;

Without these constraints, verification might miss real-world behaviors that violate expected properties.

4. Environment Consistency

Smart contract execution environment must be properly modeled:

// Ensure the caller is actually the account owner
if (functionSelector == transfer) {
    require env.msg.sender == fromAccount;
}

Without proper sender constraints, verification might allow functions to operate on behalf of unauthorized accounts.

5. Handling Complex Data Structures

Dynamic data requires special verification techniques:

// Use optimistic loop flag for string handling
// --optimistic_loop
function name() external view returns (string memory);

This tells the verification tool how to approach unbounded data structures that would otherwise be difficult to fully verify.

6. Specification vs. Implementation

When verification fails, analyze whether the issue is in:

• The property being verified (incorrect specification)

• The code (implementation doesn't satisfy the property)

Counterexamples from failed verification often reveal overlooked edge cases in both specifications and implementations.