Assura

Write what it should do. AI proves it does.

Assura is a contract-first AI-native language that transpiles to verified Rust. Humans write behavioral contracts. AI writes implementations. The compiler proves correctness mathematically via SMT solvers. Ships as native or WASM binaries through rustc.

contract SafeDivision {
  input(a: Int, b: Int)
  output(result: Int)

  requires { b != 0 }
  ensures  { result * b + (a mod b) == a }
  ensures  { abs(result) <= abs(a) }
  effects  { pure }
}

Quick Start

# Preferred:
cargo install assura --locked

# Or from a monorepo clone:
# cargo install --path crates/assura-cli --locked

# Check a contract
assura check my_contract.assura

# Build (generates verified Rust)
assura build my_contract.assura

See CRATES-IO.md and the root README for co-publish details and prebuilt GitHub Release installers.

Documentation

• Getting started: Install, first check, build, run
• Tutorial: Broader language tour after the first contract
• What we prove: Verified / Unknown / Counterexample honesty map
• SMT portfolio note: Dual solvers, timeouts, Unknown policy
• Compared to other tools: Dafny, Verus, Liquid Haskell, tests
• Case studies: Heartbleed, libwebp, showcase demos
• For AI agents: JSON check, IR acceptance, MCP
• Preferred URLs: Canonical links (not assura.dev)
• Cheatsheet: Quick reference for syntax and features
• Cookbook: Common patterns and recipes
• Language Specification: Complete language reference
• Error code index: Axxxxx phase map for agents and humans
• Compiler Internals: How the compiler works

Getting Started with Assura

From install to a verified, runnable implementation.

This guide works on a clean machine (no monorepo required). It uses a tiny result-bearing showcase contract. For synthesizable ensures shapes (including result == x and multi-clause bounds), assura check synthesizes an in-memory implementation body so you get Verified without writing IR by hand. Residual shapes use assura build --write-ir (offline) or --auto-implement (LLM).

For broader language coverage, see TUTORIAL.md and demos/README.md (showcase vs EXPECT FAIL taxonomy).

After your first successful check, read What we prove so Verified / Unknown / Counterexample (and vacuous success) are not confused. AI-oriented workflow: AI-AGENTS.md.

1. Install

Preferred (crates.io): requires Rust 1.85+ (edition 2024). Z3 is pulled in automatically for verification builds.

cargo install assura --locked
assura --help

Prebuilt shell installer (GitHub Releases; no Rust toolchain needed for the binary itself): see the latest release assets (assura-installer.sh) or the root README. There is no Homebrew formula yet.

From a git checkout instead of crates.io:

cargo install --path crates/assura-cli --locked

1b. Try without a full local install

If you only want to see a check result before installing:

1. Open the repo in GitHub Codespaces (.devcontainer/devcontainer.json installs Rust + libz3-dev), then:

   cargo install --path crates/assura-cli --locked
   assura check demos/showcase-echo.assura
   

   Same commands work on any machine that already has Rust 1.85+ and Z3.
2. Watch the demo GIF (no install):
   https://github.com/assura-lang/assura/blob/main/assets/demo/assura-check.gif
3. Copy-paste the showcase from section 2 into a file after cargo install assura --locked.

There is no hosted WASM playground yet (tracked separately). Prefer install + one local check over a partial browser demo that cannot run Z3.

2. Create a tiny project

mkdir hello-assura && cd hello-assura

Write the contract only (ShowcaseEcho.assura). No sidecar required for identity:

cat > ShowcaseEcho.assura << 'EOF'
// SHOWCASE: result-bearing identity (auto-synthesized IR).
contract ShowcaseEcho {
  input(x: Int)
  output(result: Int)
  ensures { result == x }
}
EOF

In the Assura monorepo you can use demos/showcase-echo.assura (and optional demos/ShowcaseEcho.ir if you want an explicit sidecar).

3. Check (prefer all clauses Verified)

assura check ShowcaseEcho.assura

Expected: ShowcaseEcho: ensures ... verified and check passed (no errors).

Synthesizable ensures shapes (no hand IR):

Shapes the planner cannot synthesize still report Unknown (not a fake pass). Ladder when that happens:

1. Simplify ensures toward the table above, or
2. assura build file.assura --write-ir (offline heuristic IR next to source), or
3. assura build file.assura --auto-implement (offline first, then LLM for residuals).

Inequality synthesis picks one witness body (e.g. result >= x uses result = x); multi-bound clauses share one witness (prefer lower bound). That is not a full specification of every satisfying implementation.

Use assura check -v to see synthesized in-memory: ContractName. For multi-ensures contracts, verbose also names the body driver ensures (which clause selected the IR body) and any residual ensures that were not the driver (still checked under that body; may CE or stay Unknown). Agents using assura check --json get the same surface under file_info.ir (colocated, synthesized, synth_notes).

Optional: co-located IR sidecar

When you want an explicit body (or synthesis cannot cover the shape), add {ContractName}.ir next to the source (name matches the contract, not the file stem):

cat > ShowcaseEcho.ir << 'EOF'
module ShowcaseEcho {
  fn #0 : ($0: Int) -> Int ! pure
  {
    $result = load $0 : Int
  }
}
EOF

4. Build (IR becomes the implementation)

assura build ShowcaseEcho.assura --output generated

Assura loads co-located IR for verification and injects it into the generated Rust body (you should see a log line about injected IR bodies). assura build --write-ir also writes that IR next to the source so a later assura build reuses it. Field and abs/min/max/clamp/signum IR lower to real Rust (.y, .abs(), .min(), .clamp(), .signum()) that cargo test exercises via proptest. The generated crate is a library with a property test, not a binary.

5. Run tests on the generated artifact

cd generated
cargo test

Expected: proptest test test_showcaseecho passes (identity on random i64 inputs, with debug_assert! on the ensures).

Call the generated API from your own code:

use generated::contract_showcaseecho::check;

fn main() {
    assert_eq!(check(42), 42);
}

A minimal extra smoke test inside the generated crate (optional; do not commit edits under generated/, re-run assura build after contract changes):

cd generated
cat >> src/lib.rs << 'EOF'

#[cfg(test)]
mod smoke {
    #[test]
    fn echo_forty_two() {
        assert_eq!(super::contract_showcaseecho::check(42), 42);
    }
}
EOF
cargo test smoke::echo_forty_two

What you just proved

Offline IR (no LLM) and runnable binary

Generate co-located IR from ensures heuristics (no API key), inject it into Rust, and emit a binary you can cargo run:

assura build ShowcaseEcho.assura --write-ir --bin --output generated
cd generated
cargo run -- 42
# prints: 42

Auto-implement residual shapes

--auto-implement fills bodies for contracts that still lack IR:

1. Co-located .ir on disk (if any)
2. Offline ensures heuristics (same as --write-ir, no API key)
3. LLM only for remaining unanalyzable ensures (needs AI config)

assura build richer.assura --auto-implement --output generated

Strict verification (Unknown limitations fail the check):

assura check ShowcaseEcho.assura --strict

Directory mode for SHOWCASE demos only:

assura check demos --showcase-only

Next steps

• More demos: demos/README.md (prefer SHOWCASE files)
• Language tutorial: TUTORIAL.md
• Call-shaped helpers: same-file pure callees get non-identity IR siblings when their ensures are analyzable

Optional monorepo smoke

From a full clone (CI or local):

bash scripts/smoke-getting-started.sh
# or manually:
assura check demos/showcase-echo.assura
assura build demos/showcase-echo.assura --output /tmp/assura-gs-out
(cd /tmp/assura-gs-out && cargo test)

Assura Tutorial

A hands-on guide to writing, checking, and building Assura contracts.

Fastest path to a verified, runnable example: start with GETTING-STARTED.md (install → check → build → cargo test with co-located IR).

Installation

Preferred: crates.io

cargo install assura --locked

Requires Rust 1.85+ (edition 2024). The first build may download a Z3 prebuilt automatically.

Prebuilt binary

Download an installer from GitHub Releases (cargo-dist; multi-platform).

From source

# From a clone:
cargo install --path crates/assura-cli --locked

# Or from GitHub without cloning the tree:
cargo install --git https://github.com/assura-lang/assura assura --locked

Verify the installation

assura --help

Prerequisites for verification

The Z3 SMT solver is downloaded automatically during cargo build (via the z3 crate’s gh-release feature). No manual Z3 installation is needed.

CVC5 is an optional alternative solver for portfolio mode (tries both solvers). It is not required for normal use:

bash scripts/setup-cvc5.sh
# paste the printed export lines (CVC5_LIB_DIR, CVC5_INCLUDE_DIR)

Step 1: Create a Project

assura init my-project
cd my-project

This creates:

my-project/
  assura.toml           # Project configuration
  contracts/
    lib.assura          # Starter contract

The generated assura.toml:

[package]
name = "my-project"
version = "0.1.0"

[build]
target = "native"       # "native" or "wasm32-wasi"
output = "generated"

[verify]
smt-solver = "z3"       # "z3", "cvc5", or "portfolio"
layer = 1               # 0 = structural only, 1 = SMT
timeout = 1000          # SMT timeout in ms

# [dependencies]         # Optional: import contracts from other projects
# math-lib = { path = "../math-lib" }

Step 2: Write a Contract

Edit contracts/lib.assura:

contract SafeDivision {
    input(a: Int, b: Int)
    output(result: Int)

    requires { b != 0 }
    ensures  { b != 0 }
}

A contract declares:

• input(…): parameters the function accepts
• output(…): what it returns
• requires { … }: preconditions (caller’s responsibility)
• ensures { … }: postconditions (implementation’s responsibility)

The ensures { b != 0 } clause is trivially verified by Z3 because the requires clause already guarantees b != 0. As you learn the language, you’ll write more expressive postconditions.

Step 3: Check Your Contract

assura check contracts/lib.assura

Output:

Verification (1 clause(s)):
  SafeDivision:
    ensures              ... verified
contracts/lib.assura: check passed (no errors)

Verbose mode

assura check contracts/lib.assura --verbose

Shows timing for each pipeline phase (lex, parse, resolve, typecheck, verify).

Verification layers

What Verified / Unknown / Counterexample mean (and what is not proved): What we prove.

assura check contracts/lib.assura --layer 0

Step 4: Build to Rust

assura build contracts/lib.assura

This generates a Rust project in generated/:

generated/
  Cargo.toml
  src/
    lib.rs

The generated Rust includes debug_assert! statements derived from your requires and ensures clauses. Run the generated code:

cd generated
cargo test

Custom output directory

assura build contracts/lib.assura --output my-output

WASM target

assura build contracts/lib.assura --target wasm

This generates a project configured for wasm32-wasip1, including a .cargo/config.toml with the target pre-set.

Step 5: Multi-File Projects

As your project grows, split contracts across multiple files and use imports to reference them.

Project layout

my-project/
  assura.toml
  contracts/
    lib.assura          # Root contract
    math.assura         # Imported by lib

Importing local modules

Use dot-separated paths. The path maps to the filesystem relative to the project root:

import contracts.math

contract App {
    input(x: Int)
    requires { x >= 0 }
}

import contracts.math loads contracts/math.assura.

External dependencies

Add a [dependencies] section to assura.toml to import contracts from other projects:

[package]
name = "my-project"
version = "0.1.0"

[dependencies]
math-lib = { path = "../math-lib" }

Then import from the dependency using its name (hyphens become underscores in import paths):

import math_lib.core

contract App {
    input(x: Int)
    requires { x >= 0 }
}

Checking a project

Point assura check at the project directory (not a single file):

assura check .

This discovers all .assura files, resolves imports (including dependencies), and type-checks every module.

Step 6: Understand Errors

When a contract fails verification, Assura shows a counterexample:

Verification (1 clause(s)):
  SafeDivision:
    ensures    ... COUNTEREXAMPLE
      | result -> 0
      | a -> 1
      | b -> 2

Use assura explain to learn about specific error codes:

assura explain A03001   # Type mismatch
assura explain A05001   # Linear type used twice
assura explain A07003   # Unknown effect

Error spans are precise even for expressions inside braced clauses (e.g. requires { x > 0 }), thanks to full trivia capture in the parser. A type error on true will point exactly at the sub-expression, not the requires keyword.

Contract Features

Refinement types

Narrow a base type with a predicate:

type Positive = { v: Int | v > 0 }
type Percentage = { v: Float | v >= 0.0 && v <= 100.0 }

Effects

Declare what side effects a contract may perform:

contract ReadFile {
    effects {
        io
        fs
    }
    requires {
        path != ""
    }
}

Valid effect names: io, database, logging, mem, net, fs, rng, time, alloc, diverge, random, and dotted sub-effects like console.read, filesystem.write.

Quantifiers

Express properties over collections:

contract Sorted {
    ensures {
        forall i in data : i >= 0
    }
}

Services with typestate

Model stateful protocols:

service Connection {
    states { Disconnected, Connected }

    operation connect {
        requires {
            host != ""
        }
        ensures {
            connected == true
        }
    }
}

Ghost code and decreases clauses

Prove termination of recursive algorithms:

fn factorial(n: Nat) -> Nat
    requires {
        n >= 0
    }
    ensures {
        result >= 1
    }
    decreases {
        n
    }

Formatting

Format .assura files (like rustfmt for Rust):

assura fmt contracts/lib.assura

Check formatting without modifying:

assura fmt contracts/lib.assura --check

Solver Selection

Choose which SMT solver to use:

# Z3 (default)
assura check file.assura --solver z3

# CVC5
assura check file.assura --solver cvc5

# Portfolio: tries Z3 first, falls back to CVC5 on timeout
assura check file.assura --solver portfolio

Or set it in assura.toml:

[verify]
smt-solver = "portfolio"

VS Code Extension

Install the extension for syntax highlighting and LSP integration:

cd editors/vscode
npm install && npm run compile

Features: syntax highlighting, inline diagnostics via the Assura LSP server.

AI Agent Setup

To configure an AI coding assistant to use Assura, run:

assura agent-instructions > .assura-context.md

This outputs a compact reference with Assura syntax, type mappings, CLI commands, and workflow steps that you can add to your agent’s system prompt or project instructions (AGENTS.md, .cursorrules, etc.).

See the scenario guides for detailed walkthroughs of AI-assisted development workflows.

Part 2: Learning by Example

This section walks through five contracts of increasing complexity. Each builds on concepts from the previous one.

Example 1: Input Validation

The simplest useful contract: validate that a username meets length requirements.

contract ValidateUsername {
  input(name: String, min_len: Nat, max_len: Nat)
  output(valid: Bool)

  requires { min_len > 0 }
  requires { max_len >= min_len }
  requires { name.length() >= 0 }

  ensures { max_len >= min_len }
}

Save this as validate.assura and run:

assura check validate.assura

Expected output:

  ValidateUsername:
    ensures              ... verified
validate.assura: check passed (no errors)

What you learned: requires sets preconditions that callers must satisfy. ensures sets postconditions that the implementation must guarantee. Z3 proves ensures holds given the requires.

Example 2: Arithmetic with Multiple Clauses

Contracts can have multiple requires and ensures clauses. Each is checked independently.

contract SafeAverage {
  input(a: Int, b: Int, max: Int)
  output(avg: Int)

  requires { a >= 0 }
  requires { b >= 0 }
  requires { max > 0 }
  requires { a <= max }
  requires { b <= max }

  ensures { max >= 0 }
  ensures { a + b >= 0 }
}

This contract specifies an averaging function where both inputs are non-negative and bounded by max. Z3 proves each ensures clause independently against the combined requires.

Example 3: A Failing Contract (Reading Counterexamples)

This contract has a bug: the ensures clause does not follow from the preconditions.

contract BuggyClamp {
  input(value: Int, low: Int, high: Int)
  output(result: Int)

  requires { low <= high }

  ensures { result >= low }
}

Run assura check buggy_clamp.assura and you will see:

  BuggyClamp:
    ensures              ... counterexample found
      result = -1, low = 0

Why it fails: result is an unconstrained output variable. Z3 can assign it any value. Since nothing forces result >= low, Z3 finds result = -1, low = 0 as a counterexample.

The lesson: In Assura, result and output variables are free (the language is specification-only, with no implementation bodies). Write ensures clauses that follow logically from requires, or that constrain relationships between inputs only.

Example 4: Effects and Safety Annotations

Assura tracks side effects. Declare which effects a function may perform:

contract ReadConfig {
  input(path: String)
  output(config: String)

  effects { io, fs }

  requires { path.length() > 0 }
  ensures { path.length() > 0 }
}

Valid effect names include: io, fs, net, database, logging, mem, rng, time, alloc, and dotted sub-effects like filesystem.write, network.connect, database.read.

Example 5: Invariants and Quantifiers

Contracts can express properties that must hold for all elements:

contract SortedArray {
  input(arr: List<Int>, n: Nat)

  requires { n >= 0 }
  // Every element is non-negative (real property of `arr`, not a tautology).
  invariant { forall i in arr: i >= 0 }

  ensures { n >= 0 }
}

Use --layer 2 for quantified invariant verification:

assura check sorted.assura --layer 2

Part 3: Real-World CVE Walkthrough

This section walks through demos/heartbleed.assura, which models CVE-2014-0160 (the Heartbleed bug).

The Vulnerability

Heartbleed was a buffer over-read in OpenSSL’s TLS heartbeat extension. The server reads payload_length bytes from the request but does not check that payload_length is within the actual received data. An attacker sends a small payload with a large payload_length, causing the server to leak memory contents.

CVSS: 7.5 (High)

The Assura Contract

Open demos/heartbleed.assura:

contract tls_heartbeat_response {
  input(
    payload_length: Nat,
    padding_length: Nat,
    record_length: Nat
  )
  output(response: Bytes)

  requires { payload_length > 0 }
  requires { padding_length > 0 }
  requires { 3 + payload_length + padding_length <= record_length }
  requires { record_length > 0 }

  ensures { record_length > payload_length }
  ensures { record_length > 0 }
}

What Each Clause Does

• requires { payload_length > 0 }: The payload must not be empty
• requires { 3 + payload_length + padding_length <= record_length }: The key fix: total size (3-byte header + payload + padding) must fit within the record. This is the check that OpenSSL was missing.
• ensures { record_length > payload_length }: The record is always larger than the payload (no over-read possible)

Running the Check

assura check demos/heartbleed.assura --verbose

Z3 proves that record_length > payload_length follows from 3 + payload_length + padding_length <= record_length (since padding_length > 0, the record must be strictly larger).

What Would Happen Without the Fix

Remove the bounds-check requires clause and Z3 immediately finds a counterexample: payload_length = 100, record_length = 5. This is exactly the Heartbleed scenario.

Part 4: Common Mistakes and Debugging

“counterexample found” on ensures

Symptom: Your ensures clause gets a counterexample even though it “should” be true.

Cause: Output variables (result, variables in output()) are free. Z3 can assign them any value. Your ensures must follow logically from requires alone, or constrain only input relationships.

Fix: Either:

1. Make your ensures reference only input variables
2. Add requires clauses that constrain the relationship more tightly

“unknown” instead of “verified”

Symptom: Z3 returns “unknown” for a clause.

Possible causes:

• Timeout: The formula is too complex. Try --timeout 30000 (30s)
• Non-linear arithmetic: Z3 struggles with multiplication of variables. Simplify the formula or use --solver cvc5
• Unmodelable features: Some language features are not yet encoded in SMT. The CLI shows these as warnings (exit 0)

Unknown effect names

Symptom: Error A07003 “unknown effect”

Fix: Use one of the known effect names: io, database, logging, mem, net, fs, rng, time, alloc, diverge, random. For sub-effects, use dotted names: console.read, filesystem.write, network.connect, database.read, log.info.

“expected type X, got Y”

Symptom: Type error A03001

Fix: Check that your types match. Common mistakes:

• Using Integer instead of Int
• Using Natural instead of Nat
• Mixing Int and Nat without explicit bounds

Reading error output

Assura uses ariadne for rich error display:

error[A03001]: type mismatch
  --> myfile.assura:5:12
   |
 5 |   requires { x > "hello" }
   |              ^^^^^^^^^^^ expected Int, found String

The arrow (-->) points to the file and line. The underline shows exactly which expression has the error. Use assura explain A03001 for a detailed description of any error code.

Verification layers

Higher layers are slower but check more properties. Start with the default (layer 1) and increase when needed.

Part 5: Integration Guides

CI Integration

Add Assura checks to your GitHub Actions workflow:

name: Assura
on: [push, pull_request]
jobs:
  check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable
      - name: Install Z3
        run: sudo apt-get install -y libz3-dev
      - name: Install Assura
        run: cargo install --git https://github.com/assura-lang/assura assura
      - name: Check contracts
        run: assura check src/**/*.assura

LSP Integration

The Assura LSP server provides real-time diagnostics in your editor:

# Start the LSP server
assura lsp

Configure your editor’s LSP client to use assura lsp as the server command. The server provides:

• Inline diagnostics (parse errors, type errors, verification results)
• Hover information (type of expressions, contract summaries)
• Go to definition
• Document symbols

MCP Server

For AI agent integration, Assura provides an MCP (Model Context Protocol) server:

# Start the MCP server
assura mcp

The MCP server exposes tools that AI agents can use to check contracts, get error explanations, and generate contract templates.

gRPC Server

For programmatic access from any language:

# Start the gRPC server
assura server --port 50051

The gRPC API supports streaming verification results and batch checking.

Quick Reference

Contract Structure

contract Name {
  input(param1: Type1, param2: Type2)
  output(result: Type)

  requires { precondition }
  ensures { postcondition }
  invariant { property }
  effects { effect1, effect2 }
  decreases { measure }
}

Types

Operators

CLI Commands

Declaration Types

# Standard contract
contract Name { ... }

# External function (no body)
extern fn name(params) -> ReturnType { ... }

# Function with contract
fn name(params) -> ReturnType { ... }

# Liveness property
liveness Name {
  prove: eventually(condition)
}

# Service with typestate
service Name {
  states { State1, State2 }
  transitions { State1 -> State2 }
}

# Feature max constant
feature_max NAME: Type = value

# Enum type
enum Name { Variant1, Variant2 }

Next Steps

• Read the scenario guides for real workflow walkthroughs
• Read the demo contracts in demos/ for real-world examples
• See the language specification for the full grammar
• See the internals documentation for compiler architecture

Assura Quick Reference

Types

Refinement Types

x: Int where x > 0           // inline refinement
x: { n: Int | n >= 0 }       // set-builder syntax
data: NonEmpty<List<Int>>     // named refinement

Declaration Forms

Contract (standalone specification)

contract SafeDivision {
  input(a: Int, b: Int)
  output(result: Int)
  requires { b != 0 }
  ensures  { result * b + (a mod b) == a }
  effects  { pure }
}

Bind (attach contract to existing Rust function)

bind "mylib::divide" as divide_checked {
  input(a: Int, b: Int)
  output(result: Int)
  requires { b != 0 }
  ensures  { result == a / b }
}

Function

fn helper(x: Int) -> Bool
  requires { x >= 0 }
  ensures  { result == (x mod 2 == 0) }

Service (typestate)

service Connection {
  states { Disconnected, Connected, Authenticated }
  transitions {
    connect: Disconnected -> Connected
    login:   Connected -> Authenticated
    close:   * -> Disconnected
  }
}

Other declarations

type Percentage = { n: Float | n >= 0.0 && n <= 100.0 }
enum Status { Active, Inactive, Suspended }
extern fn system_time() -> Nat effects { time }
block incremental { ... }

Contract Clauses

Expression Builtins

Operator Precedence (low to high)

Effect Names

Group effects (expand to sub-effects)

Short aliases

mem, net, fs, rng, time, alloc, diverge, random

Pure functions

effects { pure }   // no side effects allowed

Custom sub-effects

Any group.sub where group is known is accepted: io.custom, database.migrate.

Error Code Ranges

Look up any code: assura explain A03001

CLI Commands

assura check file.assura          # verify (parse + resolve + types + SMT)
assura check file.assura --watch  # re-verify on save
assura build file.assura          # verify + generate Rust code
assura init my-project            # scaffold new project
assura fmt file.assura            # format source
assura fmt file.assura --check    # check formatting (CI)
assura explain A03001             # explain error code
assura infer src/lib.rs           # generate bind skeletons from Rust
assura test-gen file.assura       # generate proptest code
assura audit .                    # scan Rust project for violations
assura coverage .                 # show contract coverage
assura doctor                     # check dependencies
assura agent-instructions         # AI agent quick reference
assura completions zsh            # generate shell completions

Common Patterns

// Safe division
requires { divisor != 0 }

// Bounds check
requires { index >= 0 && index < length(data) }

// Non-empty input
requires { length(items) > 0 }

// Monotonicity
ensures { result >= old(counter) }

// Size preservation
ensures { length(result) == length(input) }

Assura Contract Cookbook

Ready-to-copy contract patterns organized by category. Each pattern is self-contained. For syntax basics, see the tutorial.

Arithmetic Safety

Safe Division

Prevents: division by zero, incorrect quotient

contract SafeDivision {
    input(a: Int, b: Int)
    output(result: Int)

    requires { b != 0 }
    ensures  { result * b + (a mod b) == a }
    ensures  { abs(result) <= abs(a) }
    effects  { pure }
}

Integer Overflow Guard

Prevents: silent integer overflow on addition

contract SafeAdd {
    input(a: Int, b: Int, max: Int)
    output(result: Int)

    requires { a >= 0 }
    requires { b >= 0 }
    requires { a + b <= max }
    ensures  { result == a + b }
    ensures  { result >= 0 }
    effects  { pure }
}

Percentage Bounds

Prevents: percentage values outside 0..100

type Percentage = { v: Float | v >= 0.0 && v <= 100.0 };

contract ApplyDiscount {
    input(price: Float, discount: Percentage)
    output(result: Float)

    requires { price >= 0.0 }
    ensures  { result >= 0.0 }
    ensures  { result <= price }
    effects  { pure }
}

Bounds Checking

Safe Array Index

Prevents: out-of-bounds array access

contract SafeIndex {
    input(arr: List<Int>, index: Nat)
    output(result: Int)

    requires { index < arr.length() }
    effects  { pure }
}

Bounded Slice

Prevents: slice overrun past buffer end

contract SafeSlice {
    input(buf: Bytes, offset: Nat, len: Nat)
    output(data: Bytes)

    requires { offset + len <= buf.length() }
    ensures  { data.length() == len }
    effects  { pure }
}

Buffer Capacity

Prevents: writes past allocated buffer capacity

contract BoundedBuffer {
    input(capacity: Nat, count: Nat, item_size: Nat)

    requires { capacity > 0 }
    requires { count * item_size <= capacity }
    invariant { count * item_size <= capacity }
    effects  { pure }
}

String and Bytes

Non-Empty String

Prevents: empty string passed where content is required

contract NonEmptyInput {
    input(name: String)

    requires { name.length() > 0 }
    effects  { pure }
}

Bounded String Length

Prevents: oversized strings causing truncation or overflow

contract BoundedString {
    input(value: String, max_len: Nat)

    requires { value.length() > 0 }
    requires { value.length() <= max_len }
    requires { max_len <= 65535 }
    effects  { pure }
}

Option/Result Safety

Safe Unwrap via Precondition

Prevents: unwrap on None/Err

contract SafeUnwrap {
    input(value: Int?, default_val: Int)
    output(result: Int)

    ensures { result == if value != null then value else default_val }
    effects { pure }
}

Error Propagation

Prevents: unhandled error cases

fn parse_port(s: String) -> Int?
    requires { s.length() > 0 }
    ensures  { result != null implies result >= 1 }
    ensures  { result != null implies result <= 65535 }
    effects  { pure }

Collection Properties

Non-Empty Collection

Prevents: operations on empty collections (head, reduce, min, max)

contract NonEmptyList {
    input(items: List<Int>)
    output(result: Int)

    requires { items.length() > 0 }
    effects  { pure }
}

Sorted Output

Prevents: sort functions that return unsorted data

contract SortContract {
    input(arr: List<Int>)
    output(result: List<Int>)

    requires { arr.length() > 0 }
    ensures  { result.length() == arr.length() }
    ensures  { forall i in 0..result.length() - 1: result[i] <= result[i + 1] }
    effects  { pure }
}

Element Uniqueness

Prevents: duplicate entries in collections that require distinct elements

contract UniqueElements {
    input(items: List<Int>, new_item: Int)
    output(result: List<Int>)

    requires { forall i in items: i != new_item }
    ensures  { result.length() == items.length() + 1 }
    effects  { pure }
}

Monotonicity and Ordering

Monotonic Counter

Prevents: counter decrement, stale sequence numbers

contract IncrementCounter {
    input(current: Nat, amount: Nat)
    output(result: Nat)

    requires { amount > 0 }
    ensures  { result > current }
    ensures  { result == current + amount }
    effects  { pure }
}

Timestamp Ordering

Prevents: out-of-order event timestamps

contract AppendEvent {
    input(last_ts: Nat, new_ts: Nat)

    requires { new_ts > last_ts }
    ensures  { new_ts > last_ts }
    effects  { pure }
}

Resource Lifecycle

Connection Open/Close

Prevents: use-after-close, double-close, resource leaks

service Connection {
    states: Closed -> Open -> Closed

    operation Open {
        input(host: String)
        requires { host.length() > 0 }
        requires { self.state == Closed }
        ensures  { self.state == Open }
        effects  { net }
    }

    operation Send {
        input(data: Bytes)
        requires { self.state == Open }
        requires { data.length() > 0 }
        ensures  { self.state == Open }
        effects  { net }
    }

    operation Close {
        requires { self.state == Open }
        ensures  { self.state == Closed }
        effects  { net }
    }
}

Acquire/Release Lock

Prevents: double-acquire, use without lock, forgotten release

service Mutex {
    states: Unlocked -> Locked -> Unlocked

    operation Acquire {
        requires { self.state == Unlocked }
        ensures  { self.state == Locked }
        effects  { mem }
    }

    operation Release {
        requires { self.state == Locked }
        ensures  { self.state == Unlocked }
        effects  { mem }
    }
}

Effects and Purity

Pure Computation

Prevents: accidental side effects in business logic

contract PureTransform {
    input(items: List<Int>)
    output(result: List<Int>)

    requires { items.length() > 0 }
    ensures  { result.length() == items.length() }
    effects  { pure }
}

IO Isolation

Prevents: database access from code that should only do network IO

fn fetch_remote(url: String) -> Bytes
    requires { url.length() > 0 }
    effects  { net }

fn save_to_db(data: Bytes) -> Bool
    requires { data.length() > 0 }
    effects  { database.write }

fn api_handler(url: String) -> Bool
    requires { url.length() > 0 }
    effects  { net, database.write }

Taint Tracking

Untrusted Input Validation

Prevents: unsanitized user input reaching sensitive operations

fn read_user_input() -> String @taint:untrusted
    effects { io }

fn validate_input(
    raw: String @taint:untrusted,
    max_len: Nat
) -> String @taint:validated
    requires { max_len > 0 }
    effects  { pure }
{
    validate {
        raw.length() > 0 && raw.length() <= max_len
    } raw
        or ""
}

fn execute_query(query: String @taint:validated) -> Int
    effects { database.read }

Quantifiers

All Elements Positive

Prevents: negative values slipping into a non-negative collection

contract AllPositive {
    input(items: List<Int>)

    requires { items.length() > 0 }
    ensures  { forall i in items: i >= 0 }
    effects  { pure }
}

Element Exists

Prevents: search returning not-found when element is guaranteed present

contract FindElement {
    input(arr: List<Int>, n: Nat, target: Int)
    output(result: Int)

    requires { n > 0 }
    requires { exists i in 0..n: arr[i] == target }
    ensures  { result == target }
    effects  { pure }
}

Bind Declarations

Retrofit Existing Rust Function

Prevents: calling an existing Rust function without contract enforcement

bind "my_crate::math::divide" as safe_divide {
    input(a: Int, b: Int)
    output(result: Int)
    requires { b != 0 }
    ensures  { result * b == a }
}

Bind with Effects

Prevents: calling an FFI function without declaring its side effects

bind "libc::malloc" as safe_malloc {
    input(size: Nat)
    output(result: Bytes)
    requires { size > 0 }
    ensures  { result.length() == size }
    effects  { mem }
}

Key Derivation and Crypto

Secure Key Length

Prevents: weak cryptographic keys

contract SecureKeyDerivation {
    input(password_len: Nat, salt_len: Nat, iterations: Nat)

    requires { password_len >= 8 }
    requires { salt_len >= 16 }
    requires { iterations >= 100000 }
    effects  { pure }
}

Case studies

Short public write-ups of demos you can run today. Full sources live under demos/. Showcase (must-pass) vs EXPECT FAIL taxonomy: demos/README.md.

Heartbleed-class bounds (CVE-2014-0160)

Story: OpenSSL Heartbleed read attacker-controlled payload_length without ensuring the record actually contained that many bytes.

Demo: demos/heartbleed.assura

Run:

assura check demos/heartbleed.assura

What the contract encodes: preconditions on record layout and padding so response size cannot exceed the buffer (bounds safety as SMT-checkable ensures on inputs).

What is proved: when the contract is in the supported fragment and check reports Verified for those clauses, the modeled over-read is impossible under the stated requires. See What we prove.

libwebp Huffman / heap overflow class (CVE-2023-4863)

Story: a CVSS 9.8 heap buffer overflow in libwebp (WebP) affected browsers and Electron apps.

Demo: demos/libwebp-huffman.assura

Run:

assura check demos/libwebp-huffman.assura
# optional:
assura check demos/libwebp-huffman.assura --verbose --stats

What the contract encodes: memory region, taint, table, and related feature surface aimed at the class of bug (see file header comments).

What is proved: structural + SMT obligations that fire for the features actually modeled on that file. Treat Unknown limitation markers as incomplete encoding, not green proof.

Showcase identity (happy path)

Story: smallest result-bearing path for onboarding.

Demo: demos/showcase-echo.assura (or the copy-paste file in GETTING-STARTED.md)

Run:

assura check demos/showcase-echo.assura

assura check synthesizes analyzable IR for simple result == x shapes so you can see Verified without hand-written IR.

Next

• More patterns: Cookbook
• AI implement loop: GETTING-STARTED.md, design note DESIGN-AI-VERIFICATION-LOOP.md

Assura Scenario Walkthroughs

Five practical scenarios showing how to use Assura in real workflows. Each includes exact commands, example code, and expected output.

Table of Contents

1. Greenfield Development with AI + Assura
2. Retrofitting Contracts onto Existing Rust Code
3. Security Audit with assura audit
4. CI Integration (GitHub Actions)
5. Team Onboarding and Progressive Adoption

Scenario 1: Greenfield Development with AI + Assura

You are starting a new project from scratch. You want an AI coding agent to write both the contracts and the Rust implementation, with Assura verifying correctness at every step.

1.1 Project setup

assura init safe-parser
cd safe-parser

This creates:

safe-parser/
  assura.toml
  contracts/
    lib.assura

The generated assura.toml:

[package]
name = "safe-parser"
version = "0.1.0"

[build]
target = "native"       # "native" or "wasm32-wasi"
output = "generated"

[verify]
smt-solver = "z3"       # "z3", "cvc5", or "portfolio"
layer = 1               # 0 = structural only, 1 = SMT
timeout = 1000          # SMT timeout in ms

[profile]
type = "minimal"        # minimal, parser, database, etc.

1.2 Instructing the AI agent

Add this to your project’s AGENTS.md (or system prompt) so the AI understands the contract-first workflow:

## Development Workflow

1. Write an Assura contract FIRST that specifies the function's behavior.
2. Run `assura check contracts/lib.assura` to verify the contract is
   well-formed and the clauses are satisfiable.
3. Write the Rust implementation that satisfies the contract.
4. Run `assura build contracts/lib.assura` to generate verified Rust
   stubs with debug_assert! guards from the contract.
5. If `assura check` reports a counterexample, fix the contract or
   implementation before proceeding.

## Assura Type Mapping

Use these types in contracts (not Rust types):
- i32/i64/isize -> Int
- u32/u64/usize -> Nat
- f64 -> Float
- bool -> Bool
- String/&str -> String
- Vec<u8> -> Bytes
- Vec<T> -> List<T>
- Option<T> -> T?

## Contract Structure

contract Name {
    input(param: Type, ...)
    output(result: ReturnType)
    requires { precondition }
    ensures  { postcondition }
    effects  { pure | io | fs | net | ... }
}

1.3 Worked example: safe string parser with bounded output

Instead of the starter SafeDivision contract, write a contract for a string parser that extracts a bounded substring.

Edit contracts/lib.assura:

// Safe bounded substring extraction.
// Guarantees: no out-of-bounds access, output length matches request.

contract BoundedSubstring {
    input(s: String, start: Nat, len: Nat)
    output(result: String)

    requires { start + len <= s.length() }
    requires { len > 0 }
    ensures  { result.length() == len }
    effects  { pure }
}

// Token parser: splits input on a delimiter, returns bounded results.
// Guarantees: token count is at most max_tokens, no token exceeds max_len.

contract TokenParser {
    input(input: String, delimiter: String, max_tokens: Nat, max_len: Nat)
    output(result: List<String>)

    requires { delimiter.length() > 0 }
    requires { max_tokens > 0 }
    requires { max_len > 0 }
    ensures  { result.length() <= max_tokens }
    ensures  { forall t in result: t.length() <= max_len }
    effects  { pure }
}

1.4 Check the contract

assura check contracts/lib.assura --verbose

Expected output (exact text depends on contract complexity):

Pipeline timing for contracts/lib.assura:
  lex:       85 tokens (0.12ms)
  parse:     2 declaration(s), 0 import(s) (0.08ms)
  resolve:   4 symbol(s) (0.03ms)
  typecheck: 8 binding(s) (0.15ms)

Verification (4 clause(s)):
  BoundedSubstring:
    requires  ✓ verified
    ensures   ✓ verified
  TokenParser:
    requires  ✓ verified
    ensures   ✓ verified

contracts/lib.assura: check passed (no errors)

1.5 Iterating on counterexamples

Suppose you write a buggy contract:

contract BadDivision {
    input(a: Int, b: Int)
    output(result: Int)

    requires { b >= 0 }
    ensures  { result * b == a }
    effects  { pure }
}

The requires clause allows b == 0, which makes the ensures clause unsatisfiable for a != 0. Running:

assura check contracts/lib.assura

Produces:

Error[A05100]: verification failed for BadDivision: ensures:
               counterexample: a = 1, b = 0

contracts/lib.assura: 1 error(s) found

The counterexample shows concrete values that violate the contract. Fix it by changing b >= 0 to b > 0 (or b != 0 to also allow negative divisors).

1.6 Live feedback with watch mode

Run the checker in watch mode while editing:

assura check contracts/lib.assura --watch

Output on startup:

[watch] Checking contracts/lib.assura...

contracts/lib.assura: check passed (no errors)

[watch] Watching contracts/lib.assura for changes. Press Ctrl+C to stop.

Every time you save the file, the checker re-runs automatically. If the content has not changed (editor auto-save, formatter), it skips the re-check to avoid redundant work.

On change:

[watch] File changed, re-checking contracts/lib.assura...

Verification (4 clause(s)):
  BoundedSubstring:
    requires  ✓ verified
    ensures   ✓ verified
  ...

contracts/lib.assura: check passed (no errors)

[watch] Watching for changes. Press Ctrl+C to stop.

1.7 Build to Rust

Once contracts are verified, generate the Rust project:

assura build contracts/lib.assura --output generated

Expected output:

  wrote generated/Cargo.toml
  wrote generated/src/lib.rs
OK  contracts/lib.assura -> generated/ (generated Rust compiles)

The generated generated/src/lib.rs contains Rust functions with debug_assert! guards derived from your contract clauses. You can now add your implementation inside these function bodies.

To target WASM instead of native:

assura build contracts/lib.assura --target wasm --output generated

This additionally writes generated/.cargo/config.toml with target = "wasm32-wasip1" and runs cargo build --target wasm32-wasip1.

1.8 Verification statistics

Use --stats to see detailed timing and clause counts:

assura check contracts/lib.assura --stats

=== Verification Statistics ===
  Clauses:         4
  Verified:        4
  Counterexamples: 0
  Timeouts:        0
  Unknown:         0

  Lex time:        0.12ms (85 tokens)
  Parse time:      0.08ms
  Resolve time:    0.03ms
  Type-check time: 0.15ms
  Verify time:     12.45ms
  Total time:      12.83ms

Scenario 2: Retrofitting Contracts onto Existing Rust Code

You have an existing Rust codebase and want to add Assura contracts incrementally, without rewriting anything.

2.1 Bootstrap contract skeletons with assura infer

Suppose you have a file src/parser.rs:

#![allow(unused)]
fn main() {
pub fn parse_header(data: &[u8], offset: usize) -> Option<Header> {
    if offset + HEADER_SIZE > data.len() {
        return None;
    }
    let magic = u32::from_le_bytes(data[offset..offset+4].try_into().unwrap());
    let version = data[offset + 4];
    let length = u16::from_le_bytes(data[offset+5..offset+7].try_into().unwrap());
    Some(Header { magic, version, length: length as usize })
}

pub fn validate_checksum(data: &[u8], expected: u32) -> bool {
    let mut sum: u32 = 0;
    for byte in data {
        sum = sum.wrapping_add(*byte as u32);
    }
    sum == expected
}

pub fn extract_payload(data: &[u8], offset: usize, length: usize) -> Vec<u8> {
    data[offset..offset+length].to_vec()
}
}

Generate skeleton contracts:

assura infer src/parser.rs

Output (printed to stdout):

// Generated by: assura infer src/parser.rs
// Review and refine these contracts before use.

bind "crate::parser::parse_header" as parse_header {
    input(data: Bytes, offset: Nat)
    output(result: Header?)
    // TODO: add requires clauses (preconditions)
    // TODO: add ensures clauses (postconditions)
}

bind "crate::parser::validate_checksum" as validate_checksum {
    input(data: Bytes, expected: Nat)
    output(result: Bool)
    // TODO: add requires clauses (preconditions)
    // TODO: add ensures clauses (postconditions)
}

bind "crate::parser::extract_payload" as extract_payload {
    input(data: Bytes, offset: Nat, length: Nat)
    output(result: Bytes)
    // TODO: add requires clauses (preconditions)
    // TODO: add ensures clauses (postconditions)
}

// 3 function(s) analyzed from src/parser.rs

Write to a file instead:

assura infer src/parser.rs --output contracts/parser.assura

Filter to a single function:

assura infer src/parser.rs --function parse_header

2.2 Refining skeleton contracts

The skeletons have the right types but no invariants. Add real contracts:

bind "crate::parser::parse_header" as parse_header {
    input(data: Bytes, offset: Nat)
    output(result: Header?)

    requires { offset + 7 <= data.length() }
    ensures  {
        result.is_some() implies
            result.unwrap().length <= data.length() - offset
    }
}

bind "crate::parser::extract_payload" as extract_payload {
    input(data: Bytes, offset: Nat, length: Nat)
    output(result: Bytes)

    requires { offset + length <= data.length() }
    ensures  { result.length() == length }
}

2.3 The bind declaration in detail

bind attaches a contract to an existing Rust function without modifying the Rust source. The syntax:

bind "rust::module::path::function_name" as local_name {
    input(param1: AssuraType, param2: AssuraType)
    output(result: AssuraReturnType)

    requires { precondition_expression }
    ensures  { postcondition_expression }
    effects  { effect_list }
}

• The quoted string is the full Rust path to the function.
• as local_name gives the contract a name for Assura’s symbol table.
• input lists parameters with Assura types (not Rust types).
• output declares the return type. Use result to refer to it in ensures clauses.
• requires states what must be true before the function is called.
• ensures states what must be true after the function returns.
• effects declares side effects: pure, io, fs, net, mem, database, logging, rng, time, alloc.

2.4 Finding a real bug via counterexample

The extract_payload function above has a latent bug: if offset + length overflows usize, the slice operation panics. Without the contract’s requires clause, callers could pass values that trigger this.

Run verification:

assura check contracts/parser.assura

If the contract’s requires clause is missing:

Error[A05100]: verification failed for extract_payload: ensures:
               counterexample: data = [], offset = 1, length = 0

contracts/parser.assura: 1 error(s) found

The counterexample reveals that with an empty data array and a nonzero offset, the function would access out-of-bounds memory. The contract forces callers to prove offset + length <= data.length() before calling.

2.5 Incremental adoption strategy

You do not need to contract every function at once. A practical progression:

1. Start with assura infer on your most critical modules (parsers, crypto, network handlers).
2. Refine the generated skeletons with real preconditions and postconditions.
3. Run assura check on those contracts. Fix any counterexamples.
4. Add contracts to more modules over time.
5. Wire assura check into CI (see Scenario 4) so regressions are caught.

Focus on functions that:

• Parse untrusted input
• Perform arithmetic on sizes or offsets
• Handle cryptographic material
• Manage state transitions

2.6 AI prompt for retrofitting

Give an AI coding agent this prompt to automate the refinement step:

I have Assura skeleton contracts generated by `assura infer`. For each
bind declaration, analyze the Rust source function and:

1. Add requires clauses for every precondition the function assumes
   (non-null, in-bounds, non-zero divisor, valid state).
2. Add ensures clauses for every postcondition the function guarantees
   (output length, return value bounds, state changes).
3. Add effects declarations (pure, io, fs, net, mem, etc.).
4. Do NOT write vacuous contracts (always-true conditions).
5. Use Assura types, not Rust types: Int (not i64), Nat (not usize),
   Bytes (not &[u8]), String (not &str), List<T> (not Vec<T>).
6. After writing each contract, run `assura check <file>` and fix
   any counterexamples before moving to the next function.

Scenario 3: Security Audit with assura audit

You want to scan an existing Rust project for potential vulnerabilities without writing any contracts manually.

3.1 Running a basic audit

From the root of a Cargo workspace:

assura audit .

Output:

Scanning . ... found 47 public functions in 12 files
Generating contracts ... 47 skeleton contracts
Verifying ...

AUDIT SUMMARY: 47 functions, 38 verified, 3 findings, 0 errors

FINDINGS:
  [WARNING] parse_record: ensures  (counterexample)
    Counterexample found
    | offset = 4294967295
    | length = 1

  [WARNING] resize_buffer: ensures  (counterexample)
    Counterexample found
    | new_size = 0

  [INFO] decrypt_block: ensures  (timeout)
    Z3 timed out (needs deeper contract or longer timeout)

The audit generates skeleton contracts with heuristic preconditions (bounds checks on index-like parameters, non-empty checks on collections), runs the full pipeline (parse, resolve, type check, SMT verify), and reports findings.

3.2 Targeting risky code

Scan only functions matching a pattern:

assura audit . --focus "parser::*"

Scan only unsafe functions:

assura audit . --unsafe-only

Limit the number of functions analyzed:

assura audit . --max-functions 20

Use shallow depth (types only, no heuristic contracts):

assura audit . --depth shallow

3.3 Understanding audit findings

Each finding has a severity and a clause type:

A counterexample finding means the SMT solver found specific input values where the heuristic contract is violated. This does not always mean there is a bug; the heuristic contract may be too strict. But it always deserves investigation.

3.4 Using CVE-pattern templates

For deeper analysis, use the CVE-pattern templates to generate contracts targeting specific vulnerability classes. The templates are in templates/cve-patterns.md:

• Buffer overflow (CWE-120, CWE-787): bounds checks on index operations
• Integer overflow (CWE-190, CWE-191): arithmetic wrapping prevention
• Use-after-free (CWE-416): linear resource consumption
• Injection (CWE-89, CWE-79): taint tracking on untrusted input
• Null dereference (CWE-476): Option validation

Feed the template and your Rust function signatures to an AI agent to generate targeted contracts.

3.5 Triage workflow

1. Run assura audit . --format json > audit.json for a machine-readable report.
2. Sort findings by severity: counterexamples first, then timeouts.
3. For each counterexample, check whether the concrete values are reachable in practice. If yes, it is a real bug. If no, the heuristic contract needs refinement.
4. For timeouts, decide whether to increase --timeout, write a more specific manual contract, or accept the risk.
5. Track findings in your issue tracker. Re-run the audit after fixes to confirm resolution.

3.6 JSON output for tooling integration

assura audit . --format json

Output structure:

{
  "functions_scanned": 47,
  "files_scanned": 12,
  "verified": 38,
  "findings": 3,
  "errors": 0,
  "results": [
    {
      "function": "parse_record: ensures",
      "clause": "counterexample",
      "severity": "warning",
      "message": "Counterexample found",
      "counterexample": "offset = 4294967295\nlength = 1"
    },
    {
      "function": "resize_buffer: ensures",
      "clause": "counterexample",
      "severity": "warning",
      "message": "Counterexample found",
      "counterexample": "new_size = 0"
    },
    {
      "function": "decrypt_block: ensures",
      "clause": "timeout",
      "severity": "info",
      "message": "Z3 timed out (needs deeper contract or longer timeout)",
      "counterexample": null
    }
  ]
}

Use jq to extract actionable items:

assura audit . --format json | jq '.results[] | select(.severity == "warning")'

Scenario 4: CI Integration (GitHub Actions)

You want every PR to be verified by Assura before merging.

4.1 Complete workflow file

Create .github/workflows/assura.yml:

name: Assura Verification

on:
  pull_request:
  push:
    branches: [main]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable

      - name: Install Z3
        run: sudo apt-get install -y libz3-dev

      - name: Cache Assura build
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/bin/assura
            ~/.cargo/registry
            ~/.cargo/git
          key: assura-${{ hashFiles('assura-version') }}

      - name: Install Assura
        run: |
          if ! command -v assura &> /dev/null; then
            cargo install assura --locked
          fi

      - name: Format check
        run: |
          for f in contracts/*.assura; do
            assura fmt "$f" --check || {
              echo "::error file=$f::File is not formatted. Run: assura fmt $f"
              exit 1
            }
          done

      - name: Verify contracts (Layer 1, SMT)
        run: |
          for f in contracts/*.assura; do
            echo "Checking $f..."
            assura check "$f" --layer 1 --json > "/tmp/$(basename $f).json" 2>&1
            if [ $? -ne 0 ]; then
              echo "::error file=$f::Contract verification failed"
              cat "/tmp/$(basename $f).json"
              exit 1
            fi
          done

      - name: Build generated Rust
        run: |
          for f in contracts/*.assura; do
            assura build "$f" --output generated --no-check
          done
          cd generated && cargo check

      - name: Upload verification results
        if: always()
        uses: actions/upload-artifact@v4
        with:
          name: assura-results
          path: /tmp/*.json

4.2 Installing Z3 in CI

Z3 is required for Layer 1 (SMT) verification. On Ubuntu runners:

- name: Install Z3
  run: sudo apt-get install -y libz3-dev

On macOS runners:

- name: Install Z3
  run: brew install z3

To pin a specific Z3 version (recommended for reproducibility):

- name: Install Z3 4.13.0
  run: |
    wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-x64-glibc-2.35.zip
    unzip z3-4.13.0-x64-glibc-2.35.zip
    sudo cp z3-4.13.0-x64-glibc-2.35/bin/libz3.so /usr/lib/
    sudo cp z3-4.13.0-x64-glibc-2.35/include/*.h /usr/include/

4.3 Using JSON output for annotations

Parse JSON results to create GitHub annotations:

- name: Verify contracts with annotations
  run: |
    EXIT=0
    for f in contracts/*.assura; do
      OUTPUT=$(assura check "$f" --json 2>&1)
      RC=$?
      if [ $RC -ne 0 ]; then
        EXIT=1
        # Extract error messages from JSON diagnostics
        echo "$OUTPUT" | jq -r '
          .diagnostics[]
          | select(.severity == "error")
          | "::error file=\(.file // "unknown"),line=1::\(.code): \(.message)"
        '
      fi
    done
    exit $EXIT

4.4 Failing PRs on contract violations

The assura check command exits with code 1 when verification fails. This means any step using assura check will fail the CI job automatically. No special configuration is needed.

Exit codes:

• 0: all checks passed
• 1: verification errors (counterexamples, type errors, parse errors)
• 2: file not found, invalid arguments, or other fatal errors

4.5 Verification stats tracking

Capture stats over time to track verification coverage:

- name: Collect verification stats
  run: |
    for f in contracts/*.assura; do
      assura check "$f" --stats 2>&1 | tail -n 12
    done > stats.txt

- name: Upload stats
  uses: actions/upload-artifact@v4
  with:
    name: verification-stats
    path: stats.txt

4.6 Audit as a separate CI job

Run assura audit on PRs that modify Rust source (not just contracts):

  audit:
    runs-on: ubuntu-latest
    if: contains(github.event.pull_request.changed_files, '.rs')
    steps:
      - uses: actions/checkout@v4

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable

      - name: Install Z3
        run: sudo apt-get install -y libz3-dev

      - name: Install Assura
        run: cargo install assura --locked

      - name: Run audit
        run: |
          assura audit . --format json --max-functions 100 > audit.json
          FINDINGS=$(jq '.findings' audit.json)
          if [ "$FINDINGS" -gt 0 ]; then
            echo "::warning::Assura audit found $FINDINGS potential issues"
            jq '.results[] | select(.severity == "warning")' audit.json
          fi

Scenario 5: Team Onboarding and Progressive Adoption

You are introducing Assura to a team that has never used formal verification. This scenario covers the learning progression, common mistakes, and conventions.

5.1 Learning progression

Week 1: Simple contracts. Start with pure functions that have obvious preconditions:

// Level 1: basic precondition
contract SafeDivision {
    input(a: Int, b: Int)
    output(result: Int)

    requires { b != 0 }
    ensures  { result * b + (a mod b) == a }
    effects  { pure }
}

Run assura check and assura explain A05100 to understand counterexamples.

Week 2: Refinement types and multiple clauses. Introduce refined types and combine multiple ensures clauses:

type PositiveInt = { n: Int | n > 0 };

contract Clamp {
    input(value: Int, low: Int, high: Int)
    output(result: Int)

    requires { low <= high }
    ensures  { result >= low }
    ensures  { result <= high }
    ensures  { (value >= low and value <= high) implies result == value }
    effects  { pure }
}

Week 3: Effect tracking. Add effects to contracts for functions with side effects:

contract ReadConfig {
    input(path: String)
    output(result: Map<String, String>)

    requires { path.length() > 0 }
    ensures  { result.length() >= 0 }
    effects  { fs }
}

Week 4: Bind declarations. Start attaching contracts to existing Rust code using bind:

bind "crate::db::get_user" as get_user {
    input(id: Nat)
    output(result: User?)

    requires { id > 0 }
    ensures  { result.is_some() implies result.unwrap().id == id }
    effects  { database.read }
}

Week 5+: Advanced features. Explore quantifiers (forall, exists), typestate, taint tracking, and memory regions. Use the demo files in demos/ as reference implementations.

5.2 “Tests pass but contract finds bug” example

This is the moment that sells Assura to skeptics. Consider this function and its tests:

#![allow(unused)]
fn main() {
// src/math.rs
pub fn percentage(part: u64, total: u64) -> u64 {
    (part * 100) / total
}

// tests/math_test.rs
#[test]
fn test_percentage() {
    assert_eq!(percentage(50, 100), 50);
    assert_eq!(percentage(1, 4), 25);
    assert_eq!(percentage(0, 100), 0);
}
}

All tests pass. But the contract:

bind "crate::math::percentage" as percentage {
    input(part: Nat, total: Nat)
    output(result: Nat)

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

Running assura check:

Error[A05100]: verification failed for percentage: ensures:
               counterexample: part = 101, total = 100

contracts/math.assura: 1 error(s) found

The counterexample reveals: when part > total, the result exceeds 100. The tests never tested this case. The contract caught a real logic gap that 100% test coverage on happy paths would miss.

Fix options:

• Add requires { part <= total } to forbid invalid inputs.
• Change the implementation to std::cmp::min((part * 100) / total, 100).
• Add requires { part <= total } AND ensures { result <= 100 } so both the caller and the implementation are constrained.

5.3 When to write contracts vs tests

Contracts and tests are complementary. Contracts prove universal properties (“for all valid inputs, the output is bounded”). Tests verify specific scenarios (“given this exact input, the output is this exact value”). Use both.

5.4 Common mistakes and how to fix them

Mistake 1: Vacuous contracts. A contract that is always true catches nothing:

# BAD: always true, catches nothing
contract Useless {
    input(x: Int)
    ensures { x == x }
}

Fix: write contracts that constrain behavior. If the ensures clause is a tautology, delete it and write one that describes actual guarantees.

Mistake 2: Wrong Assura types. Using Rust types in contracts:

# BAD: Rust types in contract
contract Wrong {
    input(x: i64, y: usize)
    output(result: Vec<u8>)
}

Fix: use Assura types. i64 is Int, usize is Nat, Vec<u8> is Bytes. See the type mapping table in Scenario 2.

Mistake 3: Missing effect declarations. Forgetting to declare side effects:

# BAD: reads from filesystem but declares pure
contract ReadFile {
    input(path: String)
    output(result: Bytes)
    effects { pure }
}

The type checker rejects this with error A07003 if the bound function performs I/O. Fix: use effects { fs } or effects { io }.

Mistake 4: Overly strict ensures. Writing postconditions that are true for the implementation but impossible to verify:

# BAD: Z3 cannot reason about string formatting
contract FormatDate {
    input(year: Nat, month: Nat, day: Nat)
    output(result: String)
    ensures { result == year.to_string() + "-" + month.to_string() + "-" + day.to_string() }
}

Z3 struggles with string concatenation and formatting. Fix: write verifiable properties instead:

contract FormatDate {
    input(year: Nat, month: Nat, day: Nat)
    output(result: String)

    requires { month >= 1 and month <= 12 }
    requires { day >= 1 and day <= 31 }
    ensures  { result.length() >= 8 }
    ensures  { result.length() <= 10 }
}

Mistake 5: Not running assura explain. When you get an error code, look it up:

assura explain A05100

Output:

A05100: Verification counterexample

The SMT solver found a concrete assignment of values to the contract's
input variables that satisfies the requires clauses but violates at
least one ensures clause.

Example:

  contract Foo {
    input(x: Int)
    ensures { x > 0 }   // <-- no requires constraining x
  }
  // counterexample: x = -1

How to fix:

  Add a requires clause that rules out the counterexample values,
  or weaken the ensures clause if the property is too strong.

5.5 Team conventions

Establish these conventions early:

1. One contract file per Rust module. If your Rust source is src/parser.rs, the contract goes in contracts/parser.assura.

2. Contract names match function names. Use bind "crate::foo::bar" as bar, not as bar_contract or as BarContract.

3. Run assura fmt before committing. Like rustfmt for Rust, assura fmt normalizes whitespace and indentation. Use assura fmt --check in CI to enforce formatting.

4. Start with requires, then ensures, then effects. Consistent clause ordering makes contracts scannable:

   bind "..." as name {
       input(...)
       output(...)
       requires { ... }
       ensures  { ... }
       effects  { ... }
   }
   

5. Commit contracts alongside code changes. If a PR changes a function’s behavior, the contract must be updated in the same PR.

6. Use assura check --json in code review tools. Pipe JSON output into your review bot or CI annotations so reviewers see verification results inline.

7. Do not ignore counterexamples. Every counterexample is either a real bug or a contract that needs refinement. Both are valuable. Never suppress a counterexample without understanding it.

Assura for AI agents

Assura is built so agents can propose implementations and the compiler can accept or reject them with structured evidence.

Install

cargo install assura --locked
assura --help

Docs site: https://assura-lang.github.io/assura/

Core loop

1. Human (or agent) writes or edits a .assura contract.
2. Agent produces an implementation path (synthesized IR, co-located .ir, or Rust under check-rust).
3. Agent runs assura check / assura check-rust / assura build.
4. Agent reads machine-readable results and iterates on counterexamples, not on vibes.

assura check path/to/file.assura --json
assura check-rust src/ --json

Acceptance policy (LLM IR / auto-implement)

Do not require every clause status == "verified". Many clauses return Unknown because a feature is not yet encoded in SMT. For agent IR:

• Reject if any Counterexample appears.
• Accept when there is no counterexample (Unknown is allowed for unmodeled features). Generated Rust may still carry runtime assertions from requires/ensures codegen.

See AGENTS.md pipeline notes for verify_ir and multi-contract source pitfalls (first contract only unless single-contract source is synthesized).

Vacuous success

JSON success can still be vacuous (no contracts, or no SMT proof obligations). Inspect file_info.vacuous / vacuous_reason (and human summaries that say “no SMT proof obligations”). Do not report that as full coverage.

MCP

The assura-mcp crate exposes tools for agent hosts (rmcp). From a workspace build:

cargo run -p assura-mcp -- --help

Exact tool names evolve; list tools from your MCP client after connecting. Prefer assura check --json when MCP is unavailable.

Suggested agent checklist

1. Prefer showcase demos over *-audit.assura (many audits are EXPECT FAIL).
2. On failure, paste the clause description and model into the next edit.
3. Use --layer 0 for fast structural iteration when SMT is noisy.
4. Read What we prove before claiming “proved secure”.

Related

• Getting started
• Compared to other tools
• Case studies
• Preferred URLs

Compared to other tools

Assura is a contract-first language aimed at AI-assisted development: humans write behavioral contracts; the compiler proves implementations (or returns a counterexample) with SMT (Z3/CVC5) and emits Rust.

This page answers the first question PL and Rust audiences ask: is this just Dafny / Verus / Liquid Haskell / better unit tests?

Snapshot

When Assura is a better fit

• You want specs separate from host-language syntax so agents and humans share a stable contract surface.
• You care about an AI write → SMT check → fix loop with structured results (counterexample vs unknown vs verified).
• You want Rust as the ship format without requiring the implementation to be authored as verified Rust-in-place first.

When another tool is a better fit

Honesty constraints

Assura does not claim:

• That every clause is always decided (see What we prove).
• That it replaces human review for product requirements.
• That it is a drop-in Verus substitute for verifying arbitrary Rust crates.

For competitive research notes (internal depth), see INVESTIGATION.md. For a short public pitch, start with the docs site introduction.

What we prove

Assura uses layered checking. Not every green assura check means “mathematically proved forever for every feature.” This page is the honest map for security and formal-methods readers.

Result kinds (SMT)

Known SMT limitation (warning, not hard fail)

When the reason includes the marker not yet encoded in SMT, the CLI treats the result as a warning (exit 0 by default). That means the compiler intentionally skipped modeling a feature, not that the clause was proved.

Other Unknown reasons (non-linear arithmetic, genuine solver unknown) are treated more severely. See FAQ: “Unknown” verification result.

Layers

Default config values are short (often 1s at the options layer). Layer 1 clause solvers floor at 10 seconds so multi-clause demos are not starved; set [verify] timeout = 30000 (or higher) when you need more. See FAQ: Z3 timeout on a contract.

What is not automatically proved

• Features that still return Unknown with the known-limitation marker
• Host code outside Assura contracts / IR / check-rust body modeling
• Absolute absence of all security bugs (only the properties you state and that the solver models)
• Correctness of the SMT solvers themselves or of rustc

Vacuous success

An empty file or a contract with no SMT proof obligations can still report check success with no type errors. Human and JSON output call this out (vacuous / “no SMT proof obligations”). Agents must not treat that as coverage of ensures/invariants.

AI-generated implementations

For auto-implement / IR injection, acceptance is typically no Counterexample, not “every clause is Verified”. Unknown from unmodeled features is common; runtime assertions from codegen still apply.

Related

• FAQ — timeouts, counterexamples, Unknown
• Compared to other tools
• Preferred URLs

SMT and portfolio design notes

Technical note for readers who care about solver encoding and result policy, not AI marketing. Companion to What we prove and Compiler Internals.

Dual solvers, one policy brain

Assura can run Z3 (default) and CVC5 (portfolio / optional native). Encoding and clause gates live in shared policy modules under assura-smt (portfolio_policy, clause_gate_policy, encode_timeout_policy, …). Backends build solver terms; they should not redefine merge order or limitation strings.

Portfolio merge priority

When both solvers report a result for the same clause, merge prefers:

1. Verified
2. Counterexample
3. Unknown
4. Timeout

On equal priority, Z3 wins (richer models / unsat cores in practice). See merge_portfolio_results / portfolio_result_priority in crates/assura-smt/src/policy/portfolio_policy.rs.

Shared timeout floor

Config defaults for verify can be short (historically ~1s at the options layer). Per-clause solving floors at 10_000 ms so multi-clause demos are not starved:

Raising [verify] timeout (or CLI equivalent) above the floor passes through. Source: crates/assura-smt/src/policy/encode_timeout_policy.rs (issues #1383 / #1384).

Unknown is not one thing

Helpers: VerificationResult::unknown_not_encoded, KNOWN_SMT_LIMITATION_MARKER, is_known_smt_limitation. Do not invent alternate marker wording in new code paths.

IR bodies and unconstrained results

Without an implementation body (IR sidecar, synthesis, or check-rust encode), result (and other outputs) may be free variables. Ensures that only constrain unconstrained outputs can produce Counterexample even when the requires look fine. Mitigations:

• Co-located {ContractName}.ir
• In-memory synthesis for common result == … shapes
• assura check-rust body encoding where modeled
• Writing ensures as consequences of requires on inputs only (demo style)

Vacuous files (no SMT obligations) can still “pass” type-check; JSON exposes vacuous / “no SMT proof obligations”. Agents must not treat that as proof coverage.

AI-generated IR acceptance

For auto-implement / LLM IR injection, acceptance is typically no Counterexample, not “every clause Verified.” Unknown from unmodeled features is common; codegen still emits runtime assertions for requires/ensures where applicable.

What this is not

• A claim that Z3/CVC5 themselves are proved correct
• A claim that every Assura feature is fully encoded
• A Verus-style proof of arbitrary existing Rust

Further reading

• WHAT-WE-PROVE.md — user-facing result kinds and layers
• COMPARE.md — Assura vs Dafny / Verus / tests
• INTERNALS.md — crate and module map
• SPECIFICATION.md — language and verification layers
• Launch / outreach drafts under launch/

Preferred public URLs

Use these canonical URLs when linking to Assura (blog posts, Show HN, social, agent prompts). Do not use https://assura.dev for this project.

Install paths today: crates.io (cargo install assura --locked) or cargo-dist shell installer on Releases. No Homebrew formula is published (installers = ["shell"] only).

Brand notes

• Assura here is the contract-first language under the assura-lang GitHub organization.
• assura.dev is a different product (structure validation for developer onboarding). It is not affiliated with this language.
• Social handles for the language should use a distinctive form such as assuralang / assura-lang to avoid collisions with insurance and other brands that use the word “Assura”.

Domain policy

Until a custom domain is acquired and pointed at the docs site, the public homepage is the GitHub Pages mdBook URL above. If a domain is added later, redirect it to the same content and update this page, the repo homepage setting, and the org website field in one pass.

Troubleshooting and FAQ

Installation

Install the Assura CLI

Preferred (crates.io):

cargo install assura --locked

Requires a Rust toolchain (edition 2024 / rustc 1.85+). Also available as prebuilt binaries from GitHub Releases (cargo-dist).

From a monorepo clone or git:

cargo install --path crates/assura-cli --locked
# or:
cargo install --git https://github.com/assura-lang/assura assura --locked

More detail: README Quick Start, Tutorial installation, and CRATES-IO.md (what co-publishes, and embedding assura-pipeline from crates.io).

After install, confirm the binary:

assura --version
assura doctor

Z3 is not found

Symptom: assura check prints “Z3 is required for SMT verification” or verification results are all Timeout.

Fix:

# macOS
brew install z3

# Ubuntu/Debian
sudo apt-get install -y libz3-dev

# Verify
z3 --version
assura doctor

If Z3 is installed but not found, check that the z3 binary is on your $PATH. On Linux, you may also need libz3.so in the library path:

export LD_LIBRARY_PATH=/usr/lib/x86_64-linux-gnu:$LD_LIBRARY_PATH

Rust toolchain version

Assura requires Rust edition 2024 (rustc 1.85+). Check with:

rustc --version
rustup update stable

Verification

Solver timeout on a contract

Symptom: Verification result says Timeout instead of Verified or Counterexample.

Causes and fixes:

1. Complex quantifiers. Quantifiers (forall, exists) with nested data structures are expensive. Simplify the quantifier body or add trigger annotations.

2. Large numeric ranges. Constraints like forall x: Int, 0 <= x && x < 1000000 enumerate a huge space. Use tighter bounds or refinement types.

3. Increase the timeout. VerifyOptions / assura.toml default to 1000 ms, but Layer 1 clause solvers floor at 10 seconds so short defaults do not starve multi-clause demos. Set a higher value (e.g. 30000 or 60000) when you need more than the floor:

   [verify]
   timeout = 30000
   

   The same budget applies to Z3 and CVC5 (shell and native), and to portfolio mode: Z3 uses the solver timeout option; CVC5 uses tlimit / --tlimit with the same floor/resolve helper. Layer 2 advanced passes use the configured value without that floor.

4. Use Layer 0 first. Structural checks (Layer 0) are instant and catch type errors, undefined names, and effect violations without invoking Z3:

   assura check file.assura --layer 0
   

5. Try portfolio mode. CVC5 may handle the query faster:

   assura check file.assura --solver portfolio
   

Understanding counterexamples

Symptom: Z3 returns a Counterexample but the values look strange.

A counterexample is a concrete set of inputs that violates a contract clause. For example:

Counterexample for SafeDivision ensures clause:
  a = -2147483648
  b = -1

This means signed integer division of INT_MIN / -1 overflows. The fix is to add a precondition:

requires { !(a == min_int() && b == -1) }

Tips for reading counterexamples:

• Z3 picks adversarial edge cases: 0, -1, MAX_INT, MIN_INT, empty collections.
• If the counterexample involves very large numbers, your contract may be missing overflow guards.
• If the values look random, the contract clause may be too weak to constrain the search space.

“Unknown” verification result

Full honesty map: What we prove.

Unknown means the solver could not decide the obligation. Reasons include timeouts, incomplete models, and known SMT limitations (reason contains not yet encoded in SMT). The CLI treats that known limitation marker as a warning (exit 0), not a hard verification failure. Other Unknown reasons are more severe.

This is different from Timeout (budget exceeded) and from Counterexample (definite failure with a model).

Common causes of inconclusive results:

• Non-linear arithmetic (multiplication of two variables)
• Recursive functions without decreases clauses
• Mixing bitvector and integer theories

Fix: simplify the contract or add auxiliary lemmas.

Verification passes but generated code fails cargo check

The contract is verified but the generated Rust code does not compile. This usually means:

1. Missing type import. The generated code references a type that is not in scope. Add it to the contract’s context.

2. Generic type mismatch. The contract uses Int but the Rust function expects a specific integer type like i32. The codegen maps Int to i64 by default.

3. Generated project structure. Check the generated/ directory. It should be a valid Cargo workspace. Run cargo check inside it to see the exact error.

Type Errors

A03001: type mismatch

The most common error. An expression has type X but the context expects type Y. Also used for empty tuple types such as (,), (Int,,Bool), nested List<(,)> / Map<String, (,)>, type aliases (type Bad = (,) or type Bad = List<(,)>), refined bases (type Bad = { x: (,) | true }), enum payloads (enum E { Bad((,)) }), and empty tuple params or returns on fn / service (use () for Unit, or (T,) for a 1-tuple). Pair tuples and generics work in enum payloads and params: enum E { Box(List<Int>), Pair((Int, Bool)) }, fn f(t: (Int, Bool)). Match arms must use the right field count: Pair(x, y) is valid; Pair(x) is A03001.

Error A03001: type mismatch
  expected Bool, found Int
  --> contracts/lib.assura:5:15

Fix: Check that the requires/ensures clause body evaluates to Bool. Arithmetic expressions like x + 1 are Int, not Bool. Use comparisons: x + 1 > 0.

A03005: unknown field or method

Error A03005: unknown field `len` on type List<Int>

In Assura contracts, use length(xs) instead of xs.len(). The contract language uses mathematical functions, not Rust methods.

A03006: clause body not Bool

Error A03006: requires clause must be Bool, found Int

requires / ensures / invariant clause bodies must be boolean predicates. Use comparisons (x > 0) or logical operators, not bare arithmetic (x + 1). (Arity mismatches on function calls use A03002.)

Effect Errors

A07001: undeclared effect

Error A07001: undeclared effect `io` in pure function

The function body uses an effect that is not in the effects clause. Either add the effect:

effects { io }

Or mark the function as pure only if it truly has no side effects.

A07003: unknown effect name

Error A07003: unknown effect name `memory`

Use one of the built-in effect names:

Groups: io, database, logging

Leaf effects: console.read, console.write, filesystem.read, filesystem.write, network.connect, network.send, network.receive, time.read, random, database.read, database.write, log.debug, log.info, log.warn, log.error

Short aliases: mem, net, fs, rng, time, alloc, diverge

Custom sub-effects like io.custom are accepted if the group (io) is known.

Name Resolution Errors

A02001: undefined symbol

Error A02001: undefined symbol `result`
  --> contracts/lib.assura:7:15

result is only available inside ensures clauses. In requires clauses, you can only reference input parameters.

Similarly, old(x) is only valid in ensures clauses.

CLI

assura check vs assura build

• check runs the full verification pipeline (parse, resolve, type-check, SMT) and reports results. Does not generate code.
• build does everything check does, plus generates a Rust project in generated/ and runs cargo check on it.

Use check during development. Use build when you are ready to integrate the generated code.

assura infer output is incomplete

assura infer generates skeleton bind declarations from Rust source files. It extracts public function signatures but cannot infer meaningful preconditions and postconditions.

The output is a starting point. You must fill in the requires and ensures clauses based on the function’s intended behavior.

assura audit is slow

assura audit generates contracts for every public function and verifies them all. For large projects:

# Focus on specific modules
assura audit . --focus "parser::*"

# Limit function count
assura audit . --max-functions 20

# Reduce timeout per function
assura audit . --timeout 2000

# Only audit unsafe functions
assura audit . --unsafe-only

Watch mode does not detect changes

assura check file.assura --watch uses filesystem notifications. If changes are not detected:

1. Save the file explicitly (some editors delay writes).
2. Check that the file path matches exactly (watch tracks the specific file, not the directory).
3. On Linux, check inotify limits:

   cat /proc/sys/fs/inotify/max_user_watches
   # Increase if needed
   echo 524288 | sudo tee /proc/sys/fs/inotify/max_user_watches
   

Editor Integration

VS Code: LSP not starting

1. Install the Assura extension from the editors/vscode/ directory.
2. Set the server path in settings:

   {
     "assura.serverPath": "/path/to/assura-lsp"
   }
   

3. Build the LSP server:

   cargo build --bin assura-lsp
   

4. Restart VS Code.

The LSP provides diagnostics, go-to-definition, hover, completions, formatting, find references, and rename.

VS Code: no syntax highlighting

The TextMate grammar in editors/vscode/syntaxes/assura.tmLanguage.json provides basic highlighting. If colors are missing:

1. Reload the extension: Ctrl+Shift+P > “Developer: Reload Window”
2. Check that .assura files are recognized: look for “Assura” in the bottom-right language selector.

Project Configuration

assura.toml options

[package]
name = "my-project"
version = "0.1.0"

[build]
output = "generated"
target = "native"    # or "wasm"

[verify]
timeout = 5000
layer = 255          # 0=structural, 1=SMT, 255=all
solver = "z3"        # "z3", "cvc5", or "portfolio"

[profile]
parallel = true
cache = true

Creating a new project

assura init my-project
cd my-project
assura check contracts/lib.assura

This creates assura.toml and a starter contract in contracts/.

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

Assura Language Specification v0.1

Implementer’s reference. Every section is designed so an engineer can build the corresponding compiler component without ambiguity.

Verification Scope

Assura verifies safety and liveness properties of single-node programs under all Rust memory orderings (SeqCst, AcqRel, Relaxed).

Safety (Layer 0-2): preconditions, postconditions, invariants, frame conditions, structural invariants. Decidable or bounded SMT.

Liveness (Layer 2-3): bounded model checking with k-induction. Properties like “eventually a leader is elected” are verified up to a configurable step bound K, with optional unbounded proof via k-induction.

Concurrency (Layer 1-2): per-thread views for weak memory ordering, prophecy variables for linearizability proofs. These extend the verification beyond what Dafny, F*, or SPARK offer.

Table of Contents

• 1. Contract Language Grammar
• 2. Type System
• 3. Effect System
• 4. Implementation IR Format
• 5. Verification Architecture
• 6. Rust Codegen Mapping
• 7. Error Code Catalog
• 8. Module System
• 9. Standard Library
• 10. CLI Interface
• 11. AI Agent API
• 12. Decidability Boundaries
• 13. Type Interaction Test Cases
• 14. Verification Categories
  • 14.CORE: Verification Infrastructure
  • 14.MEM: Memory Safety
  • 14.TYPE: Types and Contracts
  • 14.SEC: Trust and Security
  • 14.CONC: Concurrency
  • 14.STOR: Storage and Durability
  • 14.FMT: Data Formats and Parsing
  • 14.NUM: Numerical and Precision
  • 14.PLAT: Platform and Configuration
  • 14.PERF: Performance
  • 14.TEST: Testing and Verification Workflow
  • 14.MISC: Specialized

1. Contract Language Grammar

The contract language is what humans write. It is declarative, readable, and complete. The grammar below is in EBNF notation. Terminals are in 'quotes' or UPPER_CASE. Non-terminals are in PascalCase.

1.2 Project Profile

A project declares which verification categories are active. Features in excluded categories are ignored by the parser and skipped by the verifier.

project stb_image_rs {
  profile: [core, mem, sec, fmt, num, type, test]
}

CORE is always included and cannot be excluded.

Preset Profiles

Custom profiles list categories explicitly. Adding a category mid-project is always safe (additive).

1.1 Lexical Grammar

(* Identifiers *)
Ident          = Letter (Letter | Digit | '_')* ;
TypeIdent      = UpperLetter (Letter | Digit | '_')* ;
FieldIdent     = LowerLetter (Letter | Digit | '_')* ;
EffectIdent    = LowerLetter (Letter | Digit | '.' | '_')* ;

(* Literals *)
IntLit         = ['-'] Digit+ ['_' Digit+]* ;
FloatLit       = ['-'] Digit+ '.' Digit+ ;
StringLit      = '"' { StringChar } '"' ;
BoolLit        = 'true' | 'false' ;

(* Comments *)
LineComment    = '//' { any except newline } ;
BlockComment   = '/*' { any } '*/' ;

(* Keywords *)
Keyword        = 'service' | 'contract' | 'type' | 'enum' | 'states'
               | 'transition' | 'operation' | 'query' | 'input'
               | 'output' | 'errors' | 'requires' | 'ensures'
               | 'invariant' | 'effects' | 'must-not' | 'rule'
               | 'data-flow' | 'extern' | 'bind' | 'import'
               | 'module' | 'pub' | 'where' | 'forall' | 'exists'
               | 'in' | 'not' | 'and' | 'or' | 'if' | 'then'
               | 'else' | 'old' | 'result' | 'self'
               | 'concurrency' | 'privacy' | 'retention' | 'audit'
               | 'evolution' | 'transaction' | 'serialization'
               | 'api_compat' | 'performance' | 'protocol'
               | 'observe' | 'compliance' | 'ordering'
               | 'idempotent' ;

1.2 Top-Level Declarations

SourceFile     = ModuleDecl? { ImportDecl } { TopDecl } ;

ModuleDecl     = 'module' QualifiedName ';' ;

ImportDecl     = 'import' QualifiedName ['as' Ident]
                 ['{' ImportList '}'] ';' ;
ImportList     = Ident { ',' Ident } ;

QualifiedName  = Ident { '.' Ident } ;

TopDecl        = ServiceDecl
               | ContractDecl
               | TypeDecl
               | EnumDecl
               | ExternDecl
               | BindDecl
               | ComplianceDecl
               | ProtocolDecl ;

1.3 Service Declarations

ServiceDecl    = 'service' TypeIdent '{'
                   { ServiceItem }
                 '}' ;

ServiceItem    = TypeDecl
               | EnumDecl
               | StateDecl
               | TransitionDecl
               | OperationDecl
               | QueryDecl
               | InvariantDecl
               | ConcurrencyDecl
               | PrivacyDecl
               | RetentionDecl
               | AuditDecl
               | EvolutionDecl
               | TransactionDecl
               | SerializationDecl
               | ApiCompatDecl
               | PerformanceDecl
               | ProtocolDecl
               | ObserveDecl
               | ComplianceDecl
               | OrderingDecl
               | IdempotencyDecl ;

1.4 Type Declarations

TypeDecl       = 'type' TypeIdent [TypeParams] ['=' TypeExpr]
                 ['{' { FieldDecl } '}']
                 [WhereClause] ;

TypeParams     = '<' TypeParam { ',' TypeParam } '>' ;
TypeParam      = TypeIdent [':' KindExpr] ;

FieldDecl      = [Visibility] FieldIdent ':' TypeExpr
                 [FieldConstraint] ';' ;

Visibility     = 'pub' ;

FieldConstraint = 'where' Predicate ;

(* Types *)
TypeExpr       = BaseType
               | RefinedType
               | FunctionType
               | GenericType
               | TupleType
               | OptionType
               | ListType
               | MapType
               | SetType ;

BaseType       = TypeIdent [TypeArgs]
               | BuiltinType ;

BuiltinType    = 'Int' | 'Nat' | 'Float' | 'Bool' | 'String'
               | 'Bytes' | 'Unit' | 'Never' ;

RefinedType    = '{' Ident ':' TypeExpr '|' Predicate '}' ;

FunctionType   = '(' [ParamList] ')' '->' EffectRow TypeExpr ;

GenericType    = TypeIdent '<' TypeExpr { ',' TypeExpr } '>' ;

TupleType      = '(' TypeExpr ',' TypeExpr { ',' TypeExpr } ')' ;
OptionType     = TypeExpr '?' ;
ListType       = 'List' '<' TypeExpr '>' ;
MapType        = 'Map' '<' TypeExpr ',' TypeExpr '>' ;
SetType        = 'Set' '<' TypeExpr '>' ;

TypeArgs       = '<' TypeExpr { ',' TypeExpr } '>' ;

1.5 Enum and State Declarations

EnumDecl       = 'enum' TypeIdent [TypeParams] '{'
                   EnumVariant { ',' EnumVariant } [',']
                 '}' ;
EnumVariant    = TypeIdent ['(' TypeExpr { ',' TypeExpr } ')'] ;

StateDecl      = 'states' ':' StateIdent { '->' StateIdent } ;
StateIdent     = TypeIdent ;

TransitionDecl = 'transition' StateIdent
                 ['requires' ':' Predicate]
                 ';' ;

1.6 Operations and Queries

OperationDecl  = 'operation' TypeIdent '{'
                   { OperationItem }
                 '}' ;

QueryDecl      = 'query' TypeIdent '{'
                   { OperationItem }
                 '}' ;

OperationItem  = InputDecl
               | OutputDecl
               | ErrorsDecl
               | RequiresClause
               | EnsuresClause
               | EffectsClause
               | MustNotClause
               | RuleClause
               | DataFlowClause ;

InputDecl      = 'input' ':' '{' { FieldDecl } '}' ;
               | 'input' '(' ParamList ')' ;

OutputDecl     = 'output' ':' '{' { FieldDecl } '}' ;
               | 'output' '(' ParamList ')' ;

ErrorsDecl     = 'errors' ':' '[' TypeExpr { ',' TypeExpr } ']' ;

ParamList      = Param { ',' Param } ;
Param          = Ident ':' TypeExpr ;

1.7 Contract Clauses

ContractDecl   = 'contract' TypeIdent [TypeParams] '{'
                   { ContractItem }
                 '}' ;

ContractItem   = InputDecl | OutputDecl | RequiresClause
               | EnsuresClause | EffectsClause | InvariantDecl ;

RequiresClause = 'requires' ['{'] Predicate ['}'] ;
               | 'requires' ':' Predicate ;

EnsuresClause  = 'ensures' ['{'] Predicate ['}'] ;
               | 'ensures' ':' Predicate ;

InvariantDecl  = 'invariant' ['{'] Predicate ['}'] ;
               | 'invariant' ':' Predicate ;

EffectsClause  = 'effects' ':' EffectList ;
               | 'effects' ['{'] EffectList ['}'] ;

MustNotClause  = 'must-not' ':' EffectList ;

EffectList     = EffectIdent { ',' EffectIdent } ;

RuleClause     = 'rule' ':' Predicate ;

DataFlowClause = 'data-flow' ':' Expr 'must-not-appear-in'
                 Ident { ',' Ident } ;

1.8 Predicates and Expressions

Predicate      = PredAtom
               | Predicate 'and' Predicate
               | Predicate 'or' Predicate
               | 'not' Predicate
               | Predicate '=>' Predicate        (* implication *)
               | Quantifier
               | '(' Predicate ')'
               | 'if' Predicate 'then' Predicate
                 ['else' Predicate] ;

PredAtom       = Expr RelOp Expr
               | Expr 'in' Expr
               | Expr 'not' 'in' Expr
               | Expr 'is' TypeIdent
               | Expr                             (* boolean expr *) ;

Quantifier     = 'forall' Ident 'in' Expr ':' Predicate
               | 'exists' Ident 'in' Expr ':' Predicate ;

RelOp          = '==' | '!=' | '<' | '<=' | '>' | '>=' ;

Expr           = Literal
               | Ident
               | 'self'
               | 'result'
               | 'old' '(' Expr ')'
               | Expr '.' Ident
               | Expr '.' Ident '(' [ArgList] ')'
               | Expr BinOp Expr
               | UnaryOp Expr
               | Expr '[' Expr ']'
               | '|' Expr '|'                    (* absolute value *)
               | '(' Expr ')'
               | 'if' Expr 'then' Expr 'else' Expr
               | ListExpr
               | SetExpr
               | MapExpr ;

BinOp          = '+' | '-' | '*' | '/' | '%' | '++' ;
UnaryOp        = '-' | 'not' ;

ArgList        = Expr { ',' Expr } ;
Literal        = IntLit | FloatLit | StringLit | BoolLit ;

ListExpr       = '[' [Expr { ',' Expr }] ']' ;
SetExpr        = '{' Expr { ',' Expr } '}' ;
MapExpr        = '{' [MapEntry { ',' MapEntry }] '}' ;
MapEntry       = Expr ':' Expr ;

1.9 Extended Contract Layers (8-27)

(* Layer 8: Concurrency *)
ConcurrencyDecl = 'concurrency' ':' TypeIdent 'is'
                  ConcurrencyMode ;
ConcurrencyMode = 'exclusive' | 'shared-read' | 'actor-isolated' ;

(* Layer 9: Numerical Precision -- expressed via type aliases *)
(* e.g., type Money = FixedDecimal<2, USD> *)

(* Layer 10: Temporal Ordering *)
OrderingDecl   = 'ordering' ':' TypeIdent 'must' 'be' 'processed'
                 'in' OrderingMode ;
OrderingMode   = 'chronological' 'order'
               | 'reverse' 'chronological' 'order'
               | 'dependency' 'order' ;

(* Layer 11: Idempotency *)
IdempotencyDecl = 'idempotent' ':' TypeIdent 'consumes'
                  TypeIdent '(' LinearityMode ')' ;
LinearityMode  = 'linear' | 'affine' ;

(* Layer 12: Privacy *)
PrivacyDecl    = 'privacy' ':' Expr 'purpose' '{' PurposeList '}' ;
PurposeList    = Ident { ',' Ident } ;

RetentionDecl  = 'retention' ':' Ident 'retain' Duration
                 'then' RetentionAction ;
Duration       = IntLit '_' TimeUnit ;
TimeUnit       = 'days' | 'months' | 'years' ;
RetentionAction = 'delete' | 'archive' | 'anonymize' ;

(* Layer 13: Schema Evolution *)
EvolutionDecl  = 'evolution' ':' TypeIdent 'v' IntLit
                 EvolutionAction ;
EvolutionAction = 'adds' 'field' FieldDecl
               | 'removes' 'field' Ident
               | 'renames' 'field' Ident 'to' Ident
               | 'changes' 'field' Ident 'from' TypeExpr 'to'
                 TypeExpr ['default' Expr] ;

(* Layer 14: Crash Safety *)
TransactionDecl = 'transaction' ':' TypeIdent '{'
                    { CrashHandler }
                  '}' ;
CrashHandler   = 'on_crash' ':' CrashAction ;
CrashAction    = 'rollback' Expr
               | 'mark' Expr 'as' TypeIdent
               | 'compensate' Expr ;

(* Layer 15: Audit *)
AuditDecl      = 'audit' ':' AuditRule ;
AuditRule      = 'every' 'mutation' 'to' TypeIdent
                 'requires' TypeIdent [AuditConstraint]
               | Ident 'requires' TypeIdent [AuditConstraint] ;
AuditConstraint = 'with' Predicate ;

(* Layer 16: Serialization *)
SerializationDecl = 'serialization' ':' TypeIdent
                    SerializationGuarantee ;
SerializationGuarantee = 'roundtrip' 'guarantee'
                       | 'backward' 'compatible'
                       | 'forward' 'compatible' ;

(* Layer 17: API Evolution *)
ApiCompatDecl  = 'api_compat' ':' 'v' IntLit 'of' TypeIdent
                 ApiCompatRule ;
ApiCompatRule  = 'may' 'add' ApiTarget
               | 'may' 'not' 'remove' ApiTarget
               | 'may' 'not' 'add' 'required' ApiTarget ;
ApiTarget      = 'response' 'fields'
               | 'request' 'fields'
               | 'error' 'variants' ;

(* Layer 18: Performance *)
PerformanceDecl = 'performance' ':' TypeIdent 'is'
                  ComplexityBound 'in' Ident ;
ComplexityBound = 'O' '(' ComplexityExpr ')' ;
ComplexityExpr = '1' | 'n' | 'n' '^' IntLit
               | 'log' 'n' | 'n' 'log' 'n' ;

(* Layer 19: Multi-Service Protocol *)
ProtocolDecl   = 'protocol' TypeIdent '{'
                   { ProtocolStep }
                 '}' ;
ProtocolStep   = TypeIdent '->' TypeIdent ':' TypeIdent
                 ['|' TypeIdent] ;

(* Layer 20: Observability *)
ObserveDecl    = 'observe' ':' ObserveRule ;
ObserveRule    = 'every' 'operation' 'emits' ObserveTarget
                 ['with' Ident]
               | TypeIdent 'emits' ObserveTarget ;
ObserveTarget  = 'trace_span' | 'metric' Ident | 'log' Ident ;

(* Layer 21: Regulatory Compliance *)
ComplianceDecl = 'compliance' TypeIdent '{'
                   { ComplianceRule }
                 '}' ;
ComplianceRule = 'rule' ':' Predicate ;

1.10 Extern and Bind Declarations

ExternDecl     = 'extern' 'fn' Ident '(' [ParamList] ')'
                 '->' TypeExpr
                 { ExternClause } ;

ExternClause   = RequiresClause | EnsuresClause | EffectsClause ;

BindDecl       = 'bind' StringLit 'as' Ident '{'
                   { BindItem }
                 '}' ;

BindItem       = InputDecl | OutputDecl | RequiresClause
               | EnsuresClause | EffectsClause ;

1.11 Where Clauses and Kind Expressions

WhereClause    = 'where' WhereItem { ',' WhereItem } ;
WhereItem      = TypeParam ':' KindExpr
               | Predicate ;

KindExpr       = 'Type'
               | 'Nat'
               | 'Effect'
               | 'Label'
               | KindExpr '->' KindExpr ;

1.12 Effect Rows (used in function types)

EffectRow      = '<' [EffectElem { ',' EffectElem }
                 ['|' EffectVar]] '>'
               | 'pure'
               | EffectVar ;

EffectElem     = EffectIdent ['<' TypeArgs '>'] ;
EffectVar      = LowerLetter Ident? ;

2. Type System

Assura’s type system combines six features into a unified framework. Each feature is proven in isolation by prior work; the contribution is their composition. The core calculus is based on Quantitative Type Theory (QTT, Idris 2) extended with refinement predicates (Liquid Haskell), effect rows (Koka), information flow labels (Jif/FlowCaml), and typestate (Plaid).

2.1 Universes and Kinds

Kind ::= Type              -- the kind of value types
       | Nat               -- natural number indices
       | Effect            -- effect rows
       | Label             -- security labels
       | Kind -> Kind      -- higher-order kinds

All types live in Type. Natural number indices (Nat) are used for dependent typing (vector lengths, matrix dimensions). Effect is the kind of effect rows. Label is the kind of security labels.

2.2 Core Judgment Forms

The central typing judgment is:

Gamma; Delta; Sigma |- e : T ! E

Where:

• Gamma = unrestricted context (types, constants, type aliases)
• Delta = graded linear context (variables with usage grades)
• Sigma = typestate context (variables with current state)
• e = expression
• T = type (possibly refined)
• E = effect row

Graded Linear Context (Delta)

Each entry in Delta has the form x :_{r} T where r is a grade from the semiring (N+, 0, 1, +, *) extended with omega (unlimited):

Grade ::= 0         -- erased (compile-time only)
        | 1         -- linear (use exactly once)
        | n         -- exact count (use exactly n times)
        | omega     -- unrestricted (use any number of times)

Grades compose:

• Parallel use: r + s (both branches of a pair use x)
• Sequential use: r * s (f uses x r times, applied to g that uses x s times)
• Subgrading: 0 <= 1 <= omega (a linear variable can be treated as unrestricted is NOT allowed; the reverse is)

Typestate Context (Sigma)

Each entry in Sigma has the form x @ S where S is the current state of x from a declared state machine:

Sigma = { x1 @ S1, x2 @ S2, ... }

Operations on x update its state in Sigma. The type checker rejects any operation that is not valid for the current state.

2.3 Refinement Types

A refined type {v : T | P} pairs a base type T with a predicate P over the value v. The predicate is a term in the decidable fragment of first-order logic (QF_UFLIA: quantifier-free uninterpreted functions + linear integer arithmetic).

Subtyping Rule

Gamma |- {v:S | P} <: {v:T | Q}
  if  S <: T
  and Gamma, v:T, P |- Q    (checked by SMT: P => Q is valid)

Refinement subtyping reduces to SMT validity checking. The solver receives P => Q and must prove it valid (return unsat for P and not Q).

Built-in Refinement Aliases

type Nat       = {v: Int  | v >= 0}
type Pos       = {v: Int  | v > 0}
type NonEmpty<T> = {v: List<T> | len(v) > 0}
type Btwn<Lo, Hi> = {v: Int | Lo <= v and v < Hi}
type Percentage = {v: Float | 0.0 <= v and v <= 1.0}

Measures

Measures bridge data structures into the logic. They are structurally recursive functions lifted into the refinement language:

measure len : List<T> -> Nat
  len([])     = 0
  len(_ :: t) = 1 + len(t)

measure elems : List<T> -> Set<T>
  elems([])      = {}
  elems(x :: xs) = {x} ++ elems(xs)

Measures appear as uninterpreted functions in SMT with axioms generated from their definitions.

2.4 Dependent Types

Types may depend on values. The dependent function type (Pi type) is:

(x : A) -> B    where B may mention x

Assura supports a restricted form of dependent types: types may depend on values of kind Nat, Bool, and finite enums. Full value-level dependency (arbitrary terms in types) is deferred to v2.

Examples

type Vec<T, n: Nat> = ...

fn head(v: Vec<T, n>) -> T
  where n > 0

fn append(a: Vec<T, n>, b: Vec<T, m>) -> Vec<T, n + m>

fn replicate(x: T, n: Nat) -> Vec<T, n>

Index Erasure

All Nat-kinded indices are erased at runtime. They exist only for type checking. The generated Rust code has no runtime representation of type indices.

2.5 Linear and Graded Types

Following Granule and Idris 2’s QTT, every binding carries a usage grade:

fn use_once(conn :_1 DbConnection) -> Result
  -- conn must be used exactly once

fn use_twice(val :_2 Token) -> (Token, Token)
  -- val is used exactly twice

fn read_only(cfg :_omega Config) -> Settings
  -- cfg can be used any number of times

fn compile_only(phantom :_0 TypeInfo) -> Unit
  -- phantom is erased at runtime

Context Splitting

When type-checking a pair (e1, e2), the linear context Delta is split: Delta = Delta1 + Delta2 where each variable’s grade is partitioned between the two sub-expressions.

Delta1 + Delta2 = Delta
  if for each x:  r1 + r2 = r  where Delta(x) = r, Delta1(x) = r1, Delta2(x) = r2

Linear Protocol: Resource Safety

Linear types enforce resource protocols:

type File<State> where State in {Closed, Open}

fn open(path: String) -> File<Open> :_1
  effects: filesystem.read

fn read(f: File<Open> :_1) -> (File<Open> :_1, Bytes)
  effects: filesystem.read

fn close(f: File<Open> :_1) -> Unit
  effects: filesystem.write

-- COMPILE ERROR: f used twice (grade violation)
-- fn bad(f: File<Open> :_1) = (read(f), read(f))

-- COMPILE ERROR: f not used (linear variable dropped)
-- fn leak(f: File<Open> :_1) = ()

2.6 Typestate

Typestate tracks the protocol state of objects through the type system. State changes are reflected in the type.

State Machine Declaration

type Order<State>
  where State in {Created, Paid, Shipped, Delivered, Cancelled}

Transition Typing

Gamma; Delta; Sigma, x @ S1 |- transition(x) : T ! E -| Sigma', x @ S2

The judgment produces an updated typestate context where x moves from state S1 to state S2.

Transition Rules

fn pay(o: Order<Created> :_1, payment: Payment)
    -> Order<Paid> :_1
  requires { payment.amount > 0 }
  effects: payment.charge

fn ship(o: Order<Paid> :_1, tracking: NonEmpty<String>)
    -> Order<Shipped> :_1
  effects: logistics.dispatch

-- COMPILE ERROR: cannot ship from Created state
-- fn bad(o: Order<Created>) = ship(o, "TRACK123")

Typestate + Linearity Interaction

Typestate variables MUST be linear (grade 1). This prevents aliasing: if two references point to the same object, the state becomes ambiguous. Linearity guarantees each stateful object has exactly one owner.

2.7 Information Flow Types

Every type carries a security label from a lattice (L, <=). Data can only flow from lower to higher labels. The default lattice is:

Public < Internal < Confidential < Restricted

Label Annotation

type SSN = String @Restricted
type Email = String @Internal
type PublicName = String @Public
type LogMessage = String @Public

Flow Rules

Gamma |- e : T @L1,  L1 <= L2
---------------------------------
Gamma |- e : T @L2                 (subsumption: can raise label)

Gamma |- e1 : T1 @L1,  Gamma |- e2 : T2 @L2
----------------------------------------------
Gamma |- (e1, e2) : (T1, T2) @(L1 join L2)    (join: pair takes max)

Declassification

Explicit declassification is required to lower a label:

fn mask_ssn(ssn: SSN) -> String @Public
  declassify { "***-**-" ++ ssn.last(4) }

Declassification points are tracked and auditable. The compiler emits a warning for every declassify so security reviews can inspect them.

Purpose Labels (GDPR/Privacy)

Beyond the security lattice, data carries purpose labels:

privacy: employee.ssn purpose {payroll, tax_reporting, w2_generation}

The compiler checks that ssn is only used in functions whose declared purpose includes one of {payroll, tax_reporting, w2_generation}. Using it in a function with purpose {analytics} is a compile error.

2.8 Totality Checking

Every function must be total unless annotated partial:

1. Coverage: Pattern matches must be exhaustive
2. Termination: Recursive calls must decrease on a well-founded measure

Termination Measures

fn factorial(n: Nat) -> Nat
  decreases n
{
  if n == 0 then 1
  else n * factorial(n - 1)
}

The compiler checks that n - 1 < n on each recursive call using the specified decreases measure.

Partial Escape Hatch

partial fn server_loop() -> Never
  effects: io
{
  -- intentionally non-terminating
}

partial functions cannot be called from total functions without an explicit trust annotation.

2.9 Type Interaction Rules

The six type features interact. These rules govern the interactions:

Rule 1: Refinement + Linearity

A refined linear type {v: T @_1 | P} is checked by splitting: the linear context tracks usage, the refinement predicate is verified by SMT. They do not interfere.

Rule 2: Typestate + Effects

A state transition must declare its effects. The effect row is checked independently from the state transition:

fn ship(o: Order<Paid> :_1) -> Order<Shipped> :_1
  effects: database.write, logistics.dispatch

Both the state transition (Paid -> Shipped) AND the effect compliance (only database.write and logistics.dispatch) are checked.

Rule 3: Information Flow + Effects

Effects are labeled with the minimum security level of data they may handle:

effects: log.info @Public          -- log may only contain public data
effects: database.write @Restricted -- database may contain restricted data

A function that handles Restricted data can call database.write but NOT log.info unless the data is declassified first.

Rule 4: Refinement + Dependent Types

Refinement predicates may reference dependent indices:

fn safe_index(v: Vec<T, n>, i: {x: Nat | x < n}) -> T

Here n is a dependent index and x < n is a refinement predicate. The SMT solver handles the arithmetic; the type checker handles the index propagation.

Rule 5: Linearity + Information Flow

Linear types and information flow labels are orthogonal. A value can be both linear and labeled:

fn process(key: CryptoKey @Restricted :_1) -> EncryptedData

The key must be used exactly once (linear) and cannot flow to public sinks (restricted).

Rule 6: Totality + Effects

Total functions must be pure or use only terminating effects. A function with effects: io (which may block indefinitely) cannot be total. The compiler partitions effects into terminating (pure, database.read) and potentially non-terminating (io, network).

3. Effect System

3.1 Effect Algebra

Effects use row polymorphism (Koka model). An effect row is an unordered set of effect labels with an optional row variable tail:

EffectRow = <l1, l2, ..., ln>       -- closed row (exactly these effects)
          | <l1, l2, ..., ln | e>   -- open row (these effects plus whatever e contains)
          | pure                     -- empty row (no effects)

Effect Labels (Built-in)

pure                   -- no side effects
console.read           -- read from stdin
console.write          -- write to stdout/stderr
filesystem.read        -- read files
filesystem.write       -- write files
network.connect        -- open network connections
network.send           -- send data over network
network.receive        -- receive data from network
database.read          -- read from database
database.write         -- write to database
payment.charge         -- charge a payment method
payment.refund         -- refund a payment
log.debug              -- debug logging
log.info               -- info logging
log.warn               -- warning logging
log.error              -- error logging
time.read              -- read current time
random                 -- generate random values
state<T>               -- mutable state of type T
exception<E>           -- may throw exception of type E
diverge                -- may not terminate

Custom Effects

effect audit.write<T>            -- write audit entries of type T
effect email.send                -- send emails
effect sms.send                  -- send SMS messages
effect cache.read                -- read from cache
effect cache.write               -- write to cache

3.2 Effect Polymorphism

Functions that are generic over effects use a row variable:

fn map<T, U>(list: List<T>, f: (T) -> <e> U) -> <e> List<U>

map inherits whatever effects f has. If f is pure, map is pure. If f does IO, map does IO.

3.3 Effect Subtyping

A function with fewer effects is a subtype of a function with more:

<e1> <: <e1, e2>     -- fewer effects is more specific
pure <: <e>          -- pure is subtype of any effect

This means a pure function can be passed where an effectful function is expected, but not the reverse.

3.4 Effect Handlers

Effect handlers eliminate effects from the row. A handler for exception<E> transforms <exception<E> | e> into <e>:

handle result = risky_operation()
  with exception<ParseError> -> default_value
-- result has type T with effect row <e> (exception removed)

3.5 Effect Checking Rules

(* A function's body must only use effects declared in its signature *)

Gamma; Delta |- body : T ! E_actual
E_actual <=_row E_declared
-----------------------------------------
Gamma; Delta |- fn f() -> <E_declared> T { body }  OK

(* Effect row inclusion *)
E1 <=_row E2   iff   every label in E1 is also in E2
                 or   E2 has an open tail variable

3.6 Effect Hierarchy

Effects form a hierarchy for convenience:

io = {console.read, console.write, filesystem.read, filesystem.write,
      network.connect, network.send, network.receive, time.read, random}

database = {database.read, database.write}

logging = {log.debug, log.info, log.warn, log.error}

Using effects: io is shorthand for allowing all IO sub-effects.

4. Implementation IR Format

The Implementation IR is what AI generates. It is NOT human-readable. It is a flat, fully-annotated, canonically-serialized format optimized for Transformer attention patterns and maximum compiler checking.

4.1 Design Principles

1. No variable names. Slots are numbered ($0, $1, $2). Eliminates naming hallucination.
2. Flat structure. No nesting deeper than 2 levels. Each operation is a single instruction. Optimized for Transformer positional attention.
3. Complete annotations. Every expression has an explicit type. No type inference. Every function has explicit effect and linearity annotations.
4. Canonical serialization. One way to write everything. No stylistic variation. Enables exact diff and caching.
5. Stable addressing. Instructions are addressed by index, not by name. Enables stable error references.

4.2 IR Grammar

IRModule       = 'module' ModuleId '{' { IRDecl } '}' ;

IRDecl         = IRFunction
               | IRType
               | IRImpl ;

IRFunction     = 'fn' FnId ':' IRFnType '{'
                   { IRInstr }
                 '}' ;

IRFnType       = '(' { SlotDecl } ')' '->' IRType '!' EffectRow
                 '@' Grade
                 ['pre' ':' IRPred]
                 ['post' ':' IRPred] ;

SlotDecl       = SlotId ':' IRType '@' Grade ['@' Label] ;
SlotId         = '$' Nat ;

IRInstr        = SlotId '=' IRExpr ':' IRType ;

IRExpr         = 'const' Literal
               | 'load' SlotId
               | 'call' FnId '(' { SlotId } ')'
               | 'field' SlotId '.' FieldIndex
               | 'construct' TypeId '{' { FieldIndex '=' SlotId } '}'
               | 'match' SlotId '{' { MatchArm } '}'
               | 'if' SlotId 'then' BlockId 'else' BlockId
               | 'arith' ArithOp SlotId SlotId
               | 'cmp' CmpOp SlotId SlotId
               | 'cast' SlotId 'as' IRType
               | 'transition' SlotId 'to' StateId
               | 'declassify' SlotId 'to' Label
               | 'handle' EffectId BlockId HandlerBlock ;

MatchArm       = Pattern '=>' BlockId ;
BlockId        = '#' Nat ;
FieldIndex     = '.' Nat ;

ArithOp        = 'add' | 'sub' | 'mul' | 'div' | 'mod' ;
CmpOp          = 'eq' | 'ne' | 'lt' | 'le' | 'gt' | 'ge' ;

IRPred         = 'true'
               | 'false'
               | 'cmp' CmpOp SlotId SlotId
               | 'and' IRPred IRPred
               | 'or' IRPred IRPred
               | 'not' IRPred
               | 'forall' SlotId 'in' SlotId ':' IRPred
               | 'measure' MeasureId '(' SlotId ')' CmpOp Literal
               | 'call' FnId '(' { SlotId } ')' ;

4.3 IR Example

The contract:

contract SafeDivision {
  input(a: Int, b: Int)
  output(result: Int)
  requires { b != 0 }
  ensures  { result * b + (a mod b) == a }
  effects  { pure }
}

Generates IR:

module safe_division {
  fn #0 : ($0: Int @omega, $1: Int @omega) -> Int ! pure
    pre: cmp ne $1 (const 0)
    post: cmp eq (arith add (arith mul $result $1) (arith mod $0 $1)) $0
  {
    $2 = arith div $0 $1 : Int
    $result = load $2 : Int
  }
}

4.4 Canonical Serialization Format

The IR has two serialization formats:

1. Text format (.assura-ir): Human-inspectable, used for debugging. The grammar above.
2. Binary format (.assura-irb): Compact, used for caching and transmission. MessagePack encoding with a fixed schema.

Both formats are canonicalized:

• Slots are numbered sequentially from $0
• Instructions are in topological order (definition before use)
• No comments, no whitespace variation
• Identical IR always produces identical bytes

4.5 IR Metadata

Every IR module includes metadata for tracing:

{
  "source_contract": "src/contracts/division.assura",
  "source_hash": "sha256:abc123...",
  "generator": "claude-4/2026-06",
  "generation_timestamp": "2026-06-11T20:00:00Z",
  "assura_version": "0.4.0",
  "verification_status": "unverified"
}

5. Verification Architecture

5.1 Verification Layers

The compiler verifies in layers, fastest first. Each layer runs only if all previous layers pass.

Layer 0: Syntactic / Structural (No SMT, < 10ms)

Checks performed purely by the parser and type checker algorithms:

No SMT solver is invoked. These checks are decidable and deterministic.

Layer 1: Lightweight SMT (Decidable, < 200ms)

Checks using quantifier-free decidable SMT theories:

All queries in this layer are decidable. The solver always terminates.

Layer 2: Heavy SMT (Undecidable, < 10s, budgeted)

Checks using quantified or nonlinear SMT theories with timeouts:

Each query has a timeout. If the solver times out, the compiler does NOT reject the code. Instead:

1. It emits a warning: W0801: Unable to verify invariant within 5s
2. It generates a property-based test for the unverified property
3. The property is re-checked at Layer 2 if the user runs assura verify --deep

5.2 Z3 Encoding Strategy

Refinement Types -> SMT

Each refinement subtyping check {v:S | P} <: {v:T | Q} generates:

; Declare the value variable
(declare-const v Int)

; Assert the antecedent (what we know)
(assert P_encoded)

; Assert the negation of the consequent (what we need to prove)
(assert (not Q_encoded))

; Check satisfiability
(check-sat)
; unsat => P implies Q => subtyping holds
; sat   => counterexample exists => type error

Measures -> Uninterpreted Functions

measure len : List<T> -> Nat
  len([])     = 0
  len(_ :: t) = 1 + len(t)

Encodes as:

(declare-fun len (List) Int)
(assert (= (len nil) 0))
(assert (forall ((x T) (xs List))
  (= (len (cons x xs)) (+ 1 (len xs)))))
(assert (forall ((xs List)) (>= (len xs) 0)))

Typestate -> Enumeration Datatypes

(declare-datatypes () ((OrderState Created Paid Shipped Delivered Cancelled Error)))

(define-fun valid_transition ((from OrderState) (action Int)) OrderState
  (ite (and (= from Created) (= action 0)) Paid        ; pay
  (ite (and (= from Paid)    (= action 1)) Shipped     ; ship
  (ite (and (= from Shipped) (= action 2)) Delivered   ; deliver
       Error))))

; Verify sequence: pay then ship
(declare-const s0 OrderState)
(declare-const s1 OrderState)
(assert (= s0 (valid_transition Created 0)))
(assert (= s1 (valid_transition s0 1)))
(assert (= s1 Error))
(check-sat)  ; unsat => sequence is valid

Information Flow -> Lattice Constraints

(declare-datatypes () ((Label Public Internal Confidential Restricted)))

(define-fun flows ((from Label) (to Label)) Bool
  (or (= from to)
      (and (= from Public) (not (= to Public)))  ; Public flows anywhere
      (and (= from Internal) (or (= to Confidential) (= to Restricted)))
      (and (= from Confidential) (= to Restricted))))

; Check: can Restricted data flow to Public log?
(assert (flows Restricted Public))
(check-sat)  ; sat would mean it's allowed; expect unsat

Business Invariants -> Quantified Assertions

invariant { forall u in users.values(): u.email.is_valid() }

Encodes as:

(declare-fun users (Int) User)
(declare-fun user_count () Int)
(declare-fun is_valid_email (String) Bool)

(assert (not
  (forall ((i Int))
    (=> (and (>= i 0) (< i user_count))
        (is_valid_email (email (users i)))))))
(check-sat)
; sat => counterexample: specific i where email is invalid
; unsat => invariant holds

5.3 Counterexample Extraction

When Z3 returns sat (property violated), the compiler extracts a model (concrete values for each variable) and formats it as a structured counterexample:

{
  "error_code": "E0412",
  "category": "invariant_violation",
  "constraint": "order.total == sum(item.price * item.qty)",
  "counterexample": {
    "items": [{"price": 10, "qty": 2}, {"price": 5, "qty": 3}],
    "expected_total": 35,
    "actual_total": 0
  },
  "model_values": {
    "v": 0,
    "items.len": 2,
    "items[0].price": 10,
    "items[0].qty": 2
  }
}

The counterexample includes concrete inputs that violate the property, making it actionable for AI to fix.

6. Rust Codegen Mapping

The Assura compiler generates Rust source code. This section defines how each Assura construct maps to Rust.

6.1 Types

6.2 Refinement Types

Refinement types erase to their base type at runtime. The predicate is checked at construction in debug mode:

type Pos = {v: Int | v > 0}

Generates:

#![allow(unused)]
fn main() {
/// Assura refinement type: {v: Int | v > 0}
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Pos(i64);

impl Pos {
    pub fn new(v: i64) -> Result<Self, AssuraRefinementError> {
        #[cfg(debug_assertions)]
        if !(v > 0) {
            return Err(AssuraRefinementError {
                type_name: "Pos",
                predicate: "v > 0",
                actual_value: format!("{}", v),
            });
        }
        Ok(Self(v))
    }

    pub fn value(&self) -> i64 { self.0 }
}
}

In release mode, the check is elided. The Assura compiler has already proven the predicate holds at every construction site.

6.3 Typestate

Typestate maps to Rust phantom types + the typestate pattern:

type Order<State> where State in {Created, Paid, Shipped}

Generates:

#![allow(unused)]
fn main() {
pub mod order_states {
    pub struct Created;
    pub struct Paid;
    pub struct Shipped;
}

pub struct Order<State> {
    // ... fields ...
    _state: std::marker::PhantomData<State>,
}

impl Order<order_states::Created> {
    pub fn pay(self, payment: Payment) -> Order<order_states::Paid> {
        Order {
            // ... fields ...
            _state: std::marker::PhantomData,
        }
    }
}

impl Order<order_states::Paid> {
    pub fn ship(self, tracking: String) -> Order<order_states::Shipped> {
        // ...
    }
}

// pay() on Order<Shipped> does not exist -> compile error in Rust too
}

The self parameter consumes the old state (Rust ownership = linear). The return type has the new state. Rust’s type checker enforces the state machine as a second safety net.

6.4 Effects

Effects map to Rust traits that bound what capabilities a function receives:

fn save(order: Order) -> OrderId
  effects: database.write, log.info

Generates:

#![allow(unused)]
fn main() {
pub fn save<Db: DatabaseWrite, Log: LogInfo>(
    db: &mut Db,
    log: &Log,
    order: Order,
) -> OrderId {
    // implementation
}
}

Capability traits are passed explicitly. A function that declares effects: pure receives no capability parameters and cannot perform any side effects.

6.5 Linear Types

Linear types map to Rust ownership. A linear parameter is passed by value (moved), ensuring single use:

fn close(f: File<Open> :_1) -> Unit

Generates:

#![allow(unused)]
fn main() {
pub fn close(f: File<Open>) {
    // f is moved in, cannot be used after this call
    drop(f);
}
}

Rust’s move semantics naturally enforce linearity. The Assura compiler additionally checks exact usage counts (Rust allows unused variables with #[allow(unused)]; Assura does not).

6.6 Information Flow Labels

Labels erase at runtime. They exist only in the Assura type checker. The generated Rust code has no label representation:

type SSN = String @Restricted

Generates:

#![allow(unused)]
fn main() {
pub type SSN = String;  // label erased
}

The Assura compiler has already verified that no Restricted data flows to Public sinks. The Rust code does not need to re-check.

6.7 Contracts (requires/ensures)

In debug mode, contracts become runtime assertions. In release mode, they are elided:

fn divide(a: Int, b: Int) -> Int
  requires { b != 0 }
  ensures  { result * b + (a % b) == a }

Generates:

#![allow(unused)]
fn main() {
pub fn divide(a: i64, b: i64) -> i64 {
    debug_assert!(b != 0, "Assura requires: b != 0");

    let result = a / b;

    debug_assert!(
        result * b + (a % b) == a,
        "Assura ensures: result * b + (a % b) == a"
    );

    result
}
}

6.8 Measures

Measures generate pure Rust functions used only in debug assertions:

measure len : List<T> -> Nat

Generates:

#![allow(unused)]
fn main() {
#[cfg(debug_assertions)]
fn assura_measure_len<T>(list: &[T]) -> u64 {
    list.len() as u64
}
}

6.9 Dependent Indices

Dependent indices erase completely. Vec<T, n> becomes Vec<T>:

fn append(a: Vec<T, n>, b: Vec<T, m>) -> Vec<T, n + m>

Generates:

#![allow(unused)]
fn main() {
pub fn append<T>(mut a: Vec<T>, b: Vec<T>) -> Vec<T> {
    a.extend(b);
    a
}
}

The index arithmetic (n + m) was verified at compile time. The Rust code is a plain Vec with no runtime size tracking.

6.10 Extern and Bind

extern functions generate a trait that the hand-written Rust code must implement:

extern fn render_template(name: String, data: Map<String, Value>) -> Html
  effects: filesystem.read

Generates:

#![allow(unused)]
fn main() {
pub trait RenderTemplateExtern {
    fn render_template(
        &self,
        name: String,
        data: BTreeMap<String, Value>,
    ) -> Html;
}
}

bind functions generate wrapper functions with debug assertions around the bound Rust function:

#![allow(unused)]
fn main() {
pub fn render_page_checked(template: String, user: User) -> Html {
    debug_assert!(!template.is_empty(), "Assura requires: template.length > 0");

    let result = app::renderer::render_page(template, user.clone());

    debug_assert!(
        result.contains(&user.name),
        "Assura ensures: result.contains(user.name)"
    );
    debug_assert!(
        !result.contains(&user.password),
        "Assura ensures: not result.contains(user.password)"
    );

    result
}
}

7. Error Code Catalog

Error codes are stable identifiers for AI fix-pattern databases. The format is ANNSSS where A = Assura, NN = category (2 digits), SSS = specific error (3 digits).

7.1 Category Index

7.2 Specific Error Codes

Syntax (A01xxx)

Name Resolution (A02xxx)

Type Mismatch (A03xxx)

Refinement Violation (A04xxx)

Linearity (A05xxx)

Typestate (A06xxx)

Effect Violation (A07xxx)

Information Flow (A08xxx)

Totality (A09xxx)

Business Invariant (A11xxx)

Concurrency (A12xxx)

Numerical Precision (A13xxx)

Privacy (A16xxx)

Schema Evolution (A17xxx)

API Evolution (A21xxx)

Complexity Bounds (A22xxx)

7.3 Error Output Format

Every error is emitted as structured JSON:

{
  "error_code": "A05001",
  "severity": "error",
  "category": "linearity",
  "message": "Linear variable `conn` used twice",
  "primary_location": {
    "file": "src/db.assura-impl",
    "line": 23,
    "col": 5,
    "instruction_index": 14
  },
  "secondary_locations": [
    {
      "file": "src/db.assura-impl",
      "line": 27,
      "col": 5,
      "instruction_index": 18,
      "label": "second use here"
    }
  ],
  "contract_reference": {
    "file": "contracts/db.assura",
    "line": 8,
    "clause": "conn :_1 DbConnection"
  },
  "suggested_fixes": [
    {
      "description": "Clone conn before second use",
      "confidence": 0.4,
      "note": "Cloning a linear resource defeats its purpose"
    },
    {
      "description": "Split operations into separate functions",
      "confidence": 0.85,
      "replacement_hint": "extract second use into a new function"
    }
  ],
  "related_errors": [],
  "documentation_url": "https://assura-lang.github.io/assura/error-codes.html"
}

8. Module System

8.1 Module Declaration

Every .assura file is a module. The module name matches the file path:

contracts/
  payment/
    order.assura     -> module payment.order
    refund.assura    -> module payment.refund
  user.assura        -> module user

8.2 Import Rules

import payment.order                    -- import entire module
import payment.order { Order, Item }    -- import specific names
import payment.order as po              -- aliased import

Visibility

By default, all declarations are module-private. Use pub to export:

pub type Order { ... }          -- exported
type InternalHelper { ... }     -- private to module

pub contract PlaceOrder { ... } -- exported

8.3 Contract Composition

Contracts can extend other contracts:

contract BaseEntity {
  ensures { self.id != "" }
  ensures { self.created_at <= self.updated_at }
}

contract Order extends BaseEntity {
  -- inherits BaseEntity's ensures clauses
  ensures { self.total >= 0 }
}

8.4 Service Composition

Services can depend on other services:

service OrderService {
  depends: PaymentService, InventoryService

  operation PlaceOrder {
    -- can reference PaymentService.charge and InventoryService.reserve
  }
}

8.5 Contract Libraries

Reusable contract patterns are published as packages:

import assura.std.crud { CrudService }
import assura.std.auth { Authenticated, Authorized }

service UserService extends CrudService<User> {
  -- inherits Create, Read, Update, Delete operations
  -- with standard contracts for each
}

9. Standard Library

9.1 Core Types

module assura.core

-- Primitive types are built-in: Int, Nat, Float, Bool, String,
-- Bytes, Unit, Never

-- Standard refinement aliases
pub type Pos       = {v: Int   | v > 0}
pub type NonNeg    = {v: Int   | v >= 0}
pub type NonZero   = {v: Int   | v != 0}
pub type Percentage = {v: Float | 0.0 <= v and v <= 1.0}

-- Constrained strings
pub type NonEmpty  = {v: String | len(v) > 0}
pub type Email     = {v: String | is_email(v)}
pub type Url       = {v: String | is_url(v)}
pub type Uuid      = {v: String | is_uuid(v)}

-- Time
pub type Timestamp = {v: Int | v > 0}    -- Unix epoch millis
pub type Duration  = {v: Int | v >= 0}   -- milliseconds
pub type Date      = { year: Int, month: Btwn<1,13>, day: Btwn<1,32> }

9.2 Collection Contracts

module assura.collections

pub measure len<T> : List<T> -> Nat
pub measure elems<T> : List<T> -> Set<T>
pub measure keys<K,V> : Map<K,V> -> Set<K>
pub measure values<K,V> : Map<K,V> -> List<V>
pub measure size<T> : Set<T> -> Nat

pub contract ListOps<T> {
  operation head {
    input(list: NonEmpty<List<T>>)
    output(result: T)
    ensures { result in elems(list) }
    effects { pure }
  }

  operation append {
    input(a: List<T>, b: List<T>)
    output(result: List<T>)
    ensures { len(result) == len(a) + len(b) }
    ensures { elems(result) == elems(a) ++ elems(b) }
    effects { pure }
  }

  operation filter {
    input(list: List<T>, pred: (T) -> Bool)
    output(result: List<T>)
    ensures { len(result) <= len(list) }
    ensures { forall x in result: x in elems(list) }
    ensures { forall x in result: pred(x) == true }
    effects { pure }
  }

  operation sort {
    input(list: List<T>)
    output(result: List<T>)
    requires { T has Ord }
    ensures { len(result) == len(list) }
    ensures { elems(result) == elems(list) }
    ensures { forall i in 0..len(result)-1:
                result[i] <= result[i+1] }
    effects { pure }
  }
}

9.3 Numerical Types

module assura.numeric

pub type FixedDecimal<Scale: Nat, Unit: Label>

pub type USD
pub type EUR
pub type GBP
pub type Percent

pub type Money<C> = FixedDecimal<2, C>

pub contract NumericOps {
  operation add<S, U> {
    input(a: FixedDecimal<S, U>, b: FixedDecimal<S, U>)
    output(result: FixedDecimal<S, U>)
    ensures { result == a + b }
    effects { pure }
  }

  operation scale<S, U> {
    input(amount: FixedDecimal<S, U>, factor: Float)
    output(result: FixedDecimal<S, U>)
    effects { pure }
  }
}

9.4 Common Contract Patterns

module assura.std.crud

pub service CrudService<Entity> {
  type Id = Uuid

  states: Draft -> Active -> Archived -> Deleted

  operation Create {
    input(data: Entity)
    output(id: Id)
    ensures { self.store.contains(id) }
    ensures { self.store[id] == data }
    effects { database.write }
  }

  operation Read {
    input(id: Id)
    output(entity: Entity)
    requires { self.store.contains(id) }
    effects { database.read }
  }

  operation Update {
    input(id: Id, data: Entity)
    requires { self.store.contains(id) }
    ensures  { self.store[id] == data }
    effects  { database.write }
  }

  operation Delete {
    input(id: Id)
    requires { self.store.contains(id) }
    ensures  { not self.store.contains(id) }
    effects  { database.write }
  }

  invariant { forall id in self.store.keys():
                self.store[id].is_valid() }
}

9.5 Auth Contracts

module assura.std.auth

pub type Role = enum { Admin, User, ReadOnly, Service }
pub type Principal = { id: Uuid, roles: Set<Role> }

pub contract Authenticated {
  requires { self.principal != null }
  requires { self.principal.is_authenticated() }
}

pub contract Authorized<R: Role> {
  extends Authenticated
  requires { R in self.principal.roles }
}

10. CLI Interface

10.1 Commands

assura <command> [options] [files...]

COMMANDS:
  check       Type-check contracts and implementations (layers 0-1)
  verify      Full verification including SMT (layers 0-2)
  build       Check + generate Rust code + compile
  run         Build + execute
  init        Create a new Assura project
  fmt         Format contract files
  lsp         Start the language server
  ir          Inspect generated IR
  explain     Show detailed explanation of an error code

OPTIONS (global):
  --json              Output diagnostics as JSON (default for AI)
  --human             Output diagnostics as human-readable text
  --color             Force color output
  --no-color          Disable color output
  -q, --quiet         Only output errors
  -v, --verbose       Show verification details
  --threads <N>       Number of parallel verification threads

10.2 Command Details

assura check

assura check [options] [files...]

Runs layers 0 and 1 (structural checks + decidable SMT).
Fast feedback loop for AI iteration.

OPTIONS:
  --layer <N>         Run only up to layer N (0, 1, or 2)
  --contract <file>   Check only this contract
  --watch             Watch for file changes and re-check
  --timeout <ms>      SMT solver timeout per query (default: 1000)

assura verify

assura verify [options] [files...]

Runs all layers including layer 2 (heavy SMT).
Used for pre-commit verification.

OPTIONS:
  --deep              Enable maximum verification depth
  --timeout <ms>      SMT solver timeout per query (default: 10000)
  --fuel <N>          Recursion unfolding depth (default: 5)
  --solver <name>     SMT solver: z3 (default), cvc5
  --stats             Show verification statistics
  --dump-smt <dir>    Write SMT queries to directory for debugging

assura build

assura build [options]

Verify + generate Rust code + compile with rustc.

OPTIONS:
  --release           Optimize generated Rust (release mode)
  --target <triple>   Rust target triple (e.g., wasm32-wasi)
  --out <dir>         Output directory (default: target/)
  --skip-verify       Skip layer 2 (only layers 0-1), for dev speed
  --keep-generated    Don't delete generated .rs files after build

assura init

assura init [name]

Create a new Assura project.

Generated structure:
  <name>/
    assura.toml          # project configuration
    contracts/
      main.assura        # initial contract file
    src/
      main.rs            # hand-written Rust entry point
    Cargo.toml           # workspace manifest

assura explain

assura explain <error_code>

Show detailed explanation of an error code with examples.

$ assura explain A05001
Error A05001: Linear variable used twice
Category: Linearity (Layer 0)

A variable with linear grade (exactly-once usage) was used more
than once. Linear types ensure resources like database connections,
file handles, and tokens are consumed exactly once.

Example:
  fn bad(conn :_1 DbConnection) -> (Result, Result) {
    (query(conn, "SELECT 1"), query(conn, "SELECT 2"))
  }           ^^^^^                     ^^^^^
  First use here                Second use here (ERROR)

Fix: Split into separate functions, each receiving its own connection.

10.3 Configuration File

assura.toml at the project root:

[project]
name = "my-service"
version = "0.1.0"
assura-version = "0.1"

[contracts]
path = "contracts/"

[build]
target = "native"           # or "wasm32-wasi"
generated-dir = "generated/"
keep-generated = false

[verify]
default-layer = 1           # default for `assura check`
smt-solver = "z3"
smt-timeout-ms = 5000
fuel = 5

[effects]
[effects.custom]
"audit.write" = { label = "Internal" }
"email.send"  = { label = "Public" }

[security]
labels = ["Public", "Internal", "Confidential", "Restricted"]
default-label = "Internal"

11. AI Agent API

The AI agent API is how AI systems interact with the Assura compiler programmatically. It supports both gRPC and JSON-over-HTTP.

11.1 API Operations

Check

POST /v1/check

Request:
{
  "contracts": [
    {
      "path": "contracts/order.assura",
      "content": "service OrderService { ... }"
    }
  ],
  "implementations": [
    {
      "path": "src/order.assura-ir",
      "content": "module order { fn #0 ... }"
    }
  ],
  "options": {
    "max_layer": 2,
    "smt_timeout_ms": 5000,
    "fuel": 5
  }
}

Response:
{
  "status": "error",
  "diagnostics": [ ... ],
  "statistics": {
    "layer_0_time_ms": 12,
    "layer_1_time_ms": 87,
    "layer_2_time_ms": 2340,
    "smt_queries": 15,
    "smt_sat": 1,
    "smt_unsat": 14,
    "smt_timeout": 0
  }
}

Build

POST /v1/build

Request:
{
  "contracts": [ ... ],
  "implementations": [ ... ],
  "target": "wasm32-wasi",
  "release": true
}

Response:
{
  "status": "success",
  "artifacts": [
    {
      "path": "target/order.wasm",
      "size_bytes": 45230,
      "content_base64": "AGFzbQEA..."
    }
  ]
}

Explain

GET /v1/explain/A05001

Response:
{
  "error_code": "A05001",
  "category": "linearity",
  "layer": 0,
  "title": "Linear variable used twice",
  "description": "...",
  "examples": [ ... ],
  "fix_patterns": [ ... ]
}

Health

GET /v1/health

Response:
{
  "status": "healthy",
  "version": "0.1.0",
  "smt_solver": "z3",
  "smt_solver_version": "4.13.0"
}

11.2 gRPC Service Definition

syntax = "proto3";
package assura.v1;

service AssuraCompiler {
  rpc Check(CheckRequest) returns (CheckResponse);
  rpc Build(BuildRequest) returns (BuildResponse);
  rpc Explain(ExplainRequest) returns (ExplainResponse);
  rpc Health(HealthRequest) returns (HealthResponse);
  rpc CheckStream(stream CheckRequest) returns (stream Diagnostic);
}

message CheckRequest {
  repeated SourceFile contracts = 1;
  repeated SourceFile implementations = 2;
  CheckOptions options = 3;
}

message SourceFile {
  string path = 1;
  string content = 2;
  string hash = 3;
}

message CheckOptions {
  int32 max_layer = 1;
  int32 smt_timeout_ms = 2;
  int32 fuel = 3;
  string solver = 4;
}

message CheckResponse {
  Status status = 1;
  repeated Diagnostic diagnostics = 2;
  VerificationStats statistics = 3;
}

enum Status {
  STATUS_UNKNOWN = 0;
  STATUS_OK = 1;
  STATUS_ERROR = 2;
  STATUS_WARNING = 3;
}

message Diagnostic {
  string error_code = 1;
  Severity severity = 2;
  string category = 3;
  string message = 4;
  Location primary_location = 5;
  repeated Location secondary_locations = 6;
  ContractReference contract_reference = 7;
  Counterexample counterexample = 8;
  repeated SuggestedFix suggested_fixes = 9;
}

enum Severity {
  SEVERITY_UNKNOWN = 0;
  SEVERITY_ERROR = 1;
  SEVERITY_WARNING = 2;
  SEVERITY_INFO = 3;
  SEVERITY_HINT = 4;
}

message Location {
  string file = 1;
  int32 line = 2;
  int32 col = 3;
  int32 end_line = 4;
  int32 end_col = 5;
  string label = 6;
  string source_text = 7;
}

message ContractReference {
  string file = 1;
  int32 line = 2;
  string clause = 3;
}

message Counterexample {
  string constraint = 1;
  map<string, string> inputs = 2;
  string expected = 3;
  string actual = 4;
}

message SuggestedFix {
  string description = 1;
  float confidence = 2;
  string replacement = 3;
}

message VerificationStats {
  int32 layer_0_ms = 1;
  int32 layer_1_ms = 2;
  int32 layer_2_ms = 3;
  int32 smt_queries = 4;
  int32 smt_sat = 5;
  int32 smt_unsat = 6;
  int32 smt_timeout = 7;
}

message BuildRequest {
  repeated SourceFile contracts = 1;
  repeated SourceFile implementations = 2;
  string target = 3;
  bool release = 4;
}

message BuildResponse {
  Status status = 1;
  repeated Artifact artifacts = 2;
  CheckResponse verification = 3;
}

message Artifact {
  string path = 1;
  int64 size_bytes = 2;
  bytes content = 3;
}

message ExplainRequest {
  string error_code = 1;
}

message ExplainResponse {
  string error_code = 1;
  string category = 2;
  int32 layer = 3;
  string title = 4;
  string description = 5;
  repeated string examples = 6;
  repeated string fix_patterns = 7;
}

message HealthRequest {}

message HealthResponse {
  string status = 1;
  string version = 2;
  string smt_solver = 3;
  string smt_solver_version = 4;
}

11.3 Streaming Mode

For AI iteration loops, the CheckStream RPC accepts a stream of incremental submissions. The AI sends a revised implementation, and the compiler streams back diagnostics as they are discovered (layer 0 results first, then layer 1, then layer 2). This enables the AI to start fixing layer 0 errors while layer 2 verification is still running.

12. Decidability Boundaries

This section defines exactly which checks are decidable (always terminate), semidecidable (may not terminate but have practical mitigations), and undecidable (require timeouts).

12.1 Decidability Map

12.2 Dangerous Combinations

These combinations are known to cause solver instability:

1. Quantified refinements + recursive measures: Can trigger unbounded MBQI. Mitigation: limit fuel, use E-matching triggers.

2. Nonlinear integer arithmetic (NIA): Undecidable. Avoid refinements with multiplication of two variables (x * y > z). Allow constant multiplication (x * 3 > z, which is LIA).

3. Array theory + quantifiers: Can cause exponential blowup. Mitigation: use bounded quantification (forall i in 0..n).

4. Bitvector arithmetic + quantifiers: Decidable but exponential in bit-width. Avoid mixing BV with quantified formulas.

12.3 Timeout Strategy

When the SMT solver times out:

1. Layer 2 timeout: Emit warning, not error. Code compiles. Unverified property is flagged.

2. Layer 1 timeout: Emit error suggesting simplified predicate.

3. Persistent timeout: Suggest lemma hints, property splitting, trust annotation, or property-based test fallback.

12.4 Trust Escape Hatch

trust "manually reviewed: hash collision resistance"
invariant { forall a, b: if hash(a) == hash(b) then a == b }

Trust annotations:

• Require a justification string
• Are logged in the verification report
• Are flagged in security audits
• Cannot bypass layer 0 checks (syntax, types, linearity)

12.5 Verification Budget Configuration

[verify.budgets]
layer_0_timeout_ms = 100
layer_1_timeout_ms = 1000
layer_2_timeout_ms = 10000
total_timeout_ms = 300000
max_fuel = 10
max_smt_queries = 1000

13. Type Interaction Test Cases

The six type features (refinement, dependent, linear, typestate, effect, information flow) are each well-understood in isolation. The hard problem is their composition. This section defines concrete use cases that stress-test each pairwise and higher-order interaction, identifies what can go wrong, and specifies the expected compiler behavior.

There are C(6,2) = 15 pairwise interactions. We cover all 15, plus 4 three-way and 2 full-stack interactions, for 21 total test cases.

Test Case 1: Refinement + Linear (Ghost Use Problem)

Scenario: A refinement predicate references a linear variable.

fn transfer(
    from: Account :_1,
    to: Account :_1,
    amount: {v: Money<USD> | v > 0 and v <= from.balance}
) -> (Account, Account)
  effects: database.write

The problem: The refinement v <= from.balance “reads” from. Does this count as a use for linearity purposes? If yes, from is used twice (once in the refinement, once in the body). If no, the type checker must distinguish ghost/logical uses from computational uses.

Required behavior: Refinement predicates are ghost (logical, not computational). They do NOT count as a linear use. The grade of a variable in a refinement context is always 0 (erased). The type checker must track two usage contexts:

• Delta_computational: tracks runtime uses (must satisfy grades)
• Delta_logical: tracks refinement uses (always grade 0, unlimited)

Expected result: This code compiles. from is used once computationally (in the body) and once logically (in the refinement). The logical use is free.

Test:

-- MUST COMPILE: refinement use is ghost
fn test1(x: Int :_1, y: {v: Int | v < x}) -> Int
  effects: pure
{ x + y }

-- MUST REJECT: x used twice computationally
fn test1_bad(x: Int :_1, y: {v: Int | v < x}) -> (Int, Int)
  effects: pure
{ (x, x) }

Test Case 2: Refinement + Typestate (Guarded Transitions)

Scenario: A state transition whose validity depends on a refinement predicate over the object’s data.

service LoanService {
  type Loan<State> {
    amount: Money<USD>,
    credit_score: Nat,
    approved_amount: Money<USD>?
  }
  where State in {Applied, UnderReview, Approved, Denied, Disbursed}

  fn review(loan: Loan<Applied> :_1) -> Loan<UnderReview> :_1
    effects: database.write

  fn approve(
      loan: Loan<UnderReview> :_1,
      approved: {v: Money<USD> | v > 0 and v <= loan.amount}
  ) -> Loan<Approved> :_1
    requires { loan.credit_score >= 650 }
    effects: database.write

  fn deny(loan: Loan<UnderReview> :_1) -> Loan<Denied> :_1
    effects: database.write

  fn disburse(loan: Loan<Approved> :_1) -> Loan<Disbursed> :_1
    requires { loan.approved_amount is Some }
    effects: payment.charge, database.write
}

The problem: The approve transition has BOTH a typestate requirement (must be UnderReview) AND a refinement requirement (credit_score >= 650). The type checker must verify both independently: typestate via DFA, refinement via SMT. But what happens when the refinement references state-dependent data?

Interaction rule: Typestate checking happens BEFORE refinement checking in the same layer 0 pass. The typestate check confirms the transition is valid. Then the refinement check confirms the data guard. If typestate fails, refinement is not checked (no point).

Test:

-- MUST REJECT A06002: wrong state (Applied, need UnderReview)
fn bad1(loan: Loan<Applied> :_1) -> Loan<Approved> :_1
{ approve(loan, Money.new(1000)) }

-- MUST REJECT A04001: credit_score may be < 650
fn bad2(loan: Loan<UnderReview> :_1) -> Loan<Approved> :_1
{ approve(loan, Money.new(1000)) }

-- MUST COMPILE: both state and refinement satisfied
fn good(
    loan: Loan<UnderReview> :_1
) -> Loan<Approved> :_1
  requires { loan.credit_score >= 700 }
{ approve(loan, Money.new(loan.amount.value())) }

Test Case 3: Refinement + Dependent (Index Arithmetic)

Scenario: A function that splits a vector at a refined index, producing two vectors whose lengths must add up.

fn split_at<T>(
    v: Vec<T, n>,
    i: {x: Nat | x <= n}
) -> (Vec<T, i>, Vec<T, n - i>)
  effects: pure
  ensures { len(result.0) + len(result.1) == n }

The problem: The return type (Vec<T, i>, Vec<T, n - i>) uses i as both a refinement-checked value AND a dependent index. The type checker must:

1. Verify i <= n (refinement, SMT)
2. Compute n - i as a type-level index (dependent types)
3. Verify i + (n - i) == n (ensures clause, SMT)

Interaction rule: Refined values that appear in dependent positions are first checked for their refinement predicate, then their value is lifted into the index domain. The SMT solver sees both the refinement constraint and the index arithmetic in the same query.

Test:

-- MUST COMPILE: i is within bounds, arithmetic checks out
fn test3() -> (Vec<Int, 3>, Vec<Int, 2>)
  effects: pure
{
  let v: Vec<Int, 5> = [1, 2, 3, 4, 5]
  split_at(v, 3)
}

-- MUST REJECT A04005: index may exceed length
fn bad3<T>(v: Vec<T, n>, i: Nat) -> (Vec<T, i>, Vec<T, n - i>)
  effects: pure
{ split_at(v, i) }
  -- i has no upper bound refinement

Test Case 4: Linear + Effect (Resource-Scoped Effects)

Scenario: A database transaction where the connection is linear and effects are scoped to the connection’s lifetime.

fn with_transaction<T>(
    conn: DbConnection :_1,
    body: (TxHandle :_1) -> <database.write, database.read> T
) -> T
  effects: database.write, database.read
  ensures { conn is consumed }
  ensures { transaction is committed or rolled back }

The problem: The body closure captures a TxHandle that is linear (must be committed or rolled back exactly once). The effect row of the closure must be a SUBSET of the effects declared by with_transaction. And the linear handle must be consumed inside the closure, not leaked out.

Interaction rule: When type-checking a closure:

1. The closure’s effect row must be a subset of the enclosing function’s effect row
2. Linear variables captured by the closure must be consumed within it (they cannot escape)
3. The closure itself may be linear (called exactly once)

Test:

-- MUST COMPILE: handle consumed, effects match
fn good4(conn: DbConnection :_1) -> Order
  effects: database.write, database.read
{
  with_transaction(conn, fn(tx: TxHandle :_1) -> Order {
    let order = tx.insert(new_order)    -- database.write
    tx.commit()                          -- consumes tx
    order
  })
}

-- MUST REJECT A05002: tx not consumed (never committed)
fn bad4a(conn: DbConnection :_1) -> Order
  effects: database.write, database.read
{
  with_transaction(conn, fn(tx: TxHandle :_1) -> Order {
    let order = tx.insert(new_order)
    order
    -- tx dropped without commit or rollback!
  })
}

-- MUST REJECT A07001: network effect not in closure's allowed set
fn bad4b(conn: DbConnection :_1) -> Order
  effects: database.write, database.read
{
  with_transaction(conn, fn(tx: TxHandle :_1) -> Order {
    let data = http.get("http://example.com")  -- network effect!
    tx.commit()
    data
  })
}

Test Case 5: Typestate + Information Flow (Label Transitions)

Scenario: A medical record system where reviewing a record changes its security label.

service MedicalRecords {
  type Record<State> {
    patient_name: String @Confidential,
    diagnosis: String @Restricted,
    summary: String @Internal
  }
  where State in {Draft, InReview, Approved, Published}

  -- Draft records are fully restricted
  fn submit_for_review(r: Record<Draft> :_1)
      -> Record<InReview> :_1
    effects: database.write
    -- all fields remain at their original labels

  -- Approving declassifies the summary to Public
  fn approve(r: Record<InReview> :_1)
      -> Record<Approved> :_1
    effects: database.write, audit.write
    ensures { result.summary @Public }
    declassify { r.summary to @Public }

  -- Publishing requires the summary to be public
  fn publish(r: Record<Approved> :_1)
      -> Record<Published> :_1
    requires { r.summary @Public }
    effects: database.write, network.send
}

The problem: The approve transition does TWO things: changes the typestate (InReview -> Approved) AND changes the information flow label of a field (summary from @Internal to @Public via explicit declassification). The type checker must:

1. Track typestate transitions (DFA)
2. Track information flow labels per field
3. Verify that declassification is explicit
4. Verify that publish can only be called when summary is @Public

Interaction rule: Typestate and information flow labels are tracked in separate contexts (Sigma for state, Lambda for labels). A state transition may include declassify clauses that update the label context. The label change is only valid inside a declassify block.

Test:

-- MUST COMPILE: full valid pipeline
fn good5(r: Record<Draft> :_1) -> Record<Published> :_1
  effects: database.write, audit.write, network.send
{
  let r1 = submit_for_review(r)
  let r2 = approve(r1)     -- declassifies summary
  publish(r2)               -- summary is now Public, OK
}

-- MUST REJECT A08001: diagnosis is Restricted, can't go to Public
fn bad5(r: Record<Approved> :_1) -> String @Public
  effects: pure
{ r.diagnosis }

-- MUST REJECT A06001: can't publish from InReview (skip approve)
fn bad5b(r: Record<InReview> :_1) -> Record<Published> :_1
  effects: database.write, network.send
{ publish(r) }

Test Case 6: Dependent + Effect (Sized IO)

Scenario: A function that reads exactly n bytes from a stream, where n is a dependent index.

fn read_exact(
    stream: InputStream :_omega,
    n: Nat
) -> Vec<Byte, n>
  effects: io.read
  ensures { len(result) == n }

fn read_header(stream: InputStream :_omega) -> Header
  effects: io.read
{
  let magic: Vec<Byte, 4> = read_exact(stream, 4)
  requires { magic == [0x89, 0x50, 0x4E, 0x47] }  -- PNG magic

  let length_bytes: Vec<Byte, 4> = read_exact(stream, 4)
  let length: Nat = parse_u32(length_bytes)

  let data: Vec<Byte, length> = read_exact(stream, length)
  -- `length` is a runtime value used as a dependent index!

  Header { magic, length, data }
}

The problem: length is a runtime value obtained from IO, but it’s used as a dependent type index in Vec<Byte, length>. The type checker must:

1. Accept length as a valid Nat index (it came from parse_u32, which returns Nat)
2. Track that read_exact(stream, length) returns Vec<Byte, length>
3. NOT try to statically verify the exact value of length (it’s runtime-determined)

Interaction rule: Dependent indices that come from effectful computations are treated as abstract at the type level. The type checker knows length: Nat but not its value. Index arithmetic (n + m) works abstractly. Refinement predicates on the index can be verified only at runtime (they generate debug_assert).

Test:

-- MUST COMPILE: abstract index from IO
fn test6(stream: InputStream :_omega) -> Vec<Byte, n>
  effects: io.read
{
  let n: Nat = read_u32(stream)
  read_exact(stream, n)
}

-- MUST REJECT A03006: index mismatch (4 != 8)
fn bad6() -> Vec<Byte, 8>
  effects: pure
{
  let v: Vec<Byte, 4> = [1, 2, 3, 4]
  v  -- returns Vec<Byte, 4> but declared Vec<Byte, 8>
}

Test Case 7: Linear + Information Flow (Secret Key Protocol)

Scenario: A cryptographic signing protocol where the private key is both linear (use once then zeroize) AND restricted (must not leak).

fn sign_once(
    key: PrivateKey @Restricted :_1,
    message: Bytes @Public
) -> Signature @Public
  effects: crypto.sign
  ensures { verify(result, message, key.public_key()) }
{
  let sig = crypto_sign(key, message)
  -- key is consumed (linear) AND restricted (info flow)
  -- sig is Public (declassified output of restricted operation)
  zeroize(key)  -- key memory zeroed after use
  sig
}

The problem: The key is simultaneously:

• Linear (grade 1): must be consumed exactly once
• Restricted: must not flow to public sinks

The function produces a Signature @Public from a @Restricted key. This is a declassification: the SIGNATURE is public, but the KEY is not. The type checker must verify:

1. key is used exactly once (linear check)
2. key never flows to a public sink (info flow check)
3. The output sig is correctly labeled @Public (it’s derived from the key, but the signing operation is a valid declassification)

Interaction rule: Linearity and information flow are orthogonal axes. A value has both a grade AND a label. The grade tracks how many times it’s used; the label tracks where it can flow. A declassify does not change the grade. Consuming a linear value does not change its label.

Test:

-- MUST COMPILE: key used once, output correctly declassified
fn test7(key: PrivateKey @Restricted :_1, msg: Bytes @Public)
    -> Signature @Public
  effects: crypto.sign
{ sign_once(key, msg) }

-- MUST REJECT A05001 + A08001: key used twice AND leaked
fn bad7(key: PrivateKey @Restricted :_1) -> PrivateKey @Public
  effects: pure
{ key }  -- A08001: Restricted -> Public flow
         -- AND key is consumed by return, but if we tried to use
         -- it again, A05001 would fire

-- MUST REJECT A08002: key bytes logged
fn bad7b(key: PrivateKey @Restricted :_1) -> Unit
  effects: log.info
{
  log("Key bytes: " ++ key.to_string())  -- A08001: Restricted in Public log
  zeroize(key)
}

Test Case 8: Typestate + Effect + Refinement (Three-Way)

Scenario: A payment processor where state transitions require specific effects and are guarded by refinement predicates.

service PaymentProcessor {
  type Payment<State> {
    amount: Money<USD>,
    retries: Nat,
    last_error: String?
  }
  where State in {Pending, Charging, Charged, Failed, Refunded}

  fn charge(
      p: Payment<Pending> :_1
  ) -> Payment<Charged> :_1 | Payment<Failed> :_1
    requires { p.amount > Money.zero() }
    effects: payment.charge, log.info, database.write

  fn retry(
      p: Payment<Failed> :_1
  ) -> Payment<Pending> :_1
    requires { p.retries < 3 }
    ensures  { result.retries == p.retries + 1 }
    effects: database.write

  fn refund(
      p: Payment<Charged> :_1
  ) -> Payment<Refunded> :_1
    requires { p.amount > Money.zero() }
    effects: payment.refund, database.write, audit.write
}

The problem: Three features interact simultaneously:

1. Typestate: charge only from Pending, retry only from Failed, refund only from Charged
2. Refinement: retry only if retries < 3 (prevents infinite retry loops)
3. Effect: refund requires audit.write (audit trail), which charge does not

The type checker must verify all three independently and then compose the results. A retry loop must be provably bounded:

-- MUST COMPILE: bounded retry loop with all three checks
fn charge_with_retry(p: Payment<Pending> :_1)
    -> Payment<Charged> :_1 | Payment<Failed> :_1
  requires { p.retries == 0 }
  effects: payment.charge, log.info, database.write
{
  match charge(p) {
    Charged(result) => Charged(result),
    Failed(failed) => {
      if failed.retries < 3 {
        let retried = retry(failed)  -- Failed -> Pending
        charge_with_retry(retried)   -- recursive, but bounded
      } else {
        Failed(failed)
      }
    }
  }
}

Interaction rule: The type checker handles this as:

• Layer 0: typestate (DFA transitions valid), linearity (each payment consumed once per branch), effect (set containment)
• Layer 1: refinement (retries < 3 guard ensures bounded recursion)
• The decreases 3 - p.retries annotation proves termination

Test Case 9: All Six Features (Full Stack)

Scenario: A secure data pipeline that processes sensitive records with exact resource management.

service SecurePipeline {
  type Record<State> {
    id: Uuid,
    data: Bytes @Restricted,
    processed_chunks: Nat,
    total_chunks: Nat
  }
  where State in {Received, Validating, Processing, Complete, Failed}

  fn process_chunk(
      record: Record<Processing> :_1,
      chunk_index: {i: Nat | i == record.processed_chunks
                          and i < record.total_chunks},
      encryption_key: AESKey @Restricted :_1
  ) -> Record<Processing> :_1
    requires { chunk_index < record.total_chunks }
    ensures  { result.processed_chunks == record.processed_chunks + 1 }
    effects: database.write, crypto.encrypt
    privacy: record.data purpose {processing, storage}
  {
    -- 1. TYPESTATE: record must be in Processing state
    -- 2. REFINEMENT: chunk_index must equal processed_chunks
    --    and be less than total_chunks
    -- 3. DEPENDENT: processed_chunks is a Nat index that
    --    tracks progress toward total_chunks
    -- 4. LINEAR: encryption_key used exactly once per chunk
    -- 5. EFFECT: only database.write and crypto.encrypt allowed
    -- 6. INFO FLOW: record.data is @Restricted, must not leak
    --    to logs or public outputs

    let encrypted = encrypt(encryption_key, record.data.chunk(chunk_index))
    -- key consumed (linear), data stays Restricted (info flow)

    let updated = record.with_processed_chunks(record.processed_chunks + 1)
    -- dependent index incremented

    updated
  }

  fn process_all(
      record: Record<Validating> :_1,
      keys: Vec<AESKey @Restricted :_1, record.total_chunks>
  ) -> Record<Complete> :_1
    requires { record.total_chunks > 0 }
    requires { len(keys) == record.total_chunks }
    ensures  { result.processed_chunks == record.total_chunks }
    effects: database.write, crypto.encrypt
    decreases record.total_chunks - record.processed_chunks
  {
    let r = transition(record, Processing)
    process_loop(r, keys, 0)
  }

  fn process_loop(
      record: Record<Processing> :_1,
      keys: Vec<AESKey @Restricted :_1, n>,
      i: {x: Nat | x <= n}
  ) -> Record<Complete> :_1
    requires { i == record.processed_chunks }
    requires { n == record.total_chunks }
    effects: database.write, crypto.encrypt
    decreases n - i
  {
    if i == record.total_chunks {
      transition(record, Complete)
    } else {
      let (key, remaining_keys) = keys.pop_first()
      -- key is linear: popped from vector, used once
      let updated = process_chunk(record, i, key)
      process_loop(updated, remaining_keys, i + 1)
    }
  }
}

What this tests simultaneously:

What can go wrong:

1. The SMT query for the loop invariant (i == processed_chunks AND i < total_chunks AND remaining_keys.len == total_chunks - i) involves quantified arithmetic over dependent indices. This could time out.

2. The linear key vector Vec<AESKey :_1, n> means each element is linear. Popping an element consumes it from the vector. The type checker must track that the vector’s length decreases by 1 each iteration AND that the popped key is consumed.

3. The decreases n - i termination measure involves both a refinement value (i) and a dependent index (n). The type checker must unify these two systems to verify termination.

Test Case 10: Conditional Typestate (Branch Divergence)

Scenario: An operation that may transition to different states depending on runtime data.

fn process_order(order: Order<Paid> :_1, inventory: Inventory)
    -> Order<Shipped> :_1 | Order<Cancelled> :_1
  effects: database.write, logistics.dispatch
{
  if inventory.has_stock(order.items) {
    let tracking = logistics.create_shipment(order)
    ship(order, tracking)  -- Paid -> Shipped
  } else {
    cancel(order, "Out of stock")  -- Paid -> Cancelled
  }
}

The problem: After the if/else, the order is in DIFFERENT states in each branch. The return type must be a union Order<Shipped> | Order<Cancelled>. The type checker must:

1. Track each branch independently
2. Join the typestate contexts
3. Verify the caller handles both possible states

Test:

-- MUST COMPILE: caller handles both branches
fn handle(order: Order<Paid> :_1, inv: Inventory) -> String
  effects: database.write, logistics.dispatch, email.send
{
  match process_order(order, inv) {
    Shipped(o) => {
      send_tracking_email(o)
      "Shipped"
    }
    Cancelled(o) => {
      send_cancellation_email(o)
      "Cancelled"
    }
  }
}

-- MUST REJECT A10001: non-exhaustive match (missing Cancelled)
fn bad10(order: Order<Paid> :_1, inv: Inventory) -> String
  effects: database.write, logistics.dispatch
{
  match process_order(order, inv) {
    Shipped(o) => "Shipped"
    -- Missing Cancelled case!
  }
}

Test Case 11: Effect + Information Flow (Labeled Effects)

Scenario: A logging system where the log effect has a security label, preventing sensitive data from being logged.

fn process_user(user: User) -> ProcessingResult
  effects: database.write, log.info @Public
{
  log.info("Processing user: " ++ user.id)          -- OK: id is Public
  log.info("User email: " ++ user.email)             -- A08002: email is @Internal
  log.info("User SSN: " ++ user.ssn)                 -- A08002: ssn is @Restricted

  let result = compute(user)
  log.info("Result: " ++ result.summary)              -- OK if summary is @Public
  result
}

The problem: The log.info effect is annotated @Public, meaning it can only receive data labeled @Public or lower. When a @Restricted value (user.ssn) is passed to a @Public effect, the compiler must reject it.

Interaction rule: Each effect in the effect row carries a maximum security label. Data flowing into an effect must have a label at or below the effect’s label. This is checked by combining the effect row check (layer 0) with the information flow check (layer 1).

Summary: Interaction Matrix

Implementation Priority

For the compiler prototype, implement interactions in this order:

1. Linear + Typestate (easiest: typestate requires linearity)
2. Linear + Effect (common: resource-scoped effects)
3. Refinement + Dependent (core value: index safety)
4. Effect + Info Flow (core value: preventing PII leaks)
5. Refinement + Linear (ghost use rule)
6. Typestate + Refinement (guarded transitions)
7. Dependent + Effect (abstract indices from IO)
8. Typestate + Info Flow (label transitions)
9. Three-way combinations (after pairwise is solid)
10. Full stack (integration test, last)

Each test case above serves as both a specification and a regression test. When the type checker handles all 11 cases correctly, the interaction problem is solved.

14. Verification Categories

The base language (Sections 1-13) handles application-level services. These categories add domain-specific verification capabilities organized by concern. A project selects which categories to activate via the profile system (Section 1.2).

CORE is always active. All others are opt-in.

14.CORE: Verification Infrastructure

Always active. Cannot be excluded from any profile.

CORE.1 Ghost Code

Variables, functions, and blocks that exist only for verification. They are type-checked, verified by SMT, but completely erased from the generated Rust code. Zero runtime cost.

Motivation

Every mature verification tool has ghost code: SPARK Ada (Ghost aspect), Dafny (ghost var, ghost method), Verus (proof fn, tracked), Creusot (#[logic]). The reason is fundamental: verification often requires tracking state that the runtime code does not need.

Examples from other Assura features:

• Monotonic state (STOR.5): needs to remember the previous value to verify new >= old, but the runtime only needs the current value
• Bit-level format (FMT.2): the bit cursor position is a verification concept; the runtime tracks it implicitly via byte_pos + bit_offset
• Multi-pass refinement (TEST.3): quality measurement exists only to prove convergence, not for runtime behavior
• Page cache (STOR.2): pin count invariants need logical tracking of which pages are pinned by whom

Without ghost code, these verification-only values must be embedded in the runtime code behind #[cfg(debug_assertions)], which conflates debugging and verification.

Grammar

GhostDecl   = 'ghost' GhostItem ;

GhostItem   = 'var' Ident ':' TypeExpr ['=' Expr]
            | 'fn' FnDecl
            | 'type' TypeDecl
            | '{' StmtList '}' ;

GhostAttr   = '#[ghost]' ;

Full Example

type SortedList<T: Ord> {
  data: Vec<T>,

  // Ghost: the abstract sequence for verification
  ghost var elements: Sequence<T>,

  invariant {
    // Runtime data and ghost sequence are in sync
    data.len() == elements.len(),
    for_all(i in 0..data.len(), data[i] == elements[i]),
    // Sortedness expressed on the ghost sequence
    for_all(i in 0..elements.len()-1,
      elements[i] <= elements[i+1]
    )
  }
}

fn insert(list: &mut SortedList<T>, value: T)
  ensures {
    // Ghost sequence has the new element
    list.elements == old(list.elements).insert_sorted(value)
  }
{
  let pos = list.data.binary_search(&value)
    .unwrap_or_else(|p| p)
  list.data.insert(pos, value)

  // Ghost: update the logical sequence
  ghost { list.elements = list.elements.insert_sorted(value) }
}

// Ghost function: pure mathematical definition
ghost fn insert_sorted(seq: Sequence<T>, val: T) -> Sequence<T>
  ensures {
    result.len() == seq.len() + 1,
    result.contains(val),
    is_sorted(result)
  }
{
  // This body is verified but never compiled
  let pos = seq.find_insertion_point(val)
  seq.insert_at(pos, val)
}

// Using ghost blocks for verification state
fn binary_search(arr: &[I32], target: I32) -> Option<U32>
  requires { is_sorted(arr) }
  ensures {
    match result {
      Some(idx) => arr[idx] == target,
      None => for_all(i in 0..arr.len(), arr[i] != target)
    }
  }
{
  let mut lo: U32 = 0
  let mut hi: U32 = arr.len() as U32

  while lo < hi
    invariant {
      lo <= hi && hi <= arr.len() as U32,
      for_all(i in 0..lo, arr[i] < target),
      for_all(i in hi..arr.len() as U32, arr[i] > target)
    }
  {
    let mid = lo + (hi - lo) / 2
    if arr[mid] < target {
      lo = mid + 1
    } else if arr[mid] > target {
      hi = mid
    } else {
      return Some(mid)
    }

    // Ghost: track iteration for termination
    ghost {
      assert hi - lo < old(hi) - old(lo)
        // proves the loop terminates
    }
  }
  None
}

Verification Rule

1. Erasure guarantee: Ghost code cannot affect runtime behavior. Ghost variables cannot appear in non-ghost expressions. Ghost functions cannot be called from non-ghost code. Violations produce A54001
2. Type checking: Ghost code is fully type-checked using the same rules as runtime code
3. SMT inclusion: Ghost assertions and invariants are included in the SMT query. Ghost function bodies are available for inlining by the solver
4. Ghost purity: Ghost functions must be pure (no effects). Ghost variables can only be modified inside ghost blocks

Error Codes

Rust Codegen

Ghost code is completely erased:

#![allow(unused)]
fn main() {
// Assura:
//   ghost var elements: Sequence<T>
//   ghost { elements = elements.insert_sorted(value) }
//
// Rust: (nothing generated)

// Ghost assertions become debug_assert in debug mode only
#[cfg(debug_assertions)]
{
    debug_assert!(is_sorted(&list.data));
}
}

CORE.2 Lemmas and Proof Functions

Functions that prove properties but generate no runtime code. They exist to help the SMT solver establish facts that are needed by other contracts.

Motivation

SMT solvers are powerful but not omniscient. Sometimes the solver cannot prove a property directly but can verify it if given an intermediate step. Lemmas provide those steps.

Examples:

• Proving a sort is correct requires transitivity of comparison
• Proving a hash table has no collisions requires properties of the hash function
• Proving a balanced tree stays balanced after rotation requires height relationships

Dafny has lemma, Verus has proof fn, Lean has theorem. Without lemmas, Assura must either hope the SMT solver can prove everything automatically (it often cannot) or encode hints in awkward ways.

Grammar

LemmaDecl   = 'lemma' Ident ['<' TypeParams '>']
              '(' ParamList ')'
              RequiresClause
              EnsuresClause
              [LemmaBody] ;

LemmaBody   = '{' { LemmaStep } '}' ;

LemmaStep   = 'assert' Predicate
            | 'apply' LemmaIdent '(' ArgList ')'
            | 'induction' Ident
            | 'cases' Ident '{' { CaseArm } '}' ;

Full Example

// Lemma: if a list is sorted and we insert in the right
// position, the result is still sorted
lemma insert_preserves_sorted<T: Ord>(
    seq: Sequence<T>,
    val: T,
    pos: U32
)
  requires {
    is_sorted(seq),
    pos <= seq.len(),
    pos == 0 || seq[pos - 1] <= val,
    pos == seq.len() || val <= seq[pos]
  }
  ensures {
    is_sorted(seq.insert_at(pos, val))
  }
{
  // Proof by cases on the elements around the insertion point
  assert for_all(i in 0..pos,
    seq[i] <= val  // all before pos are <= val
  )
  assert for_all(i in pos..seq.len(),
    val <= seq[i]  // all after pos are >= val
  )
  // SMT can now derive sortedness of the result
}

// Lemma: transitivity of comparison (helps sort proofs)
lemma comparison_transitive<T: Ord>(a: T, b: T, c: T)
  requires { a <= b && b <= c }
  ensures { a <= c }
  // No body needed: SMT handles this directly

// Lemma: CRC32 distributes over concatenation
// (needed for chunked integrity verification)
lemma crc32_concat(data_a: &[U8], data_b: &[U8])
  requires { true }
  ensures {
    crc32(concat(data_a, data_b)) ==
      crc32_combine(crc32(data_a), crc32(data_b), data_b.len())
  }
{
  induction data_b
  // Base case: data_b is empty
  //   crc32(concat(a, [])) == crc32(a) == crc32_combine(crc32(a), 0, 0)
  // Inductive step: data_b = [head] ++ tail
  //   apply crc32_concat(data_a, tail)
  //   assert crc32(concat(a, [head]++tail)) == ...
}

// Using a lemma in a function contract
fn merge_sorted(a: &[I32], b: &[I32]) -> Vec<I32>
  requires { is_sorted(a) && is_sorted(b) }
  ensures { is_sorted(result) && result.len() == a.len() + b.len() }
{
  // ... merge logic ...

  // Invoke lemma to help the solver
  apply insert_preserves_sorted(partial_result, next_val, insert_pos)
}

Verification Rule

1. No runtime effect: Lemmas generate no code. They exist only as proof obligations for the SMT solver
2. Must be valid: The solver must be able to verify the lemma itself (the ensures follows from the requires + body)
3. Can be applied: apply lemma_name(args) adds the lemma’s ensures clause as an assumption at that point in the proof
4. Induction support: induction var generates the base case and inductive step for structural induction on var

Error Codes

Rust Codegen

Lemmas are completely erased. No runtime code is generated.

#![allow(unused)]
fn main() {
// Assura:
//   lemma insert_preserves_sorted(...) { ... }
//   apply insert_preserves_sorted(partial, val, pos)
//
// Rust: (nothing generated for either declaration or application)
}

CORE.3 Frame Conditions

Explicit declarations of which state a function modifies, enabling the verifier to prove that everything else is unchanged.

Motivation

Assura’s effects system (Section 3) tracks what kind of side effects occur (filesystem, database, network). But it does not track WHICH specific variables or fields change. Frame conditions fill this gap.

Without frame conditions, the verifier must assume a function call could modify anything. This makes modular verification impossible: proving a property about variable X is useless if the next function call might silently change X.

SPARK Ada has Global and Depends aspects. Frama-C has assigns clauses. Dafny has modifies clauses. All of them learned that frame conditions are essential for scalable verification.

Grammar

FrameClause   = 'modifies' '{' ModifiesTarget
                  { ',' ModifiesTarget } '}'
              | 'reads' '{' ReadsTarget
                  { ',' ReadsTarget } '}' ;

ModifiesTarget = Ident
               | Ident '.' FieldIdent
               | Ident '[' Expr ']'
               | '*' Ident  // all fields of the object ;

ReadsTarget    = Ident
               | Ident '.' FieldIdent
               | '*' Ident ;

Full Example

type BTreeNode {
  keys: Vec<I64>,
  children: Vec<BTreeNode>,
  count: U32,
  parent: Option<&BTreeNode>,
}

// Frame condition: only modifies the node's keys and count
fn insert_key(
    node: &mut BTreeNode,
    key: I64,
    pos: U32
)
  modifies { node.keys, node.count }
  // Implicit: node.children and node.parent are UNCHANGED
  requires { pos <= node.count }
  ensures {
    node.count == old(node.count) + 1,
    node.keys[pos] == key,
    // children unchanged (guaranteed by frame condition)
    node.children == old(node.children)
  }
{
  node.keys.insert(pos as usize, key)
  node.count += 1
}

// Frame condition on a struct field
type PageCache {
  pages: HashMap<U32, Page>,
  dirty_set: HashSet<U32>,
  stats: CacheStats,
}

fn mark_dirty(cache: &mut PageCache, page_id: U32)
  modifies { cache.dirty_set, cache.stats }
  // pages themselves are NOT modified
  requires { cache.pages.contains_key(page_id) }
  ensures {
    cache.dirty_set.contains(page_id),
    cache.pages == old(cache.pages)  // frame: pages unchanged
  }
{
  cache.dirty_set.insert(page_id)
  cache.stats.dirty_count += 1
}

// reads clause: function only reads these fields
fn lookup(cache: &PageCache, page_id: U32) -> Option<&Page>
  reads { cache.pages }
  // Does not read dirty_set or stats
  ensures {
    result.is_some() == cache.pages.contains_key(page_id)
  }
{
  cache.pages.get(&page_id)
}

Verification Rule

1. Write restriction: If modifies { a, b } is declared, the function body can only assign to a and b. Writing to any other state is a compile error
2. Frame inference: For any variable NOT in the modifies set, the verifier adds an implicit ensures { x == old(x) }
3. Callee frames: When a function with modifies { x } calls another function with modifies { y }, the verifier checks that y is a subset of x or that y is local state
4. Read restriction: If reads { a } is declared, the function body can only read from a. This enables the verifier to skip tracking changes to other fields

Error Codes

Rust Codegen

Frame conditions are erased (compile-time only). In debug mode, they generate field-level change tracking:

#![allow(unused)]
fn main() {
#[cfg(debug_assertions)]
{
    let old_children = node.children.clone();
    // ... function body ...
    debug_assert_eq!(node.children, old_children,
        "frame violation: children modified");
}
}

CORE.4 Axiomatic Definitions

Abstract mathematical definitions that the verifier uses for reasoning without requiring an implementation. They define WHAT something means, not HOW to compute it.

Motivation

Some concepts are easier to define mathematically than to implement:

• “A sequence is sorted” is a one-line mathematical definition but a multi-line runtime check
• “Two sets are disjoint” is trivial in math but requires iteration at runtime
• “A tree is balanced” has a clean recursive definition but a complex imperative check

Axioms let the verifier reason about these concepts directly without needing executable code. Frama-C has axiomatic blocks. Dafny has predicate and function (which can be ghost). Why3 has axiom.

Grammar

AxiomDecl     = 'axiom' Ident ['<' TypeParams '>']
                '(' ParamList ')' ':' TypeExpr
                '=' AxiomBody ;

AxiomBody     = Predicate
              | '{' { AxiomClause } '}' ;

AxiomClause   = 'define' ':' Predicate
              | 'property' ':' Predicate ;

Full Example

// Axiom: what "sorted" means
axiom is_sorted<T: Ord>(seq: Sequence<T>) : Bool =
  for_all(i in 0..seq.len()-1, seq[i] <= seq[i+1])

// Axiom: what "permutation" means
axiom is_permutation<T>(a: Sequence<T>, b: Sequence<T>) : Bool = {
  define: a.len() == b.len()
       && for_all(x: T, a.count(x) == b.count(x))
}

// Axiom: what a valid B-tree is
axiom is_valid_btree(node: BTreeNode, order: U32) : Bool = {
  define:
    // Keys are sorted within each node
    is_sorted(node.keys)
    // Number of children = number of keys + 1 (for internal nodes)
    && (node.is_leaf() || node.children.len() == node.keys.len() + 1)
    // All keys in left subtree < key < all keys in right subtree
    && for_all(i in 0..node.keys.len(),
         (i == 0 || all_less(node.children[i], node.keys[i]))
         && (i == node.keys.len() - 1
             || all_greater(node.children[i+1], node.keys[i]))
       )
    // Recursively valid
    && for_all(child in node.children, is_valid_btree(child, order))

  property:
    // All leaves are at the same depth
    for_all(leaf_a in leaves(node), leaf_b in leaves(node),
      depth(leaf_a) == depth(leaf_b)
    )
}

// Using axioms in contracts
fn sort(data: &mut [I32])
  ensures {
    is_sorted(result),
    is_permutation(old(data).to_seq(), result.to_seq())
  }
{
  // ... sorting implementation ...
}

fn btree_insert(tree: &mut BTree, key: I64)
  requires { is_valid_btree(tree.root, tree.order) }
  ensures { is_valid_btree(tree.root, tree.order) }
{
  // ... insertion logic ...
}

Verification Rule

1. No runtime evaluation: Axioms are never executed. They exist only in the SMT domain
2. Consistency: The verifier checks that axiom definitions are not contradictory (e.g., axiom absurd() : Bool = true && false)
3. Totality: Recursive axioms must be well-founded (they must terminate on all inputs). The verifier checks structural decrease or explicit fuel bounds
4. Properties: property clauses are additional facts the verifier must prove follow from the define clause

Error Codes

Rust Codegen

Axioms are completely erased. In debug mode, simple axioms generate runtime checks:

#![allow(unused)]
fn main() {
// Simple axiom: can generate a runtime check
#[cfg(debug_assertions)]
fn debug_is_sorted(seq: &[i32]) -> bool {
    seq.windows(2).all(|w| w[0] <= w[1])
}

// Complex axiom (recursive, quantified): no runtime check possible
// Verified purely at compile time via SMT
}

CORE.5 Quantifier Triggers

Hints that tell the SMT solver how to instantiate universal quantifiers. Without them, the solver either times out or explores an exponential search space.

Motivation

Universal quantifiers (for_all) are the most common source of SMT solver timeouts. When the solver sees for_all(x: T, P(x)), it must decide which concrete values of x to try. Without guidance, it may try none (proof fails) or too many (timeout).

Verus and Dafny both have explicit trigger syntax because they learned this is practically essential. Triggers tell the solver: “when you see an expression matching this pattern, instantiate the quantifier with the matching value.”

This is an implementation concern, not a mathematical one. But without it, real verification systems hit timeout walls on moderate-size programs.

Grammar

TriggerClause  = '#[trigger' '(' TriggerPattern
                   { ',' TriggerPattern } ')' ']' ;

TriggerPattern = Expr ;  // expression pattern the solver matches

AutoTrigger    = '#[auto_trigger]' ;  // let the solver choose

Full Example

// Without trigger: solver may time out on large arrays
fn lookup_correct(table: &HashMap<K, V>, key: K) -> Option<V>
  ensures {
    // Trigger: when the solver sees table.get(k) for any k,
    // it should instantiate this quantifier with that k
    #[trigger(table.get(x))]
    for_all(x: K,
      result == table.get(key)
    )
  }

// Sorted array: trigger on array access
fn binary_search_spec(arr: &[I32], target: I32) -> Option<U32>
  requires {
    // Trigger: when the solver sees arr[i], instantiate with
    // that i
    #[trigger(arr[i])]
    for_all(i in 0..arr.len()-1, arr[i] <= arr[i+1])
  }

// Multiple triggers: instantiate when EITHER pattern matches
lemma map_preserves_length<T, U>(
    seq: Sequence<T>,
    f: fn(T) -> U
)
  ensures {
    #[trigger(seq[i], mapped[i])]
    for_all(i in 0..seq.len(),
      mapped[i] == f(seq[i])
    )
    && mapped.len() == seq.len()
  }

// Auto-trigger: let the solver choose (simpler but less reliable)
fn contains_all(subset: &[I32], superset: &[I32]) -> Bool
  ensures {
    #[auto_trigger]
    for_all(x in subset, superset.contains(x))
  }

Verification Rule

1. Trigger validity: Trigger patterns must mention the bound variable of the quantifier. A trigger that does not reference the quantified variable is useless (A58001)
2. Trigger coverage: The trigger must be specific enough to avoid matching loops (where instantiation creates new matches). The verifier warns on potential matching loops (A58002)
3. Auto-trigger fallback: If no trigger is specified and #[auto_trigger] is not present, the verifier uses Z3/CVC5’s built-in heuristic but warns that explicit triggers are recommended for reliability
4. Multi-trigger: Multiple trigger patterns create a conjunction: the quantifier is instantiated only when ALL patterns match simultaneously

Error Codes

Rust Codegen

Triggers are erased (they are SMT directives, not runtime code).

#![allow(unused)]
fn main() {
// Triggers affect only the verification pass.
// No Rust code is generated for trigger annotations.
}

CORE.6 Opaque Functions

Functions whose implementation is hidden from the verifier. The solver reasons only about the function’s contract (requires/ ensures), not its body. This prevents the solver from unfolding complex or recursive definitions and timing out.

Motivation

When the verifier encounters a function call, it can either:

1. Inline the function body (precise but expensive)
2. Use only the contract (fast but requires good contracts)

By default, the solver tries to inline, which causes problems:

• Recursive functions cause infinite unfolding
• Complex functions cause exponential blowup
• Implementation details leak into callers’ proofs, creating fragile verification that breaks when internals change

Dafny has opaque functions. Verus has open/closed specs. SPARK Ada uses Refined_Post to separate interface from body contracts. The pattern is universal: hide what you do not need to expose.

Grammar

OpaqueAttr    = '#[opaque]' ;

RevealStmt    = 'reveal' FnIdent ;
              // temporarily expose the body at this proof point

Full Example

// Opaque: verifier sees only the contract, not the body
#[opaque]
fn fibonacci(n: U32) -> U64
  requires { n <= 93 }  // fits in u64
  ensures {
    n == 0 => result == 0,
    n == 1 => result == 1,
    n >= 2 => result == fibonacci(n - 1) + fibonacci(n - 2)
  }
{
  // Iterative implementation (efficient)
  // Verifier does NOT see this; it uses the ensures clause
  let mut a: U64 = 0
  let mut b: U64 = 1
  for _ in 0..n {
    let temp = a + b
    a = b
    b = temp
  }
  a
}

// Caller: verifier uses only fibonacci's contract
fn fib_is_monotonic(a: U32, b: U32) -> Bool
  requires { a <= b && b <= 93 }
  ensures { fibonacci(a) <= fibonacci(b) }
{
  // Cannot prove this from contract alone; reveal the body
  reveal fibonacci
  // Now the verifier can unfold fibonacci's definition
  // (with fuel bounds to prevent infinite recursion)

  // ... inductive proof ...
  true
}

// Opaque type: hide internal representation
#[opaque]
type BloomFilter {
  bits: Vec<U64>,
  hash_count: U8,
  // Verifier cannot see these fields from outside
}

// Public contract: does not expose internal representation
fn bloom_insert(filter: &mut BloomFilter, item: &[U8])
  ensures { bloom_may_contain(filter, item) == true }

#[opaque]
fn bloom_may_contain(filter: &BloomFilter, item: &[U8]) -> Bool
  ensures {
    // False positives possible, false negatives impossible
    // (this is the ONLY fact callers can rely on)
  }

Verification Rule

1. Body hidden: When verifying callers of an opaque function, the solver uses only the requires/ensures contract. The function body is not available for inlining
2. Body verified separately: The opaque function itself is verified: its body must satisfy its ensures clause. This happens once, not at every call site
3. Reveal: reveal fn_name temporarily exposes the function body at a specific proof point. The verifier adds fuel bounds to prevent infinite unfolding of recursive functions
4. Modular verification: Opaque functions enable modular verification. Changing the body of an opaque function does not require re-verifying callers (as long as the contract is unchanged)

Error Codes

Rust Codegen

Opacity is a verification concept only. The generated Rust code is identical whether the function is opaque or not:

#![allow(unused)]
fn main() {
// Opaque functions generate normal Rust code.
// The opacity only affects the verification pass.
pub fn fibonacci(n: u32) -> u64 {
    let mut a: u64 = 0;
    let mut b: u64 = 1;
    for _ in 0..n {
        let temp = a + b;
        a = b;
        b = temp;
    }
    a
}
}

CORE.7 Prophecy Variables

Ghost variables determined by future events, not past state. Standard ghost variables (CORE.1) are history variables: their value is computed from the current and past program state. Prophecy variables have a value that is declared now but resolved later, enabling specification of properties that depend on how the execution will proceed.

Motivation

Lock-free data structures with helping mechanisms (Michael-Scott queue, Harris linked list, elimination stack) have non-fixed linearization points: the point where an operation logically takes effect may be inside ANOTHER thread’s code. Proving linearizability of these algorithms requires specifying “operation A linearizes at the point where thread B completes the help,” which is unknown when A starts.

Without prophecy variables, you can only verify algorithms with fixed linearization points (e.g., Treiber stack, where the LP is always the successful CAS). This excludes the most widely deployed lock-free data structures.

Syntax

// Declare a prophecy: value unknown now
ghost prophecy lp: ProgramPoint

// Constrain the prophecy (optional, narrows valid assignments)
ghost prophecy choice: {v: Nat | v < queue.len()}

// Resolve: fix the prophecy's value at this execution point
resolve lp = here
resolve choice = selected_index

// The verifier checks: for every execution, there EXISTS
// a valid prophecy assignment satisfying all constraints
// and all postconditions that reference the prophecy

Example: Michael-Scott Queue Dequeue

fn dequeue(q: &MichaelScottQueue<T>) -> Option<T> {
  ghost prophecy lp: ProgramPoint
  ghost prophecy result_val: Option<T>

  loop {
    let head = q.head.load(acquire)
    let next = head.next.load(acquire)

    if next.is_null() {
      resolve result_val = None
      resolve lp = here
      return None
    }

    let val = next.data
    if q.head.compare_exchange(head, next, acq_rel).is_ok() {
      resolve result_val = Some(val)
      resolve lp = here  // LP is THIS thread's CAS
      return Some(val)
    }
    // CAS failed: another thread helped. LP might be in
    // the other thread's code. Prophecy remains unresolved
    // for this iteration; loop retries.
  }
}
ensures result == result_val  // result matches prophecy
ensures linearized_at(lp)     // LP is between invoke and return

When thread B helps thread A’s dequeue, the prophecy lp for A’s operation resolves inside B’s code path. The verifier checks that for every interleaving, there exists a valid assignment of all prophecy variables such that the sequential specification holds.

Verification Rule

1. Existential check: For each prophecy variable P, the verifier introduces an existential quantifier: exists P: constraints(P) && postconditions_hold(P)
2. Resolution obligation: Every prophecy must be resolved on every execution path. A-CORE-025 fires if an unresolved prophecy reaches function exit
3. Single resolution: Each prophecy is resolved exactly once. A-CORE-026 fires on double resolution
4. Layer 2: Prophecy verification runs at Layer 2 (bounded SMT, <10s). The existential quantifier is handled via Skolemization or counterexample-guided synthesis
5. Interaction with CORE.1: Prophecy variables can be read by ghost code and used in postconditions, lemmas, and axiomatic definitions, just like history ghost variables

Error Codes

Rust Codegen

Prophecy variables are verification-only. No runtime code is generated. The resolved value exists only in the proof:

#![allow(unused)]
fn main() {
// Source Assura has: ghost prophecy lp: ProgramPoint
// Generated Rust: nothing. Prophecies are erased.
fn dequeue(q: &MichaelScottQueue<T>) -> Option<T> {
    loop {
        let head = q.head.load(Ordering::Acquire);
        let next = unsafe { (*head).next.load(Ordering::Acquire) };
        if next.is_null() {
            return None;
        }
        let val = unsafe { (*next).data };
        if q.head.compare_exchange(
            head, next, Ordering::AcqRel, Ordering::Acquire
        ).is_ok() {
            return Some(val);
        }
    }
}
}

CORE.8 Liveness Contracts

Properties that assert something good eventually happens: a leader is eventually elected, a request is eventually served, a stuck process eventually recovers. These complement safety properties (bad things never happen) with progress guarantees.

Motivation

Safety verification proves your system never does something wrong. But a system that does nothing at all is trivially safe. Liveness proves the system eventually does something right. Critical examples:

• Raft consensus: “A leader is eventually elected after partition recovery” (without this, the cluster could stay leaderless forever)
• FreeRTOS: “The scheduler eventually dispatches every ready task” (without this, a task could starve indefinitely)
• PX4 autopilot: “The controller eventually stabilizes after a disturbance” (without this, the drone could oscillate forever)
• DNS resolver: “Every query eventually receives a response or timeout” (without this, a query could hang indefinitely)

Syntax

// Eventually: at some future point, P holds
liveness leader_election {
  assume eventually_always { network.synchronous }
  prove eventually { exists n in nodes: n.role == Leader }
}

// Leads-to: whenever P holds, Q eventually follows
liveness request_service {
  prove leads_to(
    request.state == Pending,
    request.state == Served || request.state == TimedOut
  )
}

// Bounded liveness: Q follows P within K steps
liveness bounded_election {
  assume eventually_always { network.synchronous }
  prove eventually_within(steps: 3 * num_nodes) {
    exists n in nodes: n.role == Leader
  }
}

// Fairness assumption: if action is continuously enabled,
// it is eventually taken
liveness fair_scheduler {
  assume fair { task_runnable(t) } implies eventually { task_running(t) }
  prove leads_to(
    task.state == Ready,
    task.state == Running
  )
}

Example: FreeRTOS Scheduler Progress

liveness scheduler_progress {
  // Fairness: if the tick interrupt fires, the scheduler runs
  assume fair { tick_pending }
    implies eventually { scheduler_invoked }

  // If a task is the highest-priority ready task,
  // it eventually gets the CPU
  prove leads_to(
    task.priority == max_ready_priority()
      && task.state == Ready,
    task.state == Running
  )

  // Bounded version: within 2 tick periods
  prove eventually_within(ticks: 2) {
    current_task == highest_priority_ready_task()
  }
}

Example: Raft Leader Election

liveness raft_election {
  // Partial synchrony: network eventually becomes synchronous
  assume eventually_always {
    forall m in messages:
      delivered_within(m, delta)
  }

  // A leader is eventually elected
  prove eventually {
    exists n in nodes:
      n.role == Leader
      && n.term == max(node.term for node in nodes)
  }

  // Committed entries are eventually applied
  prove leads_to(
    entry.committed,
    entry.applied
  )
}

Verification Rule

Liveness is verified via liveness-to-safety reduction (Biere et al.), which transforms liveness checking into safety checking that SMT solvers handle natively:

1. Augmentation: The verifier adds a “lasso detector” to the state space. A lasso is a finite prefix followed by a cycle. If a liveness property fails, there exists a lasso where the bad thing persists forever
2. Bounded model checking (BMC): The verifier unrolls the transition relation up to K steps and checks for lassos. If no lasso is found within K steps, the property holds up to that bound
3. K-induction (optional): For unbounded proofs, the verifier uses k-induction: if no lasso of length <= k exists AND the lasso-freedom is inductive, the property holds for all lengths. This runs at Layer 2-3 with configurable timeouts
4. Fairness encoding: assume fair constraints are encoded as compassion (strong fairness) or justice (weak fairness) requirements in the transition system. The lasso detector checks that every cycle satisfies the fairness constraints
5. Step bound K: Configurable per-project. Default K=1000. For eventually_within(steps: N), the bound is exactly N

Layer assignment:
  eventually_within  → Layer 1 (bounded, decidable, <200ms)
  eventually (BMC)   → Layer 2 (bounded K, <10s)
  eventually (k-ind) → Layer 3 (unbounded, may timeout)
  leads_to           → Layer 2-3 (depends on state space)

Error Codes

Rust Codegen

Liveness contracts are verification-only. No runtime code is generated. In debug builds, optional runtime monitors can be emitted:

#![allow(unused)]
fn main() {
// Source Assura has: prove eventually_within(ticks: 2) { ... }
// Generated Rust (debug only):
#[cfg(debug_assertions)]
fn check_liveness_scheduler() {
    static TICKS_SINCE_READY: AtomicU32 = AtomicU32::new(0);
    let ticks = TICKS_SINCE_READY.fetch_add(1, Ordering::Relaxed);
    debug_assert!(
        ticks < 2,
        "liveness: highest-priority task not scheduled within 2 ticks"
    );
}

// Release build: nothing generated. The proof guarantees progress.
}

14.MEM: Memory Safety

MEM.1 Memory Regions

Memory regions are typed, bounds-tracked views into byte buffers. They enable verified pointer arithmetic without unsafe code.

Motivation

6 of 9 recent SQLite CVEs involved buffer overflows caused by computing an offset into a page buffer without bounds checking. Example: &aData[get2byte(&aData[cellOffset + 2*iCell])] accesses a page buffer using a 2-byte big-endian offset read from within the same buffer. If the offset is out of bounds, memory corruption occurs.

Grammar

RegionType     = 'Region' '<' TypeExpr '>' ;
SliceExpr      = Expr '.' 'slice' '(' Expr ',' Expr ')' ;
RegionReadExpr = Expr '.' 'read_u8' '(' Expr ')'
               | Expr '.' 'read_u16_be' '(' Expr ')'
               | Expr '.' 'read_u32_be' '(' Expr ')'
               | Expr '.' 'read_u64_be' '(' Expr ')'
               | Expr '.' 'read_i32_be' '(' Expr ')' ;
RegionWriteExpr = Expr '.' 'write_u8' '(' Expr ',' Expr ')'
               | Expr '.' 'write_u16_be' '(' Expr ',' Expr ')'
               | Expr '.' 'write_u32_be' '(' Expr ',' Expr ')'
               | Expr '.' 'write_u64_be' '(' Expr ',' Expr ')' ;

Type System

A Region<Size> is a byte buffer of exactly Size bytes. Every read and write operation requires a refined offset proving the access is in bounds:

type Region<Size: Nat> {
  invariant { len(data) == Size }
}

fn read_u16_be(
    r: Region<n>,
    offset: {i: Nat | i + 2 <= n}
) -> {v: Nat | v < 65536}
  effects: pure

fn read_u32_be(
    r: Region<n>,
    offset: {i: Nat | i + 4 <= n}
) -> U32
  effects: pure

fn write_u16_be(
    r: Region<n> :_1,
    offset: {i: Nat | i + 2 <= n},
    value: {v: Nat | v < 65536}
) -> Region<n> :_1
  effects: pure

fn slice(
    r: Region<n>,
    start: {s: Nat | s <= n},
    len: {l: Nat | s + l <= n}
) -> Region<l>
  effects: pure

SQLite Example: Cell Pointer Access

contract CellPointerAccess {
  type PageBuffer = Region<PageSize>

  fn get_cell_offset(
      page: PageBuffer,
      cell_index: {i: Nat | i < cell_count},
      cell_pointer_offset: {c: Nat | c + 2 * cell_count <= PageSize}
  ) -> {offset: Nat | offset < PageSize}
    effects: pure
  {
    let raw = page.read_u16_be(cell_pointer_offset + 2 * cell_index)
    requires { raw < PageSize }
    -- COMPILE ERROR if raw could be >= PageSize
    -- (catches SQLite-class buffer overflow at compile time)
    raw
  }
}

Rust Codegen

Region<n> maps to &[u8] (read) or &mut [u8] (write) with debug_assert bounds checks:

#![allow(unused)]
fn main() {
pub struct Region<'a> {
    data: &'a [u8],
}

impl<'a> Region<'a> {
    pub fn read_u16_be(&self, offset: usize) -> u16 {
        debug_assert!(offset + 2 <= self.data.len());
        u16::from_be_bytes([self.data[offset], self.data[offset + 1]])
    }
}
}

The dependent size index n erases. Bounds safety is proven at compile time by the refinement checker; the debug_assert is a second safety net.

MEM.2 Fixed-Width Integers

Fixed-width integers model the exact arithmetic behavior of hardware integers, including overflow and truncation.

Motivation

The dominant SQLite CVE pattern is “64-bit value truncated to 32-bit int in a size calculation.” Example: CVE-2025-52099 where sz * cnt overflows a 32-bit int in setupLookaside().

Types

// Fixed-width unsigned
type U8   = {v: Nat | v <= 255}
type U16  = {v: Nat | v <= 65535}
type U32  = {v: Nat | v <= 4294967295}
type U64  = {v: Nat | v <= 18446744073709551615}

// Fixed-width signed
type I8   = {v: Int | -128 <= v and v <= 127}
type I16  = {v: Int | -32768 <= v and v <= 32767}
type I32  = {v: Int | -2147483648 <= v and v <= 2147483647}
type I64  = {v: Int | -9223372036854775808 <= v and v <= 9223372036854775807}

// Platform-dependent
type USize = U64  // or U32, selected by target
type ISize = I64

// Checked narrowing: REQUIRES proof that value fits
fn narrow_u64_to_u32(v: U64) -> U32
  requires { v <= 4294967295 }

fn narrow_i64_to_i32(v: I64) -> I32
  requires { -2147483648 <= v and v <= 2147483647 }

// Checked multiplication: REQUIRES proof of no overflow
fn checked_mul_u32(a: U32, b: U32) -> U32
  requires { a * b <= 4294967295 }
  ensures  { result == a * b }

Arithmetic Overflow Rules

All fixed-width arithmetic generates refinement checks:

fn alloc_size(count: U64, element_size: U64) -> USize
  requires { count * element_size <= MAX_ALLOC }
{
  let total: U64 = count * element_size
  -- Compiler emits SMT query: count * element_size <= U64_MAX
  -- If caller can't prove it, error A13004

  narrow_u64_to_usize(total)
  -- Compiler emits: total <= USIZE_MAX
  -- If 32-bit target and total > U32_MAX, error A13004
}

This single feature would have caught CVE-2020-13434, CVE-2022-35737, CVE-2025-3277, CVE-2025-7709, and CVE-2025-52099.

Rust Codegen

Fixed-width types map directly to Rust primitive types:

Narrowing generates checked casts:

#![allow(unused)]
fn main() {
pub fn narrow_u64_to_u32(v: u64) -> u32 {
    debug_assert!(v <= u32::MAX as u64);
    v as u32
}
}

MEM.3 Allocator Contracts

Contracts for custom memory allocators that verify structural invariants: no overlap, no double-free, free-list acyclicity.

Grammar

AllocatorDecl  = 'allocator' TypeIdent '<' TypeParam '>' '{'
                   { AllocatorInvariant }
                   AllocateOp
                   FreeOp
                 '}' ;

AllocatorInvariant = 'invariant' ':' Predicate ;
AllocateOp     = 'allocate' '{' { OperationItem } '}' ;
FreeOp         = 'free' '{' { OperationItem } '}' ;

Full Example: Buddy Allocator

allocator BuddyAllocator<BufferSize: Nat> {
  type Block {
    offset: {v: Nat | v < BufferSize},
    size: {v: Nat | is_power_of_2(v) and v > 0},
    allocated: Bool
  }

  type FreeList = List<Block>

  state {
    buffer: Region<BufferSize>,
    blocks: Set<Block>,
    free_lists: Map<Nat, FreeList>  // size -> free blocks of that size
  }

  // No two blocks overlap
  invariant {
    forall b1, b2 in blocks:
      b1 != b2 =>
        b1.offset + b1.size <= b2.offset
        or b2.offset + b2.size <= b1.offset
  }

  // All blocks fit in the buffer
  invariant {
    forall b in blocks: b.offset + b.size <= BufferSize
  }

  // Free list is acyclic (no cycle)
  invariant {
    forall size in free_lists.keys():
      is_acyclic(free_lists[size])
  }

  // Free list only contains unallocated blocks
  invariant {
    forall size in free_lists.keys():
      forall b in free_lists[size]:
        b.allocated == false
  }

  // Total allocated + free == BufferSize
  invariant {
    sum(b.size for b in blocks) == BufferSize
  }

  allocate {
    input(requested_size: {v: Nat | v > 0 and v <= BufferSize})
    output(block: Block :_1)

    ensures { block.size >= round_up_power_of_2(requested_size) }
    ensures { block.allocated == true }
    ensures { block in blocks }
    effects: pure
  }

  free {
    input(block: Block :_1)

    requires { block.allocated == true }
    requires { block in blocks }
    ensures  { block.allocated == false }
    ensures  { block in free_lists[block.size] }
    effects: pure
  }
}

Rust Codegen

Allocator contracts generate a Rust struct implementing std::alloc::Allocator (unstable) or a custom allocator trait:

#![allow(unused)]
fn main() {
pub struct BuddyAllocator {
    buffer: Box<[u8]>,
    free_lists: [Vec<Block>; MAX_ORDER],
}

impl BuddyAllocator {
    pub fn allocate(&mut self, size: usize) -> Option<&mut [u8]> {
        let order = size.next_power_of_two().trailing_zeros() as usize;
        debug_assert!(order < MAX_ORDER);
        // ... buddy allocation logic ...
    }

    pub fn free(&mut self, block: Block) {
        debug_assert!(block.allocated);
        debug_assert!(!self.has_overlap(&block));
        // ... return to free list, coalesce buddies ...
    }
}
}

MEM.4 Circular Buffer Contracts

Contracts for ring buffers and sliding windows that track wrap-around semantics, logical-to-physical index mapping, and slide operations.

Motivation

zlib’s sliding window (deflate_state->window) is a circular buffer where the write pointer wraps around, valid history may be less than window size, and fill_window() physically slides data by copying the second half to the first and adjusting all hash chain pointers. This pattern also appears in network stacks (TCP receive buffers), audio processing (sample ring buffers), database WAL buffers, and kernel I/O schedulers.

MEM.1 handles linear buffer bounds but cannot express wrap-around indexing, the relationship between physical layout and logical sequence, or the correctness of slide operations that relocate data and update dependent pointers.

Grammar

CircularBufferDecl = 'circular_buffer' TypeIdent '<' TypeParam '>'
                     '{' CircularBufferBody '}' ;

CircularBufferBody = 'capacity' ':' Expr ','
                     'write_pos' ':' Ident ','
                     'valid_count' ':' Ident ','
                     { CircularBufferInvariant }
                     [ SlideOp ] ;

CircularBufferInvariant = 'invariant' ':' Predicate ;
SlideOp            = 'slide' '{' { OperationItem } '}' ;

Full Example: zlib Sliding Window

circular_buffer DeflateWindow<WSize: Nat> {
  storage: Region<u8>[WSize * 2],  // physical: 2x for slide
  capacity: WSize,
  write_pos: wnext,      // next write position (wraps)
  valid_count: whave,     // bytes of valid history

  // Structural invariants
  invariant: whave <= WSize
  invariant: wnext < WSize * 2

  // Logical view: the last `whave` bytes written
  ghost fn logical_view(self) -> Seq<u8> {
    if wnext >= whave {
      self.storage[(wnext - whave)..wnext]
    } else {
      // Wrap-around case
      self.storage[(WSize * 2 + wnext - whave)..] ++
        self.storage[..wnext]
    }
  }

  // Read at logical offset (0 = oldest valid)
  fn read(self, offset: {v: Nat | v < self.whave}) -> u8
    ensures result == self.logical_view()[offset]
  {
    let phys = (wnext - whave + offset) % (WSize * 2)
    self.storage[phys]
  }

  // Slide operation: move second half to first, adjust pointers
  slide {
    requires { wnext >= WSize }
    ensures  { logical_view(post) == logical_view(pre) }
    ensures  { wnext(post) == wnext(pre) - WSize }
    ensures  { whave(post) == min(whave(pre), WSize) }
    // All dependent pointers adjusted by -WSize
    ensures  {
      forall p in dependent_pointers:
        p(post) == max(0, p(pre) - WSize)
    }
  }
}

Verification Rules

1. Every index into the buffer must be reduced modulo capacity or proven within physical bounds
2. The logical_view ghost function must be consistent across wrap-around boundaries
3. After a slide operation, the logical sequence is preserved (bytes in the same logical order, just physically relocated)
4. Dependent pointers (hash chain entries in zlib) must all be adjusted by the same offset after a slide
5. Valid count never exceeds capacity

Error Codes

Rust Codegen

Circular buffer contracts generate a Rust struct with modular indexing and a slide method with debug assertions:

#![allow(unused)]
fn main() {
pub struct DeflateWindow {
    storage: Box<[u8]>,  // 2 * wsize
    wsize: usize,
    wnext: usize,
    whave: usize,
}

impl DeflateWindow {
    pub fn read(&self, offset: usize) -> u8 {
        debug_assert!(offset < self.whave);
        let phys = (self.wnext + self.storage.len()
            - self.whave + offset) % self.storage.len();
        self.storage[phys]
    }

    pub fn slide(&mut self, hash_heads: &mut [u16], hash_prev: &mut [u16]) {
        debug_assert!(self.wnext >= self.wsize);
        // Copy second half to first
        self.storage.copy_within(self.wsize..self.wsize * 2, 0);
        // Adjust all hash chain pointers
        for h in hash_heads.iter_mut() {
            *h = h.saturating_sub(self.wsize as u16);
        }
        for p in hash_prev.iter_mut() {
            *p = p.saturating_sub(self.wsize as u16);
        }
        self.wnext -= self.wsize;
        self.whave = self.whave.min(self.wsize);
    }
}
}

14.TYPE: Types and Contracts

TYPE.1 Interface Contracts

Contracts on trait objects, vtables, and dynamically dispatched functions. Every implementation must satisfy the interface contract.

Grammar

InterfaceDecl  = 'interface' TypeIdent [TypeParams] '{'
                   { InterfaceMethod }
                   { InvariantDecl }
                 '}' ;

InterfaceMethod = 'fn' Ident '(' [ParamList] ')' '->' TypeExpr
                  { InterfaceClause } ;

InterfaceClause = RequiresClause | EnsuresClause | EffectsClause ;

ImplDecl       = 'impl' TypeIdent 'for' TypeIdent '{'
                   { FnDecl }
                 '}' ;

Full Example: Virtual File System

interface VirtualFileSystem {
  type FileHandle

  fn open(path: String, flags: OpenFlags) -> FileHandle | IOError
    ensures { result is FileHandle => result.is_valid() }
    effects: filesystem.open

  fn read(
      fh: FileHandle,
      buf: Region<n> :_1,
      amount: {a: Nat | a <= n},
      offset: Nat
  ) -> (Region<n> :_1, {bytes_read: Nat | bytes_read <= amount})
    requires { fh.is_valid() }
    effects: filesystem.read

  fn write(
      fh: FileHandle,
      data: Region<n>,
      offset: Nat
  ) -> {bytes_written: Nat | bytes_written <= n}
    requires { fh.is_valid() }
    effects: filesystem.write

  fn lock(fh: FileHandle, level: LockLevel) -> Bool
    requires { valid_lock_upgrade(fh.current_lock(), level) }
    ensures  { result == true => fh.current_lock() == level }
    effects: filesystem.lock

  fn unlock(fh: FileHandle, level: LockLevel) -> Bool
    requires { level < fh.current_lock() }
    ensures  { result == true => fh.current_lock() == level }
    effects: filesystem.lock

  fn sync(fh: FileHandle, full: Bool) -> Bool
    requires { fh.is_valid() }
    effects: filesystem.sync

  // Lock ordering invariant (typestate on FileHandle)
  invariant {
    forall fh: valid_lock_upgrade(from, to) =>
      (from == Unlocked and to == Shared) or
      (from == Shared and to == Reserved) or
      (from == Reserved and to == Exclusive)
  }
}

// Platform-specific implementations
impl UnixVfs for VirtualFileSystem {
  // Must satisfy ALL interface contracts
  // Compiler verifies each method independently
}

impl WindowsVfs for VirtualFileSystem {
  // Different implementation, same contracts
}

Verification Rule

When verifying impl Foo for Interface:

1. Each method’s implementation is checked against the interface method’s requires/ensures/effects
2. The implementation may have STRONGER preconditions (contravariance)
3. The implementation may have WEAKER postconditions (covariance)
4. The implementation must not use effects beyond what the interface declares

Rust Codegen

Interface contracts map to Rust traits:

#![allow(unused)]
fn main() {
pub trait VirtualFileSystem {
    type FileHandle;

    fn open(&self, path: &str, flags: OpenFlags)
        -> Result<Self::FileHandle, IOError>;

    fn read(&self, fh: &Self::FileHandle, buf: &mut [u8], offset: u64)
        -> Result<usize, IOError>;

    fn write(&self, fh: &Self::FileHandle, data: &[u8], offset: u64)
        -> Result<usize, IOError>;

    fn lock(&self, fh: &Self::FileHandle, level: LockLevel) -> bool;
    fn unlock(&self, fh: &Self::FileHandle, level: LockLevel) -> bool;
    fn sync(&self, fh: &Self::FileHandle, full: bool) -> bool;
}
}

TYPE.2 Recursive Structural Invariants

Invariants that hold recursively across tree, graph, and linked data structures.

Grammar

StructuralInvariant = 'structural_invariant' TypeIdent
                      [TypeParams] '{'
                        { InvariantClause }
                      '}' ;

Full Example: B-Tree

type BTreeNode<K, V, Level: Nat> {
  keys: Vec<K, n> where n >= 1 and n <= 2 * ORDER - 1,
  values: Vec<V, n>,
  children: Vec<BTreeNode<K, V, Level - 1>, n + 1>
    where Level > 0
  -- Leaf nodes (Level == 0) have no children
}

structural_invariant BTreeValid<K, V, Level: Nat> {
  // 1. Keys are sorted within each node
  forall node: BTreeNode<K, V, Level>:
    forall i in 0..len(node.keys)-1:
      node.keys[i] < node.keys[i+1]

  // 2. Subtree ordering: left < key < right
  forall node: BTreeNode<K, V, Level> where Level > 0:
    forall i in 0..len(node.keys):
      max_key(node.children[i]) < node.keys[i]
    forall i in 0..len(node.keys):
      min_key(node.children[i+1]) > node.keys[i]

  // 3. All leaves at same depth (balanced)
  depth(leftmost_leaf) == depth(rightmost_leaf)

  // 4. Minimum occupancy (except root)
  forall node where node != root:
    len(node.keys) >= ORDER - 1

  // 5. Key count matches value count
  forall node:
    len(node.keys) == len(node.values)

  // 6. Child count is key count + 1 (internal nodes)
  forall node where Level > 0:
    len(node.children) == len(node.keys) + 1
}

// Measures for recursive properties
measure max_key<K, V, Level>(node: BTreeNode<K, V, Level>) -> K
  max_key(leaf) = last(leaf.keys) where Level == 0
  max_key(internal) = max_key(last(internal.children))

measure min_key<K, V, Level>(node: BTreeNode<K, V, Level>) -> K
  min_key(leaf) = first(leaf.keys) where Level == 0
  min_key(internal) = min_key(first(internal.children))

measure depth<K, V, Level>(node: BTreeNode<K, V, Level>) -> Nat
  depth(leaf) = 0 where Level == 0
  depth(internal) = 1 + depth(first(internal.children))

Verification Approach

Structural invariants are verified by induction over the data structure:

1. Base case: Verify the invariant holds for leaf nodes
2. Inductive step: Assuming the invariant holds for all subtrees, verify it holds for the parent

This maps to Z3 queries with quantified axioms over the measure functions. Budget: layer 2, 10s timeout.

TYPE.3 Error Propagation Contracts

Contracts that govern how errors flow through the call stack, preventing silent error swallowing, error masking, and error code translation mistakes.

Motivation

SQLite has ~30 error codes (SQLITE_OK through SQLITE_NOTICE) with dozens of extended codes. Error handling is the #1 source of subtle bugs in C systems code:

• Catching SQLITE_CORRUPT and returning SQLITE_OK (hiding database corruption from the caller)
• Translating SQLITE_NOMEM to SQLITE_ERROR (losing the actionable information that memory is full)
• Ignoring the return value of sqlite3_reset() (it returns the error from the last sqlite3_step(), not its own status)
• Calling sqlite3_errmsg() after a second API call (the error message is overwritten)

Effects (Section 3) track what side effects occur but not how errors propagate. Transactional rollback (STOR.4) handles the undo path but not the error code correctness. Error propagation contracts bridge this gap.

Grammar

ErrorPropDecl  = 'error_policy' TypeIdent '{'
                   { ErrorRule }
                 '}' ;

ErrorRule      = 'must_propagate' ':' ErrorCodeList
               | 'must_not_mask' ':' ErrorCodePattern
               | 'may_translate' ':' ErrorTranslation
               | 'must_check' ':' IdentList
               | 'must_preserve_detail' ':' ErrorCodeList ;

ErrorCodeList  = ErrorCode { ',' ErrorCode } ;
ErrorTranslation = ErrorCode '->' ErrorCode
                   ['when' Predicate] ;

ErrorCodePattern = ErrorCode '->' ErrorCode  // forbidden translation ;

PropagateAnnotation = '#[propagate(' ErrorCode ')]'
                    | '#[swallow(' ErrorCode ',' StringLit ')]' ;

Full Example: SQLite Error Propagation

// Global error policy for the SQLite port
error_policy SqliteErrors {
  // These errors MUST propagate to the caller. They cannot be
  // caught and turned into SQLITE_OK.
  must_propagate:
    SQLITE_CORRUPT,    // database corruption
    SQLITE_NOTADB,     // not a database file
    SQLITE_NOMEM,      // out of memory
    SQLITE_IOERR,      // disk I/O error
    SQLITE_FULL        // disk full

  // Error masking rules: these translations are FORBIDDEN
  must_not_mask:
    SQLITE_CORRUPT -> SQLITE_OK,    // hiding corruption
    SQLITE_CORRUPT -> SQLITE_ERROR, // downgrading corruption
    SQLITE_NOMEM -> SQLITE_ERROR,   // losing OOM detail
    SQLITE_IOERR -> SQLITE_OK      // hiding I/O failure

  // Allowed translations (explicit and documented)
  may_translate:
    SQLITE_BUSY -> SQLITE_LOCKED
      when holding_table_lock
    SQLITE_CONSTRAINT -> SQLITE_CONSTRAINT_UNIQUE
      when constraint_type == Unique
    SQLITE_CONSTRAINT -> SQLITE_CONSTRAINT_FOREIGNKEY
      when constraint_type == ForeignKey
    SQLITE_IOERR -> SQLITE_IOERR_READ
      when operation == Read
    SQLITE_IOERR -> SQLITE_IOERR_WRITE
      when operation == Write

  // These function return values MUST be checked by the caller
  must_check:
    sqlite3_reset,       // returns error from last step
    sqlite3_finalize,    // returns error from last step
    sqlite3_close,       // returns BUSY if statements open
    sqlite3_exec         // returns error from callback or SQL

  // These errors must preserve their detail across translations
  // (extended error code must survive)
  must_preserve_detail:
    SQLITE_IOERR,        // keep IOERR_READ vs IOERR_WRITE
    SQLITE_CONSTRAINT    // keep CONSTRAINT_UNIQUE vs FK
}

// Using error propagation contracts
fn read_page_from_disk(
    fd: FileDescriptor,
    page_num: U32
) -> Region<PageSize> | SqlError
  #[propagate(SQLITE_IOERR)]
  #[propagate(SQLITE_CORRUPT)]
  effects: filesystem.read
{
  let bytes = read_bytes(fd, page_num * PageSize, PageSize)?
  // ? propagates SQLITE_IOERR from read_bytes

  if not validate_page(bytes) {
    return SqlError(SQLITE_CORRUPT, "page checksum mismatch")
  }

  bytes
}

// COMPILE ERROR: masking corruption
fn bad_error_handling(
    fd: FileDescriptor,
    page_num: U32
) -> Region<PageSize>
  effects: filesystem.read
{
  match read_page_from_disk(fd, page_num) {
    Ok(bytes) => bytes,
    Err(e) => {
      // A48002: SQLITE_CORRUPT cannot be masked as SQLITE_OK
      // by returning a default page
      Region.zeroed()  // DANGEROUS: pretending corrupt page is OK
    }
  }
}

// COMPILE ERROR: ignoring must-check return value
fn bad_cleanup(stmt: Statement :_1)
  effects: database.read
{
  stmt.reset()
  // A48004: return value of sqlite3_reset not checked
  // (it carries the error from the last sqlite3_step)
}

// CORRECT: check and propagate
fn good_cleanup(
    stmt: Statement :_1
) -> Statement :_1 | SqlError
  effects: database.read
{
  let result = stmt.reset()
  match result {
    Ok(s) => s,
    Err(e) => {
      // Log the error from last step, return it
      log_error(e)
      return Err(e)
    }
  }
}

// Error detail preservation
fn handle_constraint_error(
    err: SqlError
) -> SqlError
  requires { err.code == SQLITE_CONSTRAINT }
  ensures {
    // Extended code must survive
    result.extended_code == err.extended_code
    // A48005: must_preserve_detail violated if extended code is lost
  }
{
  SqlError {
    code: err.code,
    extended_code: err.extended_code,  // preserve!
    message: format_constraint_message(err),
  }
}

// Swallowing an error explicitly (documented escape hatch)
fn optional_optimization(db: Database :_1) -> Database :_1
  effects: database.read
{
  // Explicitly documented: we try an optimization, but it's OK
  // if it fails (we fall back to the slow path)
  #[swallow(SQLITE_BUSY, "optimization hint, slow path is fine")]
  let _ = db.try_wal_checkpoint(WAL_CHECKPOINT_PASSIVE)

  db  // Continue regardless
}

Verification Rule

1. Must-propagate: The compiler traces every error path. If a must_propagate error is caught and not re-raised, it is a compile error
2. Must-not-mask: The compiler checks every error translation (match arm, map_err, ? with conversion). Forbidden translations are compile errors
3. Must-check: Every call to a must_check function must have its return value inspected. Discarding the result (including let _ = ... without #[swallow]) is a compile error
4. Detail preservation: Error translations that lose the extended error code for must_preserve_detail errors are compile errors
5. Explicit swallow: The #[swallow] annotation documents intentional error suppression with a justification string. Reviewers and auditors can search for all swallowed errors

Error Codes

Rust Codegen

Error propagation contracts generate Rust error types with compile-time checking via must_use and custom lints:

#![allow(unused)]
fn main() {
#[derive(Debug, Clone)]
#[must_use = "SqlError must be handled, not silently dropped"]
pub struct SqlError {
    pub code: ErrorCode,
    pub extended_code: ExtendedErrorCode,
    pub message: String,
}

// Critical errors use a wrapper that panics on drop if not handled
#[derive(Debug)]
#[must_use = "Critical errors cannot be silently dropped"]
pub struct CriticalError(SqlError);

impl Drop for CriticalError {
    fn drop(&mut self) {
        if !std::thread::panicking() {
            panic!(
                "Critical error {} dropped without handling: {}",
                self.0.code, self.0.message,
            );
        }
    }
}

impl CriticalError {
    pub fn handle(self) -> SqlError {
        let err = self.0.clone();
        std::mem::forget(self); // disarm the drop bomb
        err
    }
}

// Must-check functions return MustUse wrapper
#[must_use = "sqlite3_reset return value must be checked"]
pub fn sqlite3_reset(stmt: &mut Statement) -> Result<(), SqlError> {
    // ...
}

// Error conversion with masking prevention
impl From<IoError> for SqlError {
    fn from(e: IoError) -> Self {
        // Preserves IO error detail
        SqlError {
            code: ErrorCode::SQLITE_IOERR,
            extended_code: match e.kind() {
                ErrorKind::NotFound => ExtendedErrorCode::IOERR_READ,
                ErrorKind::PermissionDenied => ExtendedErrorCode::IOERR_WRITE,
                _ => ExtendedErrorCode::IOERR,
            },
            message: e.to_string(),
        }
    }
}
}

14.SEC: Trust and Security

SEC.1 Untrusted Data Taint

A taint tracking system for data that crosses trust boundaries. Data from disk, network, or user input is untrusted until explicitly validated.

Motivation

4 of 9 SQLite CVEs were in modules (FTS, R-Tree, JSON, Session) that parse binary data stored in shadow tables. The root cause: these modules trust on-disk metadata (BLOBs) without sufficient validation. The Black Hat 2017 “Many Birds, One Stone” attack exploited this single trust assumption across multiple modules.

Taint Labels

// Taint is a separate axis from security labels
// Security labels: who can SEE the data (confidentiality)
// Taint labels: whether the data is TRUSTED (integrity)

taint_label untrusted   // data from outside the trust boundary
taint_label validated    // data that passed validation
taint_label trusted      // data from within the trust boundary

Grammar

TaintAnnotation = '@taint:' TaintLabel ;
TaintLabel      = 'untrusted' | 'validated' | 'trusted' ;
ValidateExpr    = 'validate' '{' Predicate '}' Expr ;

Taint Propagation Rules

// All data from disk/network/user input is untrusted
fn read_from_disk(path: String) -> Bytes @taint:untrusted
  effects: filesystem.read

// Untrusted data cannot be used where trusted data is expected
fn process(data: Bytes @taint:trusted) -> Result
  // COMPILE ERROR if called with @taint:untrusted data

// Validation converts untrusted to validated
fn validate_blob(
    data: Bytes @taint:untrusted
) -> ValidBlob @taint:validated | ParseError
  effects: pure
{
  validate {
    len(data) >= HEADER_SIZE
    and read_u32(data, 0) == MAGIC_NUMBER
    and read_u32(data, 4) <= MAX_SEGMENT_SIZE
  } data
}

Taint + Information Flow Interaction

Taint (integrity) and security labels (confidentiality) are orthogonal. Data can be:

• @Restricted @taint:trusted (sensitive, from our own database)
• @Public @taint:untrusted (non-sensitive, from network)
• @Restricted @taint:untrusted (sensitive user input, not yet validated)

Both axes must be satisfied: data must be at or below the security label AND at or above the taint level.

SQLite Example: FTS Shadow Table

fn read_fts_segment(
    db: Database,
    segment_id: U64
) -> FtsSegment | CorruptionError
  effects: database.read
{
  let raw: Bytes @taint:untrusted = db.read_blob("fts_segments", segment_id)

  // Every field must be validated before use
  let header_size = validate { raw.len() >= 16 } raw.read_u32(0)
    or return CorruptionError("header too small")

  let segment_size = validate { header_size <= MAX_SEGMENT } header_size
    or return CorruptionError("segment too large")

  let content = validate { raw.len() >= segment_size } raw.slice(16, segment_size)
    or return CorruptionError("truncated segment")

  FtsSegment { header_size, content }
  // FtsSegment is @taint:validated -- safe to use
}

Error Codes

Rust Codegen

Taint labels erase at runtime (same as security labels). The compiler has already verified all validation paths. Generated Rust includes debug_assert checks on validation predicates:

#![allow(unused)]
fn main() {
pub fn read_fts_segment(db: &Database, segment_id: u64)
    -> Result<FtsSegment, CorruptionError>
{
    let raw = db.read_blob("fts_segments", segment_id)?;

    if raw.len() < 16 {
        return Err(CorruptionError::new("header too small"));
    }
    let header_size = u32::from_be_bytes(raw[0..4].try_into().unwrap()) as usize;

    if header_size > MAX_SEGMENT {
        return Err(CorruptionError::new("segment too large"));
    }

    if raw.len() < header_size {
        return Err(CorruptionError::new("truncated segment"));
    }
    let content = &raw[16..header_size];

    Ok(FtsSegment { header_size, content: content.to_vec() })
}
}

SEC.2 FFI Boundary Contracts

Contracts for functions exposed to or called from foreign languages (C, Python, Java via JNI). These define the safety contract at the boundary between verified Assura code and unverified foreign callers.

Motivation

SQLite’s entire value comes from its C API. A Rust port must expose sqlite3_open(), sqlite3_exec(), etc. as extern "C" functions. The Rust side is verified; the C caller is not. The FFI contract defines what the caller must guarantee and what the callee promises, making the boundary explicit rather than implicit.

Grammar

FfiDecl        = 'ffi' StringLit TypeIdent '{'
                   { FfiFunction }
                 '}' ;

FfiFunction    = 'export' Ident '(' [FfiParamList] ')'
                 '->' FfiReturnType
                 '{' { FfiClause } '}' ;

FfiParam       = Ident ':' FfiType [FfiAnnotation] ;
FfiType        = 'ptr' '<' TypeExpr '>'        // raw pointer
               | 'nullable_ptr' '<' TypeExpr '>'
               | 'cstring'                     // null-terminated
               | 'buffer' '<' Ident '>'        // ptr + length pair
               | 'opaque'                      // void*
               | 'c_int' | 'c_uint' | 'c_long'
               | 'size_t' ;

FfiAnnotation  = '#[not_null]'
               | '#[null_terminated]'
               | '#[valid_for(' Ident ')]'
               | '#[caller_frees]'
               | '#[callee_frees]'
               | '#[borrowed(' Lifetime ')]' ;

FfiClause      = 'caller_guarantees' ':' Predicate
               | 'callee_guarantees' ':' Predicate
               | 'error_convention' ':' FfiErrorConvention
               | 'thread_safety' ':' ThreadSafetyLevel ;

FfiErrorConvention = 'return_code' '(' IntLit '=' Ident
                     { ',' IntLit '=' Ident } ')'
                   | 'null_on_error'
                   | 'errno' ;

ThreadSafetyLevel = 'single_threaded'
                  | 'serialized'     // safe to call from any thread
                  | 'multi_threaded' // safe if different connections
                  ;

Full Example: SQLite C API

ffi "C" SqliteApi {
  // sqlite3_open(filename, **ppDb) -> int
  export sqlite3_open(
    filename: cstring #[not_null] #[null_terminated],
    ppDb: ptr<ptr<Connection>> #[not_null]
  ) -> c_int {
    caller_guarantees:
      filename points to valid null-terminated UTF-8

    callee_guarantees:
      result == SQLITE_OK =>
        *ppDb is a valid Connection pointer
      result != SQLITE_OK =>
        *ppDb may or may not be set
        // Caller MUST call sqlite3_close(*ppDb) even on error
        // if *ppDb is non-null (this is a real SQLite requirement)

    error_convention: return_code(
      0 = SQLITE_OK,
      7 = SQLITE_NOMEM,
      14 = SQLITE_CANTOPEN
    )

    thread_safety: serialized
  }

  // sqlite3_exec(db, sql, callback, arg, errmsg) -> int
  export sqlite3_exec(
    db: ptr<Connection> #[not_null]
        #[valid_for(connection_lifetime)],
    sql: cstring #[not_null] #[null_terminated],
    callback: nullable_ptr<ExecCallback>,
    callback_arg: opaque,
    errmsg: nullable_ptr<ptr<c_char>> #[callee_frees]
  ) -> c_int {
    caller_guarantees:
      db was returned by sqlite3_open and not yet closed
      and sql is valid UTF-8 SQL

    callee_guarantees:
      result == SQLITE_OK =>
        all SQL statements in sql were executed
      result == SQLITE_ABORT =>
        callback returned non-zero (user cancelled)
      result != SQLITE_OK and errmsg != null =>
        *errmsg points to a malloc'd error string
        that the caller must free with sqlite3_free

    error_convention: return_code(
      0 = SQLITE_OK,
      4 = SQLITE_ABORT,
      1 = SQLITE_ERROR
    )

    thread_safety: multi_threaded
    // Safe if no other thread uses the same db connection
  }

  // sqlite3_close(db) -> int
  export sqlite3_close(
    db: nullable_ptr<Connection>
  ) -> c_int {
    caller_guarantees:
      db is null or was returned by sqlite3_open
      and no other thread is using db
      and all prepared statements are finalized

    callee_guarantees:
      result == SQLITE_OK => db is freed, pointer is invalid
      result == SQLITE_BUSY => db is NOT freed, still valid
        // Caller must finalize statements and retry

    error_convention: return_code(
      0 = SQLITE_OK,
      5 = SQLITE_BUSY
    )

    thread_safety: single_threaded
  }

  // sqlite3_prepare_v2(db, sql, nByte, **ppStmt, *pzTail) -> int
  export sqlite3_prepare_v2(
    db: ptr<Connection> #[not_null],
    sql: buffer<nByte> #[not_null],
    nByte: c_int,
    ppStmt: ptr<ptr<Statement>> #[not_null],
    pzTail: nullable_ptr<ptr<c_char>>
  ) -> c_int {
    caller_guarantees:
      db is a valid open connection
      and sql points to nByte bytes of valid UTF-8
      and (nByte >= 0 or nByte == -1)
      // nByte == -1 means read until null terminator

    callee_guarantees:
      result == SQLITE_OK =>
        *ppStmt is a valid prepared statement
        and (pzTail != null => *pzTail points to first byte
             past the end of the first SQL statement in sql)
      result != SQLITE_OK =>
        *ppStmt is null

    error_convention: return_code(0 = SQLITE_OK, 1 = SQLITE_ERROR)
    thread_safety: multi_threaded
  }
}

Verification Rule

1. Callee side: The Assura compiler verifies that the implementation satisfies all callee_guarantees given the caller_guarantees as axioms
2. Caller side: When Assura code calls an FFI function, the compiler verifies that all caller_guarantees are met
3. Lifetime tracking: #[valid_for] annotations create phantom lifetimes in the generated Rust code
4. Null safety: ptr<T> with #[not_null] generates NonNull<T> in Rust; nullable_ptr<T> generates *mut T
5. Memory ownership: #[caller_frees] and #[callee_frees] annotations prevent double-free and leak

Error Codes

Rust Codegen

FFI contracts generate extern "C" functions with safety wrappers:

#![allow(unused)]
fn main() {
/// # Safety
/// - `filename` must be non-null, valid null-terminated UTF-8
/// - `ppDb` must be non-null and point to valid memory for *mut Db
#[no_mangle]
pub unsafe extern "C" fn sqlite3_open(
    filename: *const c_char,
    ppDb: *mut *mut Connection,
) -> c_int {
    // Validate caller guarantees (debug only)
    debug_assert!(!filename.is_null());
    debug_assert!(!ppDb.is_null());

    let filename = match CStr::from_ptr(filename).to_str() {
        Ok(s) => s,
        Err(_) => {
            *ppDb = std::ptr::null_mut();
            return SQLITE_CANTOPEN;
        }
    };

    match Connection::open(filename) {
        Ok(conn) => {
            *ppDb = Box::into_raw(Box::new(conn));
            SQLITE_OK
        }
        Err(e) => {
            // SQLite contract: ppDb may still be set on error
            *ppDb = std::ptr::null_mut();
            e.to_sqlite_code()
        }
    }
}
}

SEC.3 Constant-Time Execution

Contracts that verify a function’s execution time is independent of secret inputs, preventing timing side-channel attacks.

Motivation

WireGuard’s crypto_memneq() compares MACs using XOR accumulation with no early exit. Curve25519 uses a constant-time Montgomery ladder. If any branch depends on a secret value, an attacker can measure execution time to extract the key. No other Assura feature addresses this: taint tracking verifies where data flows, not how computation behaves on it.

Grammar

ConstTimeAnnotation = '#[constant_time]' ;
SecretAnnotation    = '#[secret]' ;
ConstTimeBlock      = 'constant_time' '{' Block '}' ;

Full Example

#[constant_time]
fn mac_verify(
    computed: Bytes #[secret],
    received: Bytes
) -> Bool
  requires computed.len() == received.len()
  ensures result == (computed == received)
{
    // Compiler rejects: early-exit comparison
    // Compiler rejects: secret-dependent array index
    // Compiler rejects: secret-dependent branch

    let mut acc: U8 = 0
    for i in 0..computed.len() {
        acc = acc | (computed[i] ^ received[i])
    }
    acc == 0
}

fn curve25519_scalarmult(
    scalar: U256 #[secret],
    point: Point
) -> Point
{
    // Montgomery ladder: both branches execute identical operations
    constant_time {
        let mut r0 = IDENTITY
        let mut r1 = point
        for bit in (0..256).rev() {
            let b = scalar.bit(bit)  // secret-dependent value
            // cswap executes same instructions regardless of b
            cswap(b, &mut r0, &mut r1)
            r1 = point_add(r0, r1)
            r0 = point_double(r0)
            cswap(b, &mut r0, &mut r1)
        }
        r0
    }
}

Verification Rule

The verifier performs information-flow analysis on #[secret] data:

1. No branch condition may depend on secret data
2. No array index may depend on secret data
3. No loop bound may depend on secret data
4. No variable-time instruction (division, modulo on some architectures) on secret data
5. constant_time { } blocks are verified as a unit

Error Codes

Rust Codegen

#[constant_time] generates normal Rust code; the timing guarantee is verified at compile time. The compiler may additionally emit:

• core::hint::black_box() around secret comparisons
• Platform-specific constant-time intrinsics (e.g., subtle::ConstantTimeEq)

#![allow(unused)]
fn main() {
fn mac_verify(computed: &[u8], received: &[u8]) -> bool {
    debug_assert_eq!(computed.len(), received.len());
    let mut acc = 0u8;
    for i in 0..computed.len() {
        acc |= computed[i] ^ received[i];
    }
    core::hint::black_box(acc) == 0
}
}

SEC.4 Secure Erasure

Contracts that guarantee secret data is zeroed in memory when no longer needed, preventing key material from lingering.

Motivation

WireGuard calls memzero_explicit() on all handshake keys after wg_noise_handshake_begin_session(). Linear types ensure single-use but not zeroing: a key consumed by linearity could be freed without overwriting. The compiler’s dead-store elimination may optimize away a memset(key, 0, 32) if it sees no subsequent read.

Grammar

SecureEraseAnnotation = '#[secure_erase]' ;
EraseExpr             = 'erase' '(' Expr ')' ;

Full Example

type SessionKey #[secure_erase] {
    key: Bytes(32),
    nonce_counter: U64
}

fn handshake_complete(
    hs: Handshake #[linear]
) -> SessionKey
  ensures memory_zeroed(hs)
{
    let session = derive_session(hs.chaining_key, hs.hash)
    erase(hs)  // compiler emits volatile zero + barrier
    session
}

fn session_expired(key: SessionKey #[linear]) -> ()
  ensures memory_zeroed(key)
{
    erase(key)
}

Verification Rule

Types marked #[secure_erase] must be erased before deallocation:

1. Every code path that drops the value must call erase() first
2. erase() emits a volatile write of zeros + compiler barrier
3. Copying a #[secure_erase] value is forbidden (linear by default)
4. Passing to a function transfers the erasure obligation

Error Codes

Rust Codegen

erase() emits zeroize::Zeroize trait call or inline volatile write with a compiler fence:

#![allow(unused)]
fn main() {
impl Drop for SessionKey {
    fn drop(&mut self) {
        // Volatile write prevents dead-store elimination
        unsafe {
            core::ptr::write_volatile(&mut self.key as *mut [u8; 32], [0u8; 32]);
        }
        core::sync::atomic::compiler_fence(core::sync::atomic::Ordering::SeqCst);
    }
}
}

SEC.5 Cryptographic Specification Conformance

Contracts that verify a cryptographic implementation correctly implements its mathematical specification, connecting C/Rust code to formal algorithm definitions from standards documents.

Motivation

mbedTLS implements AES (FIPS 197), ECDSA (FIPS 186-5), RSA (PKCS#1 v2.2), and dozens of other algorithms. A wrong constant in the NIST P-256 curve parameters, a subtle error in modular reduction, or an off-by-one in the key schedule would silently produce incorrect cryptographic output. Existing features provide building blocks (CORE.4 axioms define the math, CORE.2 lemmas prove properties, NUM.2 verifies precomputed tables), but no feature expresses the top-level claim: “this function correctly implements AES-128 as defined by FIPS 197.”

This is distinct from FMT.6 (Protocol Grammar Conformance), which verifies parsers against ABNF/BNF grammars. Cryptographic conformance verifies algorithms against algebraic/mathematical specifications. The verification techniques differ: grammar conformance uses language-theoretic checking; crypto conformance uses algebraic reasoning and equational proofs.

Projects like HACL*, Fiat-Crypto, and Jasmin provide this level of assurance. Assura makes it a first-class language feature.

Grammar

CryptoConformanceAnnotation = '#[conforms' '(' SpecRef ')' ']' ;
SpecRef        = StringLit ;      // e.g., "FIPS_197_AES_128"
AlgorithmDecl  = '#[conforms' '(' SpecRef ')' ']'
                 'fn' Ident '(' ParamList ')' '->' Type
                 '{' AlgorithmBody '}' ;
AlgorithmBody  = { Statement } ;

Full Example: AES-128 Block Cipher

// Mathematical specification (axiomatic)
spec FIPS_197_AES_128 {
  // The AES round function
  axiom SubBytes(state: Matrix<4,4,GF256>) -> Matrix<4,4,GF256> {
    forall i, j: state_out[i][j] == sbox(state_in[i][j])
  }

  axiom ShiftRows(state: Matrix<4,4,GF256>) -> Matrix<4,4,GF256> {
    forall i, j: state_out[i][j] == state_in[i][(j + i) % 4]
  }

  axiom MixColumns(state: Matrix<4,4,GF256>) -> Matrix<4,4,GF256> {
    forall j: column_out[j] == gf_matrix_mul(MIX_MATRIX, column_in[j])
  }

  axiom AddRoundKey(state: Matrix<4,4,GF256>,
                    round_key: Matrix<4,4,GF256>) -> Matrix<4,4,GF256> {
    forall i, j: state_out[i][j] == state_in[i][j] xor round_key[i][j]
  }

  // Full AES-128: 10 rounds with specified structure
  axiom encrypt(plaintext: Bytes(16), key: Bytes(16)) -> Bytes(16) {
    let state = to_matrix(plaintext)
    let round_keys = key_expansion(key)  // 11 round keys
    let s0 = AddRoundKey(state, round_keys[0])
    let s_mid = fold(1..10, s0, fn(s, r) {
      AddRoundKey(MixColumns(ShiftRows(SubBytes(s))), round_keys[r])
    })
    let s_final = AddRoundKey(ShiftRows(SubBytes(s_mid)), round_keys[10])
    from_matrix(s_final)
  }
}

// Implementation verified against the spec
#[conforms("FIPS_197_AES_128")]
fn aes_128_encrypt(
  plaintext: &[u8; 16],
  key: &[u8; 16]
) -> [u8; 16]
  ensures result == FIPS_197_AES_128.encrypt(plaintext, key)
{
  let mut state = load_state(plaintext)
  let round_keys = expand_key(key)

  state = xor_state(state, round_keys[0])
  for r in 1..10 {
    state = sub_bytes(state)
    state = shift_rows(state)
    state = mix_columns(state)
    state = xor_state(state, round_keys[r])
  }
  state = sub_bytes(state)
  state = shift_rows(state)
  state = xor_state(state, round_keys[10])
  store_state(state)
}

Verification Rules

1. The #[conforms(spec)] annotation binds the function to a named specification; the verifier must prove the function’s output matches the spec’s definition for all valid inputs
2. Helper functions (e.g., sub_bytes, mix_columns) may have their own #[conforms] annotations for compositional proof
3. Precomputed tables used by the implementation (S-boxes, round constants, curve parameters) are verified against the spec’s axiomatic definitions via NUM.2
4. Optimized implementations (AESNI intrinsics, fast NIST reduction) must also conform; PERF.1 escape requires the same conformance proof as the reference implementation
5. The spec itself is trusted (axiomatic); the implementation is verified against it

Error Codes

Rust Codegen

Conformance contracts generate debug-mode comparison against a reference implementation derived from the spec:

#![allow(unused)]
fn main() {
#[cfg(debug_assertions)]
fn aes_128_encrypt_checked(plaintext: &[u8; 16], key: &[u8; 16]) -> [u8; 16] {
    let result = aes_128_encrypt(plaintext, key);
    let reference = aes_128_reference(plaintext, key);
    debug_assert_eq!(result, reference,
        "AES-128 conformance failure: implementation diverges from FIPS 197");
    result
}

// Release mode: direct implementation, no runtime check
// (correctness proven at verification time)
#[cfg(not(debug_assertions))]
fn aes_128_encrypt_checked(plaintext: &[u8; 16], key: &[u8; 16]) -> [u8; 16] {
    aes_128_encrypt(plaintext, key)
}
}

14.CONC: Concurrency

CONC.1 Shared Memory Protocols

Verification of concurrent access patterns across OS processes that share memory-mapped regions.

Motivation

SQLite’s WAL-Reset Bug (present for 16 years, 2010-2026) was a data race between two processes accessing the -shm (shared memory) file. It required precise timing to reproduce and was never caught by testing, fuzzing, or 100% MC/DC coverage. A formal model of the shared memory locking protocol would have caught it.

Grammar

SharedMemoryDecl = 'shared_memory' TypeIdent '{'
                     LayoutDecl
                     { ProtocolDecl }
                     { SharedInvariant }
                   '}' ;

LayoutDecl       = 'layout' '{' { LayoutField } '}' ;
LayoutField      = Ident ':' SharedFieldType ';' ;
SharedFieldType  = 'Lock'
                 | 'Atomic' '<' TypeExpr '>'
                 | 'Array' '<' TypeExpr ',' IntLit '>'
                 | TypeExpr ;

SharedInvariant  = 'shared_invariant' ':' Predicate ;

ProtocolDecl     = 'protocol' TypeIdent '{'
                     { ProtocolStep }
                   '}' ;

ProtocolStep     = 'acquire' '(' Ident ')'
                 | 'release' '(' Ident ')'
                 | 'atomic_load' '(' Ident ')'
                 | 'atomic_store' '(' Ident ',' Expr ')'
                 | 'read' '(' Ident ')'
                 | 'write' '(' Ident ',' Expr ')'
                 | ProtocolStep '->' ProtocolStep ;

Type System

Shared memory protocols are verified using multiparty session types extended to shared memory. The compiler models each participant (process) as a party and verifies:

1. No data race: Reads and writes to non-atomic fields are protected by locks
2. Lock ordering: Locks are acquired in a consistent order across all protocols (no deadlock)
3. Atomic correctness: Atomic operations use appropriate memory ordering
4. Protocol compliance: Each process follows its declared protocol

Full Example: WAL Protocol

shared_memory WalIndex {
  layout {
    write_lock: Lock;
    checkpoint_lock: Lock;
    recover_lock: Lock;
    read_locks: Array<Lock, 5>;
    max_frame: Atomic<U32>;
    max_page: Atomic<U32>;
    frame_checksums: Array<U64, MAX_WAL_FRAMES>;
    checkpoint_seq: Atomic<U32>;
  }

  // Writer protocol
  protocol Writer {
    acquire(write_lock)
    -> read(frame_checksums)         // read under write lock
    -> write(frame_checksums, new)   // append new frames
    -> atomic_store(max_frame, new_max)  // publish atomically
    -> release(write_lock)
  }

  // Reader protocol
  protocol Reader {
    atomic_load(max_frame)           // snapshot max_frame
    -> acquire(read_locks[slot])     // mark our snapshot slot
    -> read(frame_checksums)         // read frames up to snapshot
    -> release(read_locks[slot])
  }

  // Checkpoint protocol
  protocol Checkpointer {
    acquire(checkpoint_lock)
    -> atomic_load(max_frame)
    -> for_each read_locks[i]:       // wait for readers past checkpoint
         wait_until(read_locks[i].snapshot >= checkpoint_frame)
    -> write(database_file, pages)   // copy WAL pages to DB
    -> atomic_store(checkpoint_seq, seq + 1)
    -> release(checkpoint_lock)
  }

  // COMPILER VERIFIES:
  // 1. Writer and Reader never write the same non-atomic field
  //    without lock protection
  // 2. Checkpointer waits for all readers before overwriting
  // 3. Lock ordering: write_lock > checkpoint_lock > read_locks
  //    (no deadlock possible)
  // 4. max_frame is always written by Writer before read by Reader
  //    (no stale snapshot)

  shared_invariant:
    forall frame_index in 0..max_frame:
      frame_checksums[frame_index] == compute_checksum(wal_file, frame_index)
}

Verification Approach

Multi-process protocols are verified using bounded model checking (Kani/CBMC-style) at layer 2. The compiler explores all interleavings of protocol steps up to a configurable bound:

[verify.shared_memory]
interleaving_bound = 100       # max interleaving steps to explore
process_count = 3              # max concurrent processes
timeout_ms = 30000             # 30s budget for model checking

Error Codes

Rust Codegen

Shared memory protocols generate Rust code using platform-specific primitives:

#![allow(unused)]
fn main() {
use std::sync::atomic::{AtomicU32, Ordering};
use memmap2::MmapMut;

pub struct WalIndex {
    mmap: MmapMut,
}

impl WalIndex {
    pub fn max_frame(&self) -> u32 {
        let ptr = &self.mmap[MAX_FRAME_OFFSET] as *const u8 as *const AtomicU32;
        unsafe { (*ptr).load(Ordering::Acquire) }
    }

    pub fn set_max_frame(&self, val: u32) {
        let ptr = &self.mmap[MAX_FRAME_OFFSET] as *const u8 as *const AtomicU32;
        unsafe { (*ptr).store(val, Ordering::Release) }
    }
}
}

The compiler generates correct Ordering annotations (Acquire for loads, Release for stores) based on the protocol analysis.

CONC.2 Callback and Re-entrancy Safety

Contracts on user-supplied callbacks that restrict what operations the callback may perform, preventing re-entrancy bugs and deadlocks.

Motivation

SQLite has 12+ callback hooks: authorizer, busy handler, progress handler, commit hook, rollback hook, update hook, WAL hook, collation callback, function callback, etc. If a callback calls back into the database (e.g., executing a query inside the authorizer), the result is corruption or deadlock. SQLite documents these restrictions in prose; Assura enforces them at compile time.

Grammar

CallbackDecl   = 'callback' TypeIdent '{'
                   'signature' ':' FnType
                   { CallbackConstraint }
                 '}' ;

CallbackConstraint = 'must_not_call' ':' IdentList
                   | 'must_not_reenter' ':' IdentList
                   | 'max_duration' ':' DurationExpr
                   | 'may_call' ':' IdentList
                   | 'must_be' ':' CallbackProperty ;

CallbackProperty = 'pure' | 'deterministic' | 'infallible'
                 | 'idempotent' | 'thread_safe' ;

CallbackInstall = 'on_install' ':' Predicate ;

Full Example: SQLite Callbacks

// Authorizer: called during query compilation
callback Authorizer {
  signature: (action: AuthAction, arg1: String?,
              arg2: String?, db_name: String?,
              trigger: String?) -> AuthResult

  // MUST NOT call any database operation (re-entrancy)
  must_not_reenter: Connection

  // MUST NOT allocate from the database's allocator
  must_not_call: sqlite3_malloc, sqlite3_free

  // Must complete quickly (called per-statement-node)
  must_be: infallible

  // May only read connection configuration
  may_call: sqlite3_db_config_read
}

// Busy handler: called when a lock cannot be acquired
callback BusyHandler {
  signature: (context: Opaque, count: Nat) -> Bool

  // MUST NOT call operations that acquire locks
  must_not_call: sqlite3_exec, sqlite3_step, sqlite3_prepare

  // MUST NOT re-enter the connection that triggered it
  must_not_reenter: Connection

  // Should eventually return false (termination)
  // (not enforced at compile time, but generates a warning)
}

// Progress handler: called periodically during long queries
callback ProgressHandler {
  signature: (context: Opaque) -> Bool

  // May call read-only operations on OTHER connections
  may_call: sqlite3_exec where connection != self.connection

  // MUST NOT modify the connection that installed it
  must_not_reenter: Connection

  must_be: thread_safe
}

// Collation callback: called for string comparison
callback CollationCallback {
  signature: (a: Region<n>, b: Region<m>) -> Ordering

  must_be: deterministic  // Same inputs must give same ordering
  must_be: pure           // No side effects
  must_be: infallible     // Cannot fail

  // Transitivity: if a < b and b < c then a < c
  invariant {
    forall a, b, c:
      compare(a, b) == Less and compare(b, c) == Less
      => compare(a, c) == Less
  }

  // Antisymmetry: if a < b then b > a
  invariant {
    forall a, b:
      compare(a, b) == Less <=> compare(b, a) == Greater
  }

  // Reflexivity: a == a
  invariant { forall a: compare(a, a) == Equal }
}

// Installing a callback
service Database {
  operation set_authorizer {
    input(auth: Authorizer)

    // Only one authorizer at a time
    ensures { self.authorizer == Some(auth) }

    // Previous authorizer is replaced (linear: old one dropped)
    ensures { old(self.authorizer) is dropped }

    on_install: self.state @ Open
  }
}

Verification Rule

1. When a callback type is used, the compiler collects all must_not_call and must_not_reenter constraints
2. Any implementation of the callback is checked: its call graph must not include any function in the must_not_call list
3. Re-entrancy is checked by verifying the callback’s transitive call graph does not include any method on the must_not_reenter target
4. must_be: deterministic triggers determinism analysis (see CONC.3)
5. must_be: pure verifies no effects beyond pure
6. Callback invariants (e.g., transitivity for collation) are checked via SMT at Layer 2

Error Codes

Rust Codegen

Callback contracts generate trait bounds with marker types:

#![allow(unused)]
fn main() {
/// Marker: callback must not re-enter Connection
pub trait NoReenter<T> {}

/// Authorizer callback trait
pub trait Authorizer: NoReenter<Connection> + Send {
    fn authorize(
        &self,
        action: AuthAction,
        arg1: Option<&str>,
        arg2: Option<&str>,
        db_name: Option<&str>,
        trigger: Option<&str>,
    ) -> AuthResult;
    // No Result<> return: infallible
}

/// Collation callback trait
pub trait Collation: Send + Sync {
    fn compare(&self, a: &[u8], b: &[u8]) -> std::cmp::Ordering;
    // Pure + deterministic: no &mut self, no interior mutability
}

impl Connection {
    pub fn set_authorizer<A: Authorizer>(&mut self, auth: A) {
        debug_assert!(self.state == ConnectionState::Open);
        self.authorizer = Some(Box::new(auth));
    }
}
}

CONC.3 Determinism Contracts

Contracts that guarantee identical output for identical input, which is stronger than purity. Pure functions have no side effects; deterministic functions additionally produce bit-identical results across invocations, platforms, and compiler versions.

Motivation

SQLite guarantees that the same query on the same database produces the same result bytes. This is critical for:

• Replication (replicas must agree)
• Testing (golden file tests)
• Digital signatures over query results
• WAL checksums (same data must produce same checksum)

Rust’s HashMap iteration order is non-deterministic (randomized seed). Floating-point operations can differ across platforms. Instant::now() introduces time-dependence. A pure function could use any of these.

Grammar

DeterministicAnnotation = '#[deterministic]' ;

DeterministicConstraints = 'deterministic_requires' '{'
                             { DeterministicRule }
                           '}' ;

DeterministicRule = 'no_hash_iteration'
                  | 'no_float_transcendentals'
                  | 'no_pointer_comparison'
                  | 'no_allocation_address'
                  | 'no_time_dependence'
                  | 'no_random'
                  | 'ordered_collections_only'
                  | 'fixed_float_rounding' ;

Full Example: Deterministic Query Execution

#[deterministic]
fn execute_select(
    db: Database,
    stmt: PreparedStatement,
    params: List<Value>
) -> List<Row>
  requires { stmt.is_valid() }
  requires { db.state @ Open }
  ensures {
    // Same db + same stmt + same params = same result, always
    forall db1, db2, params1, params2:
      db1.content == db2.content
      and params1 == params2
      => execute_select(db1, stmt, params1)
         == execute_select(db2, stmt, params2)
  }
  effects: database.read
{
  // Inside a #[deterministic] function, the compiler rejects:
  //   - HashMap (use BTreeMap)
  //   - HashSet (use BTreeSet)
  //   - Instant::now() or any time source
  //   - thread::current().id()
  //   - pointer-to-integer casts
  //   - address-dependent comparisons
  //   - f64::sin/cos/exp (platform-dependent rounding)
  //     unless #[fixed_float_rounding] is active
}

#[deterministic]
fn wal_checksum(
    data: Region<n>,
    seed: (U32, U32)
) -> (U32, U32)
  effects: pure
{
  // Checksum must be deterministic so crash recovery can
  // verify frames written by a different process
  let (mut s1, mut s2) = seed
  for i in 0..n/4 {
    let word = read_u32_native(data, i * 4)
    s1 = s1 +% word   // wrapping add
    s2 = s2 +% s1
  }
  (s1, s2)
}

// COMPILE ERROR: non-deterministic function marked deterministic
#[deterministic]
fn bad_example(items: Map<String, Int>) -> List<String>
  effects: pure
{
  items.keys()  // A35001: Map iteration order is not deterministic
                // Use BTreeMap or sort the keys explicitly
}

Banned Patterns

The compiler maintains a list of non-deterministic operations. Any call to these from a #[deterministic] function is a compile error:

Verification Rule

1. The compiler performs taint analysis: any non-deterministic source taints all downstream values
2. A #[deterministic] function’s return value must not be tainted
3. Calling a non-deterministic function from a deterministic one is an error, even if the result is unused (may affect control flow)
4. #[deterministic] implies pure (no side effects)
5. #[deterministic] is transitive: all callees must also be deterministic

Error Codes

Rust Codegen

Determinism contracts are primarily compile-time. The generated Rust code uses lint attributes to catch accidental non-determinism:

#![allow(unused)]
fn main() {
// Deterministic function: generated with ordered collections
#[cfg_attr(debug_assertions, track_caller)]
pub fn execute_select(
    db: &Database,
    stmt: &PreparedStatement,
    params: &[Value],
) -> Vec<Row> {
    // Compiler ensures BTreeMap is used internally, not HashMap
    let mut results: BTreeMap<RowId, Row> = BTreeMap::new();
    // ... query execution ...
    results.into_values().collect()
}

// Deterministic checksum
#[inline]
pub fn wal_checksum(data: &[u8], seed: (u32, u32)) -> (u32, u32) {
    let (mut s1, mut s2) = seed;
    for chunk in data.chunks_exact(4) {
        let word = u32::from_ne_bytes(chunk.try_into().unwrap());
        s1 = s1.wrapping_add(word);
        s2 = s2.wrapping_add(s1);
    }
    (s1, s2)
}
}

CONC.4 Lock Ordering

Contracts that specify a ranked hierarchy of locks and verify no code path acquires them out of order, preventing deadlocks.

Motivation

jemalloc defines ~30 ranked lock levels (witness system in witness.c). witness_lock_error_impl() aborts on rank reversal at runtime. Shared memory (CONC.1) verifies data-race freedom on individual variables; it does not express “mutex A (rank 45) must be acquired before mutex B (rank 0x1000)” across a call graph.

Grammar

LockRankDecl    = 'lock_rank' Ident '=' IntLit ';' ;
LockAnnotation  = '#[lock_rank(' Ident ')]' ;
LockOrderRule   = 'lock_order' '{' LockRankDecl { LockRankDecl } '}' ;

Full Example

lock_order {
    lock_rank CORE      = 0
    lock_rank BIN       = 10
    lock_rank ARENA     = 20
    lock_rank EXTENT    = 30
    lock_rank TCACHE    = 40
    lock_rank PROF      = 50
}

type BinMutex #[lock_rank(BIN)] { inner: Mutex }
type ArenaMutex #[lock_rank(ARENA)] { inner: Mutex }

fn arena_bin_alloc(
    arena: &Arena,
    bin: &Bin
) -> Ptr
  requires held_locks_below(BIN)
{
    arena.lock.acquire()   // rank ARENA = 20
    bin.lock.acquire()     // rank BIN = 10, ERROR: 10 < 20
}

Verification Rule

1. Each lock acquisition records the rank in a ghost set
2. Acquiring a lock with rank <= max(held_ranks) is an error
3. Releasing a lock removes it from the ghost set
4. Equal-rank locks may use address ordering (annotated explicitly)
5. Call graph analysis propagates lock requirements across functions

Error Codes

Rust Codegen

Lock ordering is verified at compile time and erased. In debug mode, a runtime witness system mirrors jemalloc’s approach:

#![allow(unused)]
fn main() {
#[cfg(debug_assertions)]
thread_local! {
    static HELD_RANKS: RefCell<Vec<u32>> = RefCell::new(Vec::new());
}

fn acquire_lock(lock: &Mutex, rank: u32) {
    #[cfg(debug_assertions)]
    HELD_RANKS.with(|ranks| {
        let ranks = ranks.borrow();
        if let Some(&max) = ranks.iter().max() {
            debug_assert!(rank > max, "lock order violation: {rank} <= {max}");
        }
    });
    lock.lock();
    #[cfg(debug_assertions)]
    HELD_RANKS.with(|ranks| ranks.borrow_mut().push(rank));
}
}

CONC.5 Temporal State Deadlines

Contracts that bind state transitions to time bounds, verifying that time-triggered actions occur within their deadlines.

Motivation

WireGuard rekeying is timer-driven: REKEY_AFTER_TIME = 120s, REJECT_AFTER_TIME = 180s. After 180 seconds, a keypair MUST be zeroed. Typestate tracks which transitions are valid; monotonic state tracks values that increase. Neither expresses “after T seconds in state S, must transition to state S’.” WireGuard’s timers.c has 5 concurrent per-peer timers with interacting deadlines.

Grammar

DeadlineAnnotation = '#[deadline(' Duration ')]' ;
TimeoutTransition  = 'timeout' '(' State ',' Duration ')' '->' State ;
Duration           = IntLit ('ms' | 's' | 'min') ;

Full Example

states KeypairState {
    Created -> Active -> Expired -> Zeroed
}

transition keypair_lifecycle {
    timeout(Active, 120s) -> Expired   // REKEY_AFTER_TIME
    timeout(Expired, 60s) -> Zeroed    // REJECT_AFTER_TIME - REKEY
    timeout(Created, 5s) -> Zeroed     // REKEY_TIMEOUT
}

contract WireGuardPeer {
    invariant keypair.state != Active
              || elapsed(keypair.activated_at) < 180s
    invariant keypair.state == Zeroed
              ==> memory_zeroed(keypair.key)
}

Verification Rule

1. Timer-triggered transitions are verified against the state machine
2. The verifier checks that all timer handlers exist and transition to the declared target state
3. Overlapping deadlines are detected (two timers on same state)
4. Missing timeout handlers generate compile errors

Error Codes

Rust Codegen

Deadlines generate timer registration and handler dispatch:

#![allow(unused)]
fn main() {
impl Peer {
    fn activate_keypair(&mut self, keypair: Keypair) {
        self.keypair = keypair;
        self.timers.set(Timer::Rekey, Duration::from_secs(120));
        self.timers.set(Timer::Reject, Duration::from_secs(180));
    }

    fn handle_timer(&mut self, timer: Timer) {
        match timer {
            Timer::Rekey => self.initiate_rekey(),
            Timer::Reject => {
                self.keypair.zeroize();
                self.keypair_state = KeypairState::Zeroed;
            }
        }
    }
}
}

CONC.6 Weak Memory Ordering

Contracts for programs that use non-sequential-consistency atomic orderings. Instead of a single global shared state, each thread maintains a ghost view of memory. Atomic operations with different orderings (Relaxed, Acquire, Release, AcqRel, SeqCst) generate different ghost view constraints.

Motivation

Every high-performance Rust concurrent data structure uses weak memory orderings. crossbeam-epoch uses Relaxed loads for fast pinning checks. parking_lot uses Relaxed loads in spin loops. arc-swap uses Acquire-Release pairs. seqlock uses Relaxed loads with explicit fences.

Without weak memory support, Assura can only verify under sequential consistency, which is sound (a program correct under SeqCst is correct under weaker orderings) but incomplete (programs that are correct under Acquire-Release may not be expressible under SeqCst, because the SeqCst model adds unnecessary ordering constraints).

Syntax

// Atomic operations carry their ordering annotation
// (matching Rust's std::sync::atomic)
shared x: AtomicU64 {
  // Per-thread views: each thread has its own view of x
  ghost view: Map<ThreadId, ViewTimestamp>
}

fn writer(x: &AtomicU64, val: u64) {
  // Release store: publishes all prior writes to x's view
  x.store(val, ordering: release)
  // Ghost effect: x.view[self_tid] = merge(x.view[self_tid], self.view)
  // All writes before this point become visible to any
  // thread that does an acquire load of x
}

fn reader(x: &AtomicU64) -> u64 {
  // Acquire load: merges x's published view into this thread's view
  let v = x.load(ordering: acquire)
  // Ghost effect: self.view = merge(self.view, x.view[writer_tid])
  // All writes the writer did before its release store
  // are now visible to this thread
  ensures v == x.value  // value is consistent with the view
}

fn fast_check(x: &AtomicU64) -> u64 {
  // Relaxed load: no view synchronization
  let v = x.load(ordering: relaxed)
  // Ghost effect: none. This thread's view is NOT updated.
  // The value may be stale (from this thread's current view)
  ensures v == x.view[self_tid].value_of(x)
}

The View Model

Each thread carries a ghost view map: a partial function from memory locations to the last-seen write timestamp. Atomic operations update views according to their ordering:

The view model is based on the GPS/RSL (Relaxed Separation Logic) approach, adapted for SMT verification.

Example: seqlock Reader

struct SeqLock<T> {
  seq: AtomicU64,  // even = unlocked, odd = write in progress
  data: T,
}

fn read(lock: &SeqLock<T>) -> T {
  loop {
    let s1 = lock.seq.load(ordering: acquire)
    requires s1 % 2 == 0  // must read even (unlocked)

    fence(ordering: acquire)
    let result = lock.data.clone()

    let s2 = lock.seq.load(ordering: acquire)

    if s1 == s2 {
      // No writer intervened: result is consistent
      ensures result == lock.data.at_view(self.view)
      return result
    }
    // Writer intervened: retry. The relaxed observation of
    // an odd sequence number means the data may be torn.
  }
}

Example: crossbeam Epoch Pin Check

fn is_pinned(guard: &Guard) -> bool {
  // Fast path: relaxed load is safe because we only need
  // a hint. If stale, the worst case is an extra epoch advance.
  let epoch = GLOBAL_EPOCH.load(ordering: relaxed)
  // Under weak memory, this might read a stale epoch.
  // The contract says: the result is valid for this thread's
  // current view, but may not reflect other threads' advances.
  ensures result == (guard.local_epoch == epoch)
    || stale_view(self.view, GLOBAL_EPOCH)
}

Verification Rule

1. View tracking: The verifier maintains a ghost view per thread. Each atomic operation generates view constraints based on its ordering annotation
2. Consistency check: The verifier checks that all read values are consistent with the reading thread’s current view. A Relaxed load may read any value that was written and not yet overwritten in the thread’s view
3. Happens-before: An acquire-load from location X after a release-store to X creates a happens-before edge. The verifier checks that all assertions that depend on happens-before are reachable only through valid edges
4. Layer 1: View tracking for Acquire-Release is decidable (QF_UFLIA). Relaxed with fences may require Layer 2
5. Interaction with CONC.1: The shared memory protocol (CONC.1) specifies the protocol-level state machine. CONC.6 specifies the memory-ordering semantics WITHIN that protocol. They compose: the protocol says “state A transitions to state B via this CAS”; CONC.6 says “the CAS uses AcqRel ordering, so views merge accordingly”

Error Codes

Rust Codegen

CONC.6 contracts compile to the same Rust atomic operations the user specified. The ordering annotations are preserved exactly. In debug builds, view assertions generate runtime checks:

#![allow(unused)]
fn main() {
// Source: x.store(val, ordering: release)
// Generated Rust:
x.store(val, Ordering::Release);

// Source: x.load(ordering: acquire)
// Generated Rust:
let v = x.load(Ordering::Acquire);

// Debug build: optional view consistency assertion
#[cfg(debug_assertions)]
{
    // View merge simulation for testing
    debug_assert!(
        THREAD_VIEW.lock().unwrap().is_consistent_with(v),
        "CONC.6: acquire load returned value inconsistent with view"
    );
}
}

14.STOR: Storage and Durability

STOR.1 Crash Recovery Contracts

Contracts that specify what happens when a system crashes at any point during a multi-step operation. Unlike typestate (which tracks normal state transitions), crash recovery reasons about non-deterministic failure points and the procedure that restores invariants on restart.

Motivation

SQLite’s WAL commit has ~12 distinct crash points. If power fails between writing a WAL frame and updating the WAL index, the recovery algorithm must detect the inconsistency and replay valid frames. SQLite’s rollback journal has a similar protocol. These protocols were designed by hand and verified by crash-testing. Assura makes them verifiable at compile time.

Grammar

RecoveryDecl   = 'recovery' TypeIdent '{'
                   RecoveryStateDecl
                   { CrashPointDecl }
                   RecoveryProc
                   RecoveryInvariant
                 '}' ;

RecoveryStateDecl  = 'durable_state' '{' { FieldDecl } '}' ;
CrashPointDecl     = 'crash_point' Ident '{'
                       'at' ':' StringLit
                       'observable' ':' IdentList
                       'recovers_to' ':' Ident
                     '}' ;
RecoveryProc       = 'recover' '{' { OperationItem } '}' ;
RecoveryInvariant  = 'post_recovery' ':' Predicate ;

Full Example: WAL Commit Recovery

recovery WalCommit {
  // What is persisted on disk (survives crash)
  durable_state {
    wal_file: File,
    db_file: File,
    wal_index: SharedMemory<WalIndexHeader>,
    frames: List<WalFrame>
  }

  // Crash point 1: frame written, index not updated
  crash_point frame_written_index_stale {
    at: "after fsync(wal_file), before updating wal_index"
    observable: wal_file contains frame F
                but wal_index.max_frame < F.frame_number
    recovers_to: consistent
  }

  // Crash point 2: index updated, not fsynced
  crash_point index_updated_not_synced {
    at: "after wal_index update, before fsync(wal_index)"
    observable: wal_index.max_frame >= F.frame_number
                but index may contain garbage beyond valid frames
    recovers_to: consistent
  }

  // Crash point 3: checkpoint in progress
  crash_point checkpoint_partial {
    at: "during checkpoint, some pages copied to db_file"
    observable: db_file has mix of old and new pages
    recovers_to: consistent
  }

  // Crash point 4: WAL reset after checkpoint
  crash_point wal_reset_partial {
    at: "after checkpoint complete, during WAL truncate"
    observable: WAL file may be truncated but salt not updated
    recovers_to: consistent
  }

  // Recovery procedure: runs on database open
  recover {
    input(
      wal: File,
      db: File,
      index: SharedMemory<WalIndexHeader>
    )

    // Step 1: Reconstruct valid frame set from WAL file
    // Walk WAL from beginning, verify each frame's checksum
    // Stop at first invalid checksum (crash boundary)
    requires { wal.exists() }

    // Step 2: Rebuild WAL index from valid frames
    ensures {
      forall f in valid_frames(wal):
        index.contains(f.page_number, f.frame_number)
    }

    // Step 3: Any page in db_file is either:
    //   - the version from before the transaction, OR
    //   - the version from the last fully committed transaction
    ensures {
      forall page_num in 1..db.page_count():
        page_content(db, page_num) == original_content(page_num)
        or page_content(db, page_num) == committed_content(page_num)
    }

    effects: filesystem.read, filesystem.write
  }

  // After recovery, the database is always consistent
  post_recovery:
    database_invariant(db) and
    wal_index_matches_wal(index, wal) and
    no_partial_transactions_visible(db, wal)
}

Verification Approach

Crash recovery is verified using bounded model checking (BMC):

1. Enumerate all crash points in the protocol
2. For each crash point, symbolically execute the recovery procedure
3. Verify that post_recovery holds after recovery from each point
4. Verify that no crash point can produce a state where recovery is impossible (liveness)

Budget: Layer 2, 10s per crash point. Total budget scales linearly with the number of declared crash points.

Error Codes

Rust Codegen

Crash recovery contracts generate recovery functions with exhaustive state detection:

#![allow(unused)]
fn main() {
pub struct WalRecovery {
    wal_path: PathBuf,
    db_path: PathBuf,
}

impl WalRecovery {
    pub fn recover(&self) -> Result<(), RecoveryError> {
        let wal = File::open(&self.wal_path)?;
        let valid_frames = self.scan_valid_frames(&wal)?;

        // Rebuild index from valid frames only
        let index = WalIndex::rebuild_from(&valid_frames)?;

        // Verify post-recovery invariant in debug mode
        debug_assert!(self.verify_consistency(&index, &valid_frames));

        Ok(())
    }

    fn scan_valid_frames(&self, wal: &File)
        -> Result<Vec<WalFrame>, RecoveryError>
    {
        let mut frames = Vec::new();
        let mut offset = WAL_HEADER_SIZE;
        while offset < wal.metadata()?.len() as usize {
            match WalFrame::read_and_verify(wal, offset) {
                Ok(frame) => {
                    frames.push(frame);
                    offset += WAL_FRAME_SIZE;
                }
                Err(_) => break, // Crash boundary: stop here
            }
        }
        Ok(frames)
    }
}
}

STOR.2 Page Cache Contracts

Contracts for reference-counted page caches with pin/unpin semantics, dirty tracking, and eviction policies.

Motivation

SQLite’s pager layer is the most complex subsystem after the B-tree. Every database page passes through a cache with these semantics:

• Fetch: get a page from cache or read from disk
• Pin: mark a page as in-use (cannot be evicted)
• Unpin: release a page (eligible for eviction)
• MakeDirty: mark a page as modified (must be written back)
• MakeClean: mark a page as written (can be discarded)
• Evict: remove unpinned clean pages under memory pressure

Bugs in this layer are catastrophic: evicting a dirty page loses data, using an evicted page is use-after-free, double-unpin corrupts the reference count. Allocator contracts (MEM.3) handle memory pools but cannot express pin/unpin reference counting, dirty tracking, or the interaction between eviction policy and transaction safety.

Grammar

CacheDecl      = 'cache' TypeIdent '<' TypeParam '>' '{'
                   CacheCapacity
                   { CacheInvariant }
                   { CacheOperation }
                 '}' ;

CacheCapacity  = 'capacity' ':' Expr ;

CacheOperation = 'fetch' | 'pin' | 'unpin'
               | 'make_dirty' | 'make_clean' | 'evict' ;

PinState       = 'pinned' '(' Ident ')' | 'unpinned' '(' Ident ')' ;
DirtyState     = 'dirty' '(' Ident ')' | 'clean' '(' Ident ')' ;

Full Example: SQLite Page Cache

cache PageCache<Page> {
  capacity: config.cache_size  // runtime-configurable

  type CacheEntry {
    page_number: U32,
    data: Region<PageSize>,
    pin_count: {v: Nat | v >= 0},
    is_dirty: Bool,
    in_journal: Bool  // written to rollback journal
  }

  // Core invariants
  invariant {
    // Pinned pages cannot be evicted
    forall entry in self.entries:
      pinned(entry) => not evictable(entry)
  }

  invariant {
    // Dirty pages cannot be evicted unless journaled
    forall entry in self.entries:
      dirty(entry) and not entry.in_journal
      => not evictable(entry)
  }

  invariant {
    // Pin count matches number of active references
    forall entry in self.entries:
      entry.pin_count == count(active_refs(entry))
  }

  invariant {
    // Cache size does not exceed capacity
    // (only unpinned clean pages are evicted to maintain this)
    count(self.entries where pinned(e) or dirty(e))
      <= self.capacity
  }

  fetch {
    input(page_num: U32)
    output(entry: CacheEntry :_1)

    ensures {
      // Returned entry is pinned (pin_count >= 1)
      pinned(entry)
    }

    ensures {
      // If page was in cache, return cached version
      // If not, read from disk and add to cache
      entry.page_number == page_num
      and entry.data == disk_page(page_num)
    }

    effects: filesystem.read
  }

  pin {
    input(entry: CacheEntry)

    requires { entry in self.entries }
    ensures  { entry.pin_count == old(entry.pin_count) + 1 }
    ensures  { pinned(entry) }

    effects: pure
  }

  unpin {
    input(entry: CacheEntry)

    requires { pinned(entry) }
    requires { entry.pin_count >= 1 }
    ensures  { entry.pin_count == old(entry.pin_count) - 1 }

    // After unpin, page may or may not still be pinned
    // (depends on whether other references exist)
    ensures {
      entry.pin_count == 0 => unpinned(entry)
    }

    effects: pure
  }

  make_dirty {
    input(entry: CacheEntry)

    requires { pinned(entry) }
    // Cannot dirty an unpinned page (someone must be using it)
    ensures  { dirty(entry) }
    ensures  { entry.is_dirty == true }

    effects: pure
  }

  make_clean {
    input(entry: CacheEntry)

    requires { dirty(entry) }
    requires {
      // Page must be written to disk or journal first
      entry.data == disk_page(entry.page_number)
      or entry.in_journal
    }
    ensures  { clean(entry) }
    ensures  { entry.is_dirty == false }

    effects: pure
  }

  evict {
    input(entry: CacheEntry)

    requires { unpinned(entry) }
    requires { clean(entry) }
    // CANNOT evict pinned or dirty pages

    ensures { entry not in self.entries }

    effects: pure
  }
}

// COMPILE ERROR: using page after unpin without re-fetch
fn bad_page_use(cache: PageCache<Page>) -> Region<PageSize>
{
  let entry = cache.fetch(42)       // pinned
  let data = entry.data
  cache.unpin(entry)                // unpinned
  data  // A44001: accessing data from unpinned cache entry
        // (entry may be evicted, data is dangling)
}

// CORRECT: pin while using, unpin when done
fn good_page_use(
    cache: PageCache<Page> :_1
) -> (PageCache<Page> :_1, Region<PageSize>)
{
  let entry = cache.fetch(42)       // pinned, pin_count = 1
  let data = copy(entry.data)       // copy data while pinned
  cache.unpin(entry)                // safe to evict now
  (cache, data)                     // return copied data
}

Error Codes

Rust Codegen

Page cache contracts generate a cache struct with runtime pin tracking and debug assertions:

#![allow(unused)]
fn main() {
pub struct PageCache {
    entries: HashMap<u32, CacheEntry>,
    capacity: usize,
}

pub struct CacheEntry {
    page_number: u32,
    data: Box<[u8; PAGE_SIZE]>,
    pin_count: AtomicU32,
    is_dirty: bool,
    in_journal: bool,
}

pub struct PinnedPage<'cache> {
    entry: &'cache CacheEntry,
    cache: &'cache PageCache,
}

impl PageCache {
    pub fn fetch(&self, page_num: u32) -> PinnedPage<'_> {
        let entry = self.entries.get(&page_num)
            .unwrap_or_else(|| self.read_from_disk(page_num));
        entry.pin_count.fetch_add(1, Ordering::Relaxed);
        PinnedPage { entry, cache: self }
    }
}

// PinnedPage auto-unpins on drop (RAII)
impl<'cache> Drop for PinnedPage<'cache> {
    fn drop(&mut self) {
        let prev = self.entry.pin_count.fetch_sub(1, Ordering::Relaxed);
        debug_assert!(prev >= 1, "Double unpin on page {}",
            self.entry.page_number);
    }
}

impl<'cache> PinnedPage<'cache> {
    pub fn data(&self) -> &[u8; PAGE_SIZE] {
        &self.entry.data
    }

    pub fn make_dirty(&mut self) {
        debug_assert!(self.entry.pin_count.load(Ordering::Relaxed) >= 1);
        // ... mark dirty ...
    }
}
}

STOR.3 MVCC and Snapshot Isolation

Contracts for multi-version concurrency control that guarantee readers see a consistent snapshot while writers modify data concurrently.

Motivation

SQLite’s WAL mode allows concurrent readers and a single writer. Each reader sees the database as it existed at the moment the read transaction started, even if the writer commits new data afterward. This is snapshot isolation: reader R at version V sees page P at version V, not version V+1 that the writer just committed.

Shared memory protocols (CONC.1) handle the atomic read/write of shared state. Snapshot isolation is a higher-level property: it defines which version of data each transaction can see, based on when the transaction started relative to commits.

Grammar

SnapshotDecl   = 'snapshot' TypeIdent '{'
                   VersionType
                   SnapshotInvariant
                   { SnapshotRule }
                 '}' ;

VersionType    = 'version' ':' TypeExpr ;

SnapshotInvariant = 'isolation' ':' IsolationLevel ;

IsolationLevel = 'snapshot'
               | 'serializable'
               | 'read_committed'
               | 'read_uncommitted' ;

SnapshotRule   = 'visible' '(' Ident ',' Ident ')' ':'
                 Predicate ;

VersionRef     = 'at_version' '(' Ident ',' Expr ')' ;

Full Example: WAL Snapshot Isolation

snapshot WalSnapshot {
  version: U32  // monotonically increasing commit counter

  isolation: snapshot

  // A transaction sees the state at the version when it started
  type Transaction {
    start_version: U32,
    is_writer: Bool,
    // Writer sees its own uncommitted changes
    pending_pages: Map<U32, Region<PageSize>>
  }

  // Core visibility rule: which page version does a reader see?
  visible(txn: Transaction, page: PageNumber):
    if page in txn.pending_pages and txn.is_writer {
      // Writer sees its own pending changes
      page_data == txn.pending_pages[page]
    } else {
      // Read the latest version <= txn.start_version
      page_data == page_at_version(page, txn.start_version)
    }

  // Snapshot consistency: all pages within a transaction
  // come from the same version
  invariant {
    forall txn: Transaction, p1: PageNumber, p2: PageNumber:
      version_of(visible(txn, p1)) == version_of(visible(txn, p2))
      // A reader never sees page 5 at version 10 and
      // page 8 at version 11
  }

  // Writer exclusion: only one writer at a time
  invariant {
    count(active_transactions where is_writer) <= 1
  }

  // Version monotonicity: commits increase the version
  invariant {
    forall commit c1 before c2:
      c1.version < c2.version
  }

  // No lost updates: a committed version is always readable
  invariant {
    forall committed_version v:
      forall txn where txn.start_version >= v:
        can_read(txn, v)
  }

  // Read-your-writes: writer sees its own pending changes
  invariant {
    forall txn where txn.is_writer:
      forall page in txn.pending_pages:
        visible(txn, page) == txn.pending_pages[page]
  }
}

// Using snapshots in queries
fn read_consistent_pair(
    txn: Transaction,
    page_a: U32,
    page_b: U32
) -> (Region<PageSize>, Region<PageSize>)
  requires { not txn.is_writer }
  ensures {
    // Both pages are from the same snapshot
    version_of(fst(result)) == version_of(snd(result))
    and version_of(fst(result)) == txn.start_version
  }
  effects: database.read
{
  let a = read_page(txn, page_a)
  // Even if a writer commits between these two reads,
  // txn still sees the old version of page_b
  let b = read_page(txn, page_b)
  (a, b)
}

// COMPILE ERROR: reading without a transaction
fn bad_read(db: Database, page: U32) -> Region<PageSize>
{
  db.read_page(page)
  // A45001: page read outside transaction context
  //         (no snapshot version, result may be inconsistent)
}

// COMPILE ERROR: write-write conflict detection
fn concurrent_writers(
    db: Database :_1
) -> Database :_1
{
  let txn1 = db.begin_write()  // OK: first writer
  let txn2 = db.begin_write()  // A45003: writer already active
  // ...
}

Verification Rule

1. Snapshot consistency: The compiler verifies that all page reads within a transaction use the same version (the transaction’s start_version)
2. Writer exclusion: At most one write transaction can be active. Starting a second writer is a compile error if the first hasn’t committed or rolled back
3. No dirty reads: A reader never sees uncommitted writer data (unless the reader IS the writer)
4. No phantom reads: The set of visible rows doesn’t change during a read transaction
5. Version tracking: The compiler tracks which version each page reference belongs to and rejects mixing versions

Error Codes

Rust Codegen

Snapshot isolation generates transaction wrappers with version tracking:

#![allow(unused)]
fn main() {
pub struct ReadTransaction<'db> {
    db: &'db Database,
    snapshot_version: u32,
}

pub struct WriteTransaction<'db> {
    db: &'db mut Database,  // exclusive borrow: one writer
    snapshot_version: u32,
    pending: HashMap<u32, Box<[u8; PAGE_SIZE]>>,
}

impl<'db> ReadTransaction<'db> {
    pub fn read_page(&self, page_num: u32) -> &[u8; PAGE_SIZE] {
        // Always reads from snapshot_version, never newer
        self.db.wal.page_at_version(page_num, self.snapshot_version)
    }
}

impl<'db> WriteTransaction<'db> {
    pub fn read_page(&self, page_num: u32) -> &[u8; PAGE_SIZE] {
        // Writer sees its own pending changes first
        if let Some(page) = self.pending.get(&page_num) {
            return page;
        }
        self.db.wal.page_at_version(page_num, self.snapshot_version)
    }

    pub fn write_page(&mut self, page_num: u32, data: [u8; PAGE_SIZE]) {
        self.pending.insert(page_num, Box::new(data));
    }

    pub fn commit(self) -> Result<(), CommitError> {
        // Atomically advance version and write pending pages to WAL
        self.db.wal.commit(self.snapshot_version, &self.pending)
    }
}

impl Database {
    pub fn begin_read(&self) -> ReadTransaction<'_> {
        ReadTransaction {
            db: self,
            snapshot_version: self.wal.current_version(),
        }
    }

    // &mut self guarantees at most one writer (Rust borrow checker)
    pub fn begin_write(&mut self) -> WriteTransaction<'_> {
        WriteTransaction {
            db: self,
            snapshot_version: self.wal.current_version(),
            pending: HashMap::new(),
        }
    }
}
}

STOR.4 Transactional Rollback

Contracts that guarantee atomic success-or-rollback semantics for multi-step operations. If any step fails (OOM, I/O error, constraint violation), the entire operation is undone and the system returns to its pre-operation state.

Motivation

SQLite handles out-of-memory gracefully: every sqlite3_malloc() call can fail, and the system rolls back to a consistent state. This is extraordinarily hard to get right in C (and Rust). There are ~1,200 malloc calls in SQLite, and every single one has a failure path. The SQLITE_NOMEM error propagates up the call stack while unwinding all partial state changes.

Grammar

AtomicDecl     = '#[atomic]' FnDecl ;
RollbackClause = 'on_failure' ':' 'rollback_to' '(' Ident ')' ;
SavepointDecl  = 'savepoint' Ident '=' Expr ;

Full Example: Atomic Insert with OOM Recovery

#[atomic]
fn btree_insert(
    tree: BtCursor :_1,
    key: Region<k>,
    data: Region<d>
) -> (BtCursor :_1) | OutOfMemoryError | DiskFullError
  requires { tree.state @ ReadyToWrite }
  ensures {
    result is BtCursor =>
      contains(result, key) and
      BTreeValid(result.tree)
  }
  on_failure: rollback_to(tree)
  // If ANY allocation or I/O fails, tree is unchanged
  effects: database.write
{
  // Save pre-operation state
  savepoint pre = snapshot(tree)

  // Step 1: Find insertion point (may allocate)
  let pos = find_position(tree, key)?

  // Step 2: Insert cell (may allocate overflow pages)
  let tree = insert_cell(tree, pos, key, data)?

  // Step 3: Rebalance if needed (may allocate new pages)
  let tree = if needs_balance(tree, pos) {
    balance(tree, pos)?
  } else {
    tree
  }

  // If we get here, all steps succeeded
  tree

  // If any ? propagates an error:
  //   1. All allocated pages are freed
  //   2. All modified pages are reverted to savepoint
  //   3. tree is returned in its original state
}

// Compound atomic operation
#[atomic]
fn execute_insert_statement(
    conn: Connection :_1,
    table: String,
    values: List<Value>
) -> (Connection :_1) | SqlError
  on_failure: rollback_to(conn)
  effects: database.write
{
  let cursor = conn.open_cursor(table)?
  let encoded = encode_record(values)?
  let cursor = btree_insert(cursor, encoded.key, encoded.data)?
  // Update indices
  for idx in conn.indices_for(table) {
    let idx_cursor = conn.open_cursor(idx.name)?
    let idx_key = idx.extract_key(values)?
    let idx_cursor = btree_insert(idx_cursor, idx_key, encoded.rowid)?
  }
  conn
}

Verification Rule

1. Savepoint capture: At entry to an #[atomic] function, the compiler inserts a logical savepoint capturing all mutable state
2. Error propagation: Every ? operator is a potential rollback point
3. Rollback proof: The compiler verifies that the on_failure state is reachable from every error point (no partial cleanup that leaves state inconsistent)
4. Nested atomicity: #[atomic] functions may call other #[atomic] functions; the inner one’s failure triggers the outer one’s rollback
5. Linear state: The rollback target must be the original linear value (can’t roll back to an intermediate state)

Error Codes

Rust Codegen

Atomic operations generate Rust code with explicit savepoint and rollback logic:

#![allow(unused)]
fn main() {
pub fn btree_insert(
    tree: &mut BTree,
    key: &[u8],
    data: &[u8],
) -> Result<(), InsertError> {
    // Save rollback state
    let savepoint = tree.savepoint();

    let result = (|| -> Result<(), InsertError> {
        let pos = tree.find_position(key)?;
        tree.insert_cell(pos, key, data)?;
        if tree.needs_balance(pos) {
            tree.balance(pos)?;
        }
        Ok(())
    })();

    match result {
        Ok(()) => {
            savepoint.commit();
            Ok(())
        }
        Err(e) => {
            savepoint.rollback(tree);
            debug_assert!(tree.verify_invariants());
            Err(e)
        }
    }
}
}

STOR.5 Monotonic State Contracts

Contracts for values that must never decrease (or never increase) over time: counters, version numbers, timestamps, sequence IDs.

Motivation

SQLite has many monotonic values:

• File change counter (header offset 24): incremented on every commit, never decremented
• Schema cookie (offset 40): incremented when schema changes
• WAL frame numbers: always increase within a WAL
• Transaction IDs: monotonically increasing
• Auto-increment rowids: always advance, never reuse

If any of these decreases, it indicates corruption, a bug in the port, or a recovery error. Refinement types express constraints on current values (v > 0) but not temporal constraints (v(t+1) >= v(t)). Typestate tracks state transitions but not numeric progression. Monotonicity needs its own concept.

Grammar

MonotonicDecl  = 'monotonic' MonotonicKind Ident ':' TypeExpr
                 [MonotonicBound] ;

MonotonicKind  = 'increasing' | 'decreasing' | 'non_decreasing'
               | 'non_increasing' ;

MonotonicBound = 'wraps_at' Expr    // for bounded counters
               | 'saturates_at' Expr ;

MonotonicCheck = 'assert_monotonic' '(' Ident ')' ;

Full Example: SQLite Monotonic Values

module database_header {
  // File change counter: incremented on each commit
  monotonic non_decreasing file_change_counter: U32
    wraps_at U32.MAX
    // When it wraps, version_valid_for is set to a
    // value not matching the counter (triggers full
    // schema reload)

  // Schema cookie: changes when schema changes
  monotonic non_decreasing schema_cookie: U32

  // Auto-increment counter per table
  monotonic increasing auto_increment: I64
    // Strict: never reuses values, even after DELETE
}

module wal {
  // WAL frame numbers always increase
  monotonic increasing frame_number: U32

  // Salt values change on WAL reset (not monotonic)
  // but within a single WAL epoch, they are constant

  // Max frame in WAL index (updated atomically)
  monotonic non_decreasing max_valid_frame: U32
}

// Using monotonic values
fn commit_transaction(
    header: DatabaseHeader :_1,
    changes: List<PageChange>
) -> DatabaseHeader :_1
  ensures {
    // Counter must advance (not stay the same)
    header.file_change_counter > old(header.file_change_counter)
    or (old(header.file_change_counter) == U32.MAX
        and header.file_change_counter == 0)
    // Wrapping is the ONLY case where new < old
  }
  effects: database.write
{
  let counter = header.file_change_counter
  let new_counter = if counter == U32.MAX {
    header.version_valid_for = 0  // invalidate
    0  // wrap
  } else {
    counter + 1
  }
  header.file_change_counter = new_counter
  header
}

// COMPILE ERROR: decrementing a monotonic value
fn bad_rollback(header: DatabaseHeader :_1) -> DatabaseHeader :_1
{
  header.file_change_counter = header.file_change_counter - 1
  // A47001: monotonic non_decreasing value decreased
  header
}

// COMPILE ERROR: reusing auto-increment
fn bad_insert(table: Table :_1, deleted_rowid: I64) -> Table :_1
{
  let row = Row { rowid: deleted_rowid, ... }
  // A47002: monotonic increasing value reused
  // deleted_rowid was previously assigned, cannot be reused
  table.insert(row)
}

// WAL frame number contract
fn append_wal_frame(
    wal: WalFile :_1,
    frame: WalFrame
) -> WalFile :_1
  requires {
    frame.frame_number > wal.last_frame_number
    // Strict increasing: no duplicate frame numbers
  }
  ensures {
    wal.last_frame_number == frame.frame_number
  }
  effects: filesystem.write
{
  assert_monotonic(wal.max_valid_frame)
  wal.write_frame(frame)
  wal.max_valid_frame = frame.frame_number
  wal
}

Verification Rule

1. Write analysis: Every assignment to a monotonic variable is checked. The new value must satisfy the monotonic constraint relative to the old value
2. Wrapping: wraps_at X allows exactly one transition from X to a smaller value (wrap-around). All other decreases are errors
3. Increasing vs non_decreasing: increasing forbids new == old; non_decreasing allows it
4. Cross-function: Monotonicity is tracked across function boundaries via the linear type system (the value is linear, so only one function modifies it at a time)
5. Recovery exception: During crash recovery (STOR.1), the compiler suspends monotonicity checks on values being restored, since recovery may roll back to a previous valid state

Error Codes

Rust Codegen

Monotonic contracts generate wrapper types that enforce the constraint at runtime in debug mode:

#![allow(unused)]
fn main() {
#[derive(Debug)]
pub struct MonotonicU32<const STRICT: bool> {
    value: u32,
    #[cfg(debug_assertions)]
    previous: u32,
}

impl<const STRICT: bool> MonotonicU32<STRICT> {
    pub fn new(initial: u32) -> Self {
        MonotonicU32 {
            value: initial,
            #[cfg(debug_assertions)]
            previous: initial,
        }
    }

    pub fn get(&self) -> u32 { self.value }

    pub fn advance(&mut self, new_value: u32) {
        #[cfg(debug_assertions)]
        {
            if STRICT {
                debug_assert!(new_value > self.value,
                    "Monotonic increasing: {} not > {}",
                    new_value, self.value);
            } else {
                debug_assert!(new_value >= self.value,
                    "Monotonic non-decreasing: {} not >= {}",
                    new_value, self.value);
            }
            self.previous = self.value;
        }
        self.value = new_value;
    }

    pub fn advance_wrapping(&mut self, new_value: u32) {
        // Allow exactly one wrap from MAX to smaller value
        #[cfg(debug_assertions)]
        {
            if new_value < self.value && self.value != u32::MAX {
                panic!("Non-wrapping decrease: {} -> {}",
                    self.value, new_value);
            }
        }
        self.value = new_value;
    }
}

// Type aliases for SQLite usage
pub type ChangeCounter = MonotonicU32<false>;     // non-decreasing
pub type SchemaCookie = MonotonicU32<false>;       // non-decreasing
pub type FrameNumber = MonotonicU32<true>;         // strict increasing
pub type AutoIncrement = MonotonicU32<true>;        // strict increasing
}

STOR.6 Storage Failure Model

Contracts that define the physical failure semantics of the underlying storage medium, enabling verification of crash recovery logic against a concrete failure model.

Motivation

littlefs’s correctness depends on specific flash physics: programming is idempotent for already-programmed bits, erased state is all-1s, and a torn program leaves only the affected prog_size region indeterminate. The FCRC mechanism CRCs the next prog-sized region to detect torn writes. Crash recovery (STOR.1) specifies what must be recovered; this feature specifies what can go wrong.

Grammar

StorageModelDecl  = 'storage_model' Ident '{' StorageRule { StorageRule } '}' ;
StorageRule       = 'on_crash_during' Ident ':' FailureSpec ';' ;
FailureSpec       = 'affected_region' '(' Expr ')' 'becomes' ('indeterminate' | 'unchanged') ;
EraseSemantics    = 'erase_value' ':' IntLit ';' ;
ProgSemantics     = 'prog_idempotent' ':' BoolLit ';' ;

Full Example

storage_model FlashDevice {
    erase_value: 0xFF
    prog_idempotent: true
    block_size: config.block_size
    prog_size: config.prog_size

    on_crash_during prog:
        affected_region(offset..offset + prog_size) becomes indeterminate
        // all other regions unchanged

    on_crash_during erase:
        affected_region(0..block_size) becomes indeterminate
        // block may be partially erased

    on_crash_during sync:
        // no effect; sync is a barrier, not a write
}

contract MetadataPairWrite {
    // Write to inactive block only
    requires target == pair[1]
    requires pair[0].crc_valid()

    // After crash during prog: pair[0] still valid (untouched)
    crash_safe {
        pair[0].crc_valid()
        pair[0].revision >= last_known_revision
    }

    // After successful commit: pair[1] now has higher revision
    ensures pair[1].revision > pair[0].revision
    ensures pair[1].crc_valid()
}

Verification Rule

1. The storage model declares what physical operations can fail and how
2. Crash recovery contracts (STOR.1) reference the storage model
3. The verifier checks that recovery logic handles every indeterminate region correctly (by detecting via CRC or FCRC)
4. Operations on erased blocks must verify erase_value assumption

Error Codes

Rust Codegen

Storage model declarations generate test infrastructure:

#![allow(unused)]
fn main() {
/// Fault-injection test harness for flash failure model
struct FlashFaultInjector {
    fail_at: Option<(usize, usize)>, // (block, offset) to corrupt
}

impl FlashFaultInjector {
    fn prog(&mut self, block: usize, off: usize, data: &[u8]) -> Result<()> {
        if self.fail_at == Some((block, off)) {
            // Write partial data (torn write simulation)
            let partial = &data[..data.len() / 2];
            self.device.write(block * self.block_size + off, partial)?;
            return Err(Error::PowerLoss);
        }
        self.device.write(block * self.block_size + off, data)
    }
}
}

14.FMT: Data Formats and Parsing

FMT.1 Binary Format Contracts

Contracts for on-disk binary formats that enforce backward compatibility across versions.

Grammar

FormatDecl     = 'format' TypeIdent '{'
                   { FormatField }
                   [CompatibilityDecl]
                 '}' ;

FormatField    = 'offset' IntLit ',' 'size' IntLit ':'
                 Ident ['=' Expr] [WhereClause] ;

CompatibilityDecl = 'compatibility' '{'
                      { FrozenDecl }
                      { ExtensibleDecl }
                    '}' ;

FrozenDecl     = 'frozen' ':' IdentList ;
ExtensibleDecl = 'extensible' ':' IdentList ;

Full Example: SQLite Database Header

format DatabaseHeader {
  offset 0,  size 16: magic = "SQLite format 3\0"
  offset 16, size 2:  page_size
    where page_size in {512, 1024, 2048, 4096, 8192, 16384, 32768, 65536}
    -- Note: value 1 means 65536 (special encoding)

  offset 18, size 1:  write_version
    where write_version in {1, 2}
    -- 1 = rollback journal, 2 = WAL

  offset 19, size 1:  read_version
    where read_version in {1, 2}

  offset 20, size 1:  reserved_space
    where reserved_space >= 0

  offset 21, size 1:  max_embedded_payload_fraction = 64

  offset 22, size 1:  min_embedded_payload_fraction = 32

  offset 23, size 1:  leaf_payload_fraction = 32

  offset 24, size 4:  file_change_counter

  offset 28, size 4:  database_size_pages
    where database_size_pages >= 0

  offset 32, size 4:  first_freelist_trunk_page

  offset 36, size 4:  freelist_page_count

  offset 40, size 4:  schema_cookie

  offset 44, size 4:  schema_format_number
    where schema_format_number in {1, 2, 3, 4}

  offset 48, size 4:  default_cache_size

  offset 52, size 4:  largest_root_btree_page

  offset 56, size 4:  text_encoding
    where text_encoding in {1, 2, 3}
    -- 1 = UTF-8, 2 = UTF-16le, 3 = UTF-16be

  offset 60, size 4:  user_version

  offset 64, size 4:  incremental_vacuum_mode

  offset 68, size 4:  application_id

  offset 72, size 20: reserved_expansion = 0

  offset 92, size 4:  version_valid_for

  offset 96, size 4:  sqlite_version_number

  compatibility {
    // These fields can NEVER change their offset, size, or meaning
    frozen: magic, page_size, write_version, read_version,
            text_encoding, schema_format_number

    // These fields may be given new valid values in future versions
    extensible: application_id, user_version
  }
}

Verification Rules

1. Frozen fields: Any change to a frozen field’s offset, size, encoding, or valid values is a compile error (A31001)
2. Extensible fields: May add new valid values but cannot change offset or size
3. New fields: May only use reserved_expansion space
4. Read compatibility: A reader must accept all valid values from all versions
5. Write compatibility: A writer must only produce values valid for the target version

Cross-Version Testing

// The compiler can verify format compatibility across versions
format_test DatabaseHeader {
  // v1 header must be readable by v2 reader
  compatible: v1 readable_by v2

  // v2 header with new features must be rejected by v1 reader
  // (if write_version > 1)
  incompatible: v2_wal rejected_by v1_reader
    when write_version == 2
}

Error Codes

Rust Codegen

Binary format contracts generate zero-copy parser/serializer code:

#![allow(unused)]
fn main() {
pub struct DatabaseHeader<'a> {
    data: &'a [u8; 100],
}

impl<'a> DatabaseHeader<'a> {
    pub fn magic(&self) -> &[u8; 16] {
        self.data[0..16].try_into().unwrap()
    }

    pub fn page_size(&self) -> u32 {
        let raw = u16::from_be_bytes([self.data[16], self.data[17]]);
        if raw == 1 { 65536 } else { raw as u32 }
    }

    pub fn write_version(&self) -> u8 {
        self.data[18]
    }

    pub fn validate(&self) -> Result<(), FormatError> {
        if self.magic() != b"SQLite format 3\0" {
            return Err(FormatError::BadMagic);
        }
        let ps = self.page_size();
        if !ps.is_power_of_two() || ps < 512 || ps > 65536 {
            return Err(FormatError::BadPageSize);
        }
        // ... validate all fields ...
        Ok(())
    }
}
}

FMT.2 Bit-Level Format Contracts

Contracts for sub-byte parsing: reading individual bits, variable-length bit fields, and bit-packed structures common in compressed data formats.

Motivation

FMT.1 (Binary Format) handles byte-aligned structures like PNG chunk headers and BMP file headers. But many real-world formats require bit-level parsing:

• JPEG Huffman decoding: reads variable-length bit sequences (1-16 bits) that are NOT byte-aligned
• DEFLATE (zlib): 3-bit block headers, 5-bit length codes, variable-width distance codes
• GIF LZW: variable-width codes (starting at min_code_size + 1 bits, growing as the dictionary fills)
• PNG interlacing: bit-packed scanline filters

Without bit-level contracts, the verifier cannot track the bit position cursor, cannot prove that a read of N bits does not exceed the remaining bits, and cannot verify that Huffman table lookups are safe.

Grammar

BitFormatDecl  = 'bit_format' Ident '{'
                   { BitFieldDecl }
                 '}' ;

BitFieldDecl   = BitField | BitChoice | BitAlign ;

BitField       = Ident ':' 'bits' '(' Expr ')'
                 [BitEndian] [BitConstraint] ;

BitChoice      = 'match_bits' '(' Expr ')' '{'
                   { BitPattern '=>' BitFieldDecl }
                 '}' ;

BitAlign       = 'align_to' '(' Expr ')' ;

BitEndian      = 'msb_first' | 'lsb_first' ;

BitConstraint  = 'where' Predicate ;

BitCursor      = 'bit_position' '(' Ident ')'
               | 'bits_remaining' '(' Ident ')' ;

Full Example: JPEG Huffman Decoding

// Bit-level format for JPEG entropy-coded data
bit_format JpegBitstream {
  // The bit cursor tracks position across byte boundaries
  invariant { bits_remaining(self) >= 0 }
}

// Huffman decode: read variable-length code
fn huffman_decode(
    stream: &mut JpegBitstream :read_bits,
    table: &HuffmanTable :verified
) -> U8 | DecodeError
  requires { bits_remaining(stream) >= 1 }
  ensures {
    // Consumed between 1 and 16 bits
    old(bit_position(stream)) < bit_position(stream),
    bit_position(stream) - old(bit_position(stream)) <= 16
  }
{
  let mut code: U16 = 0
  for len in 1..=16 {
    requires { bits_remaining(stream) >= 1 }
    let bit = stream.read_bits(1) as U16  // read exactly 1 bit
    code = (code << 1) | bit

    if table.has_code(code, len) {
      return table.lookup(code, len)
    }
  }
  DecodeError::InvalidHuffmanCode
}

// DEFLATE block header: 3 bits, not byte-aligned
bit_format DeflateBlockHeader {
  is_final: bits(1) msb_first,
  block_type: bits(2) msb_first
    where block_type <= 2  // 0=stored, 1=fixed, 2=dynamic; 3=reserved
}

// GIF LZW: variable-width codes
fn read_lzw_code(
    stream: &mut BitReader :read_bits,
    code_size: U8
) -> U16 | DecodeError
  requires { code_size >= 2 && code_size <= 12 }
  requires { bits_remaining(stream) >= code_size as U32 }
  ensures { result <= (1 << code_size) - 1 }
{
  stream.read_bits(code_size as U32) as U16
}

Verification Rule

1. Bit cursor tracking: The verifier maintains a symbolic bit position for each BitReader/BitWriter. Every read_bits(N) advances the cursor by N and requires bits_remaining >= N
2. Cross-byte safety: When a bit read spans a byte boundary, the verifier confirms the underlying byte buffer has sufficient data. bits_remaining(stream) >= N implies bytes_remaining(stream.buffer) >= ceil(N + bit_offset, 8)
3. Variable-width bounds: For variable-width reads (Huffman, LZW), the verifier checks that the maximum possible read does not exceed remaining bits. Loop invariants must prove the upper bound
4. Alignment: align_to(8) skips bits to reach a byte boundary. The verifier proves the skip does not exceed 7 bits