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