Assura

Write what it should do. AI proves it does.

A contract-first language for the AI era. Humans write behavioral contracts. AI writes verified implementations. The compiler proves correctness mathematically. Ships as Rust.

Regenerate: vhs assets/demo/assura-check.tape (requires VHS and assura on PATH).

contract HeartbeatResponse {
  input(record_length: Nat, payload_length: Nat, padding_length: Nat)

  requires { record_length >= 3 }              // TLS header: type + 2-byte length
  requires { payload_length >= 1 }
  requires { padding_length >= 16 }            // RFC 6520 minimum
  requires { 3 + payload_length + padding_length <= record_length }

  ensures  { payload_length + 16 <= record_length }   // response fits in buffer
  effects  { pure }
}

You write what. AI figures out how. Z3 proves it. rustc compiles the result.

The Problem

AI writes most new code. Nobody trusts it. AI-generated tests mirror implementation bugs: if divide(10, 0) returns 0 due to a bug, the generated test asserts == 0. The test passes. The bug ships.

Assura replaces trust with proof. Contracts define what the code must do. The compiler uses SMT solvers (Z3/CVC5) to prove the implementation satisfies every contract, or returns a counterexample showing exactly how it fails.

How It Works

Human writes contracts (.assura)
    |
    v
AI generates implementation
    |
    v
Assura compiler verifies (Z3/CVC5 SMT solver)
    |
    +--[proof fails]--> counterexample returned to AI --> AI fixes --> re-verify
    |
    v
Generates Rust source (.rs)
    |
    v
rustc compiles --> native binary / WASM

Three verification tiers, fastest first:

Tier	Time	What it checks
Structural	< 10ms	Types, syntax, names
Decidable SMT	< 200ms	Refinement types, flow analysis, effects
Heavy SMT	< 10s	Full invariants, temporal properties

Quick Start

Install the CLI

Preferred (crates.io):

cargo install assura --locked

Requires a Rust toolchain (edition 2024 / rustc 1.87+). The first build downloads a Z3 prebuilt via the z3 crate (gh-release); no manual Z3 install is needed for normal use. See docs/CRATES-IO.md.

Prebuilt binaries (shell installer, no Rust toolchain required for the binary itself): GitHub Releases via cargo-dist (assura-installer.sh on the release; Linux x86_64 and macOS arm64/x64). Example:

curl --proto '=https' --tlsv1.2 -LsSf \
  https://github.com/assura-lang/assura/releases/latest/download/assura-installer.sh | sh

There is no Homebrew formula published today (installers = ["shell"] in dist-workspace.toml). Prefer crates.io or the shell installer.

From a monorepo clone:

git clone https://github.com/assura-lang/assura.git
cd assura
cargo install --path crates/assura-cli --locked
# Optional standalone LSP binary:
cargo install --path crates/assura-lsp --locked

VS Code extension: lives in editors/vscode/ and is not published to the Marketplace yet. Build from source (see that folder's README) or use the LSP binary from Releases / cargo install --path crates/assura-lsp.

Embedding as a library: the public compile/verify facade is assura-pipeline on crates.io (v0.3.0+):

[dependencies]
assura-pipeline = "0.4"

Prefer crates.io for apps; use a git path dependency only when tracking unreleased main. Release process: docs/CRATES-IO.md.

Usage

Docs site (preferred entry): https://assura-lang.github.io/assura/

Primary path (install → check → build → test): see docs/GETTING-STARTED.md. That guide works on a clean machine with copy-paste files (no monorepo required).

# Initialize a new project
assura init my-project

# Happy-path demos (must-pass). Prefer these over *-audit.assura files.
# See demos/README.md for the showcase vs EXPECT FAIL taxonomy.
assura check demos/heartbleed.assura
# Result-bearing ensures: assura check synthesizes analyzable shapes in memory
# (no hand IR). See docs/GETTING-STARTED.md for the synthesizable table and
# residual ladder (`--write-ir` offline, then `--auto-implement`).
assura check demos/showcase-echo.assura
# Verify, inject IR into Rust, and cargo test:
#   assura build demos/showcase-echo.assura --write-ir --output /tmp/assura-out
#   (cd /tmp/assura-out && cargo test)

# Check with JSON output
assura check demos/libwebp-huffman.assura --json
# Agents: on success, inspect file_info.vacuous / vacuous_reason so empty
# sources or contracts with no SMT proof obligations are not treated as
# verified coverage (see also human-mode check-passed summaries).

# Check with verbose timing info
assura check demos/libwebp-huffman.assura --verbose

# Check with verification statistics
assura check demos/libwebp-huffman.assura --stats

# Explain an error code
assura explain A03001

# Build and generate Rust code
assura build demos/libwebp-huffman.assura

# Format a contract file
assura fmt demos/libwebp-huffman.assura

# Infer contracts from Rust source
assura infer src/main.rs

# Verify inline contract annotations in Rust source files
assura check-rust src/
# Body proof paths (in order):
#   1) co-located {Name}.ir
#   2) encoded Rust body (arith/if/match/wrapping/bitops/…; see docs/CHECK-RUST-SURFACE.md)
# Otherwise ensures are body_not_modeled (not silent verified/skipped).
# User map: docs/CHECK-RUST-SURFACE.md  |  demos: demos/check-rust/  |  interop: examples/interop-rust/
assura check-rust src/ --json
assura check-rust demos/check-rust/ok   # prove demos (expect exit 0)

# Suggest contracts for unannotated functions
assura check-rust src/ --suggest

# Shell completions (raw script, or JSON with --json for agents)
assura completions zsh
assura completions bash --json   # {"command","shell","script"}

Tip: If running from source without installing, prefix commands with cargo run --, e.g. cargo run -- check demos/libwebp-huffman.assura.

Example: CVE Prevention

CVE-2023-4863 was a CVSS 9.8 heap buffer overflow in libwebp that affected Chrome, Firefox, Safari, Android, iOS, and every Electron app on the planet.

In Assura, it is mathematically impossible. Four features block it: memory regions (MEM.1), taint tracking (SEC.1), precomputed table verification (NUM.2), and axiomatic definitions (CORE.4). See demos/libwebp-huffman.assura for the full contract.

50 Features, 12 Categories

Category	Features
CORE Verification Infrastructure	Ghost code, lemmas, frame conditions, axiomatic definitions, quantifier triggers, opaque functions, prophecy variables, liveness contracts
MEM Memory Safety	Memory regions, fixed-width integers, allocator contracts, circular buffer contracts
TYPE Types and Contracts	Interface contracts, recursive structural invariants, error propagation
SEC Trust and Security	Taint tracking, dependent types, constant-time execution, secure erasure, cryptographic spec conformance
CONC Concurrency	Shared memory protocols, callback re-entrancy, determinism, lock ordering, temporal deadlines, weak memory ordering
NUM Numerical and Precision	Numerical precision contracts, precomputed table verification
PERF Performance	Unsafe escape with proof obligation, complexity bounds
FMT Binary Formats	Binary/bit-level format contracts, string encoding, codec dispatch, checksum, protocol grammar
STOR Storage	Crash recovery, page cache, MVCC, rollback, monotonic state, failure models
PLAT Platform	Platform abstraction, feature flags, resource limits
TEST Testing	Test generation from contracts, behavioral equivalence, multi-pass refinement
MISC Miscellaneous	Incremental contracts, scoped invariant suspension

A project activates only the categories it needs. CORE is always on.

Documentation

Site: assura-lang.github.io/assura (preferred URLs; not assura.dev, a different product)

• Getting started (install → check → build)
• Tutorial (first contract, verification layers)
• What we prove (Verified / Unknown / Counterexample; honesty map)
• Compared to other tools (Dafny, Verus, Liquid Haskell, tests)
• Case studies (Heartbleed, libwebp, showcase)
• For AI agents (JSON check, IR acceptance, MCP)
• Quick Reference (types, clauses, effects, CLI commands on one page)
• Scenario Guides (greenfield dev, retrofit existing code, security audit, CI, team onboarding)
• Contract Cookbook (ready-to-copy contract patterns by category)
• Troubleshooting / FAQ (Z3 timeouts, counterexamples, common errors)
• Internals (architecture, crate map, SMT encoding)
• Language Specification (EBNF, verification features, error codes)
• Implementation Roadmap
• Competitive Analysis
• Contributing
• Demo Contracts (CVE-prevention and showcase examples)
• 50 Example Contracts (one per verification feature, organized by category)

License

Dual-licensed under MIT or Apache-2.0, at your option.