Migration Guide: Dafny, Verus, and SPARK to Assura

This guide helps users of existing formal verification tools translate their contracts and workflows to Assura. Each section covers syntax mapping, key differences, common pitfalls, and a complete worked example.

Dafny to Assura

Syntax Mapping

Key Differences

1. Separation of concerns: Dafny verifies implementation inline (the method body IS the implementation). Assura separates the contract (what) from the implementation (how). You write .assura files for contracts; AI or developers write Rust for implementations.

2. Target language: Dafny compiles to C#, Go, Java, JavaScript, or Python. Assura generates Rust source code.

3. Effect tracking: Dafny uses reads/modifies clauses. Assura uses a hierarchical effect system (io, database, net, etc.) that tracks fine-grained side effects.

4. Linear types: Dafny has no linear type system. Assura supports usage grades (:_1, :_n, :_omega) for resource management.

Common Pitfalls

• No method bodies: Assura contracts do not contain implementation code. If you have method Foo() { ... } in Dafny, split it into a contract (.assura) and a Rust implementation.
• Return values: Dafny uses named returns (returns (r: int)). Assura uses output(result: Type) and the keyword result in ensures clauses.
• Quantifier syntax: Dafny uses forall x :: P(x). Assura requires a binding domain: forall x in range : P(x).

Worked Example

Dafny:

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index < a.Length ==> a[index] == key
  ensures index == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> a[i] > key
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key { lo := mid + 1; }
    else if a[mid] > key { hi := mid; }
    else { return mid; }
  }
  return -1;
}

Assura:

contract BinarySearch {
    input(a: List<Int>, key: Int)
    output(result: Int)

    requires { forall i in a : forall j in a : i < j ==> a[i] <= a[j] }

    ensures { result >= 0 ==> a[result] == key }
    ensures { result == 0 - 1 ==> forall i in a : a[i] != key }

    effects { pure }
}

Verus to Assura

Syntax Mapping

Key Differences

1. Integration model: Verus annotates Rust source code directly with proof, exec, and spec keywords. Assura uses separate .assura files that reference Rust code via bind declarations.

2. Same language: Verus specs are written in Rust syntax. Assura has its own contract language with domain-specific features (typestate, effects, information flow).

3. Ownership model: Verus leverages Rust’s ownership and borrowing directly. Assura has its own linear type system that maps to Rust ownership in codegen.

4. SMT interaction: Verus uses a custom SMT encoding with triggers and quantifier patterns. Assura uses Z3 with configurable verification layers (Layer 0: structural, Layer 1: basic SMT, Layer 2: full).

Common Pitfalls

• No inline verification: Verus proves properties inline in Rust. Assura contracts are external specs. You cannot write proof { ... } blocks in Assura; use ghost { ... } clauses instead.
• Type mapping: Verus uses Rust types (u64, Vec<T>). Assura uses abstract types (Nat, List<T>) that map to Rust types in codegen.
• Tracked vs ghost: Verus tracked variables participate in ownership. Assura ghost variables are fully erased at runtime.

Worked Example

Verus:

#![allow(unused)]
fn main() {
use vstd::prelude::*;

verus! {
    spec fn triangle(n: nat) -> nat
        decreases n
    {
        if n == 0 { 0 }
        else { n + triangle((n - 1) as nat) }
    }

    proof fn triangle_is_monotonic(i: nat, j: nat)
        requires i <= j
        ensures triangle(i) <= triangle(j)
        decreases j - i
    {
        if i < j {
            triangle_is_monotonic(i, (j - 1) as nat);
        }
    }
}
}

Assura:

contract triangle {
    input(n: Nat)
    output(result: Nat)

    ensures { result >= 0 }
    decreases { n }

    effects { pure }
}

contract triangle_is_monotonic {
    input(i: Nat, j: Nat)
    output(result: Unit)

    requires { i <= j }
    ensures { true }

    decreases { j - i }

    effects { pure }
}

SPARK Ada to Assura

Syntax Mapping

Key Differences

1. Language family: SPARK annotates Ada code with contracts. Assura generates Rust code. The underlying language families are very different (Ada is a systems language with tasking; Rust has ownership and borrowing).

2. Information flow: SPARK has Global and Depends for data flow tracking. Assura has both effects (for side effects) and data_flow (for information flow / taint tracking). Assura’s system is more granular.

3. Concurrency: SPARK uses Ada tasking with Ravenscar profile. Assura uses effect-based concurrency tracking.

4. Tooling: SPARK uses GNATprove (based on Why3/Alt-Ergo/CVC5). Assura uses Z3 as the primary solver with CVC5 as a fallback.

Common Pitfalls

• No subtype ranges: SPARK’s range 1 .. 100 does not have a direct Assura equivalent. Use refinement types: type Bounded = { v: Int | v >= 1 && v <= 100 }.
• Global annotations: SPARK’s Global => (In_Out => State) maps to Assura’s effect system. Use effects { mem } for in-memory state modification.
• Package structure: SPARK uses Ada packages (spec + body). Assura uses modules (.assura files). Each SPARK package spec maps to one Assura module.

Worked Example

SPARK Ada:

package Stack
  with SPARK_Mode => On
is
   Max_Size : constant := 100;
   type Element is new Integer;

   procedure Push (E : in Element)
     with Pre  => not Is_Full,
          Post => Size = Size'Old + 1 and Top = E,
          Global => (In_Out => State);

   function Is_Full return Boolean
     with Post => Is_Full'Result = (Size = Max_Size),
          Global => (Input => State);

   function Size return Natural
     with Global => (Input => State);

   function Top return Element
     with Pre    => Size > 0,
          Global => (Input => State);
end Stack;

Assura:

module stack

type Element = Int

contract push {
    input(e: Element)
    output(result: Unit)

    requires { size < 100 }
    ensures { old(size) + 1 == size }

    effects { mem }
}

contract is_full {
    input()
    output(result: Bool)

    ensures { result == (size == 100) }

    effects { pure }
}

contract size {
    input()
    output(result: Nat)

    ensures { result >= 0 }
    ensures { result <= 100 }

    effects { pure }
}

contract top {
    input()
    output(result: Element)

    requires { size > 0 }

    effects { pure }
}

Quick Reference: Equivalent Concepts