Ursus Verification

Formal verification is the core value proposition of Ursus. Unlike traditional smart contract development, Ursus enables you to mathematically prove that your contracts behave correctly.

Why Verification Matters

Smart contracts are:

• Immutable - Cannot be changed after deployment
• High-value - Often control significant assets
• Publicly accessible - Anyone can interact with them
• Vulnerable - Bugs can be exploited for profit

Traditional approach: Test and hope Ursus approach: Prove and know

What Can Be Verified?

Functional Correctness

Prove that functions do what they're supposed to:

Theorem transfer_moves_tokens:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    balance s' to = balance s to + amount /\
    balance s' from = balance s from - amount.

Safety Properties

Prove that bad things never happen:

Theorem no_overflow:
  forall s s' from to amount,
    exec_transfer from to amount s = Some s' ->
    balance s' to >= balance s to.

Invariants

Prove that important properties always hold:

Theorem total_supply_constant:
  forall s s' from to amount,
    exec_transfer from to amount s = Some s' ->
    total_supply s' = total_supply s.

Security Properties

Prove absence of vulnerabilities:

Theorem no_unauthorized_transfer:
  forall s s' from to amount,
    exec_transfer from to amount s = Some s' ->
    msg_sender = from \/ has_approval s from msg_sender amount.

Verification Workflow

1. Write Contract
   ↓
2. Define Specifications
   ↓
3. Prove Properties
   ↓
4. Extract Verified Code
   ↓
5. Deploy with Confidence

Levels of Verification

Level 1: Type Safety

Automatic - Coq's type system ensures:

• No type errors
• No undefined variables
• Correct function signatures

Example:

(* This won't compile *)
::// balance := "hello" .
(* Error: Type mismatch *)

Level 2: Panic Safety

Semi-automatic - Panic flags track:

• Which functions can fail
• Where errors can occur
• Error propagation

Example:

(* Compiler tracks panic possibility *)
Ursus Definition safe_function: UExpression uint256 false.
(* Cannot call panicking functions *)

Level 3: Functional Correctness

Manual proofs - Prove specific properties:

• Pre/postconditions
• State transitions
• Return values

Example:

Theorem transfer_correct:
  forall from to amount s s',
    balance s from >= amount ->
    exec_transfer from to amount s = Some s' ->
    balance s' to = balance s to + amount.
Proof.
  (* Interactive proof *)
Qed.

Level 4: Full Verification

Complete specification - Prove all properties:

• All functions verified
• All invariants proven
• All security properties established

Verification Techniques

Hoare Logic

Specify pre/postconditions:

{{ balance >= amount }}
  balance := balance - amount
{{ balance_old = balance + amount }}

Invariant Proofs

Prove properties preserved by all operations:

Definition invariant (s: ContractState) : Prop :=
  total_supply s = sum_balances s.

Theorem all_operations_preserve_invariant:
  forall op s s',
    invariant s ->
    exec_operation op s = Some s' ->
    invariant s'.

Induction

Prove properties for all iterations:

Theorem loop_correct:
  forall n,
    exec_loop n = expected_result n.
Proof.
  induction n.
  { (* Base case *) }
  { (* Inductive case *) }
Qed.

Case Analysis

Prove by examining all cases:

Theorem conditional_correct:
  forall b,
    exec_if b = if b then result1 else result2.
Proof.
  destruct b.
  { (* Case: b = true *) }
  { (* Case: b = false *) }
Qed.

Testing vs. Verification

Best practice: Use both!

• Verification for critical properties
• Testing for quick feedback

QuickChick Integration

Ursus integrates with QuickChick for property-based testing:

#[quickchick = on]
Contract MyContract ;

Benefits:

• Automatic test generation
• Property-based testing
• Counterexample finding
• Complement to proofs

Learn more: QuickChick

Verification Tools

Coq Tactics

Standard Coq tactics for proofs:

• intros - Introduce variables
• simpl - Simplify expressions
• rewrite - Rewrite using equations
• induction - Proof by induction
• destruct - Case analysis
• auto - Automated proof search

Ursus-Specific Lemmas

Pre-proven lemmas about Ursus constructs:

• State monad properties
• Operator semantics
• Control flow behavior

Standard Library Verification

Verified implementations of common patterns:

• Arithmetic operations
• Mapping operations
• Optional handling

Learn more: StdLib Verification

Example: Verified ERC20

(* Specification *)
Definition erc20_invariant (s: ContractState) : Prop :=
  s.(totalSupply) = sum_balances s.(balances).

(* Transfer correctness *)
Theorem transfer_preserves_invariant:
  forall from to amount s s',
    erc20_invariant s ->
    exec_transfer from to amount s = Some s' ->
    erc20_invariant s'.
Proof.
  intros.
  unfold erc20_invariant in *.
  unfold exec_transfer in H0.
  (* Proof steps *)
  ...
Qed.

(* No unauthorized transfers *)
Theorem transfer_requires_authorization:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    msg_sender = from \/
    allowance s from msg_sender >= amount.
Proof.
  (* Proof steps *)
  ...
Qed.

Getting Started with Verification

Step 1: Identify Critical Properties

What must be true about your contract?

• Token conservation
• Access control
• State consistency

Step 2: Write Specifications

Express properties formally:

Definition my_property (s: ContractState) : Prop :=
  (* Property definition *)

Step 3: Prove Properties

Use Coq tactics to prove:

Theorem my_theorem:
  forall ...,
    my_property ...
Proof.
  (* Interactive proof *)
Qed.

Step 4: Extract Verified Code

Generate code from proven implementation:

coqc MyContract.v

Next Steps

• Verification Principles - Core concepts
• StdLib Verification - Verified standard library
• QuickChick - Property-based testing
• Advanced Topics - Deep verification

Further Reading

• Software Foundations
• Certified Programming with Dependent Types
• Formal Verification of Smart Contracts