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 and AGENT-LOOP.md.

Existing Rust with doc-comment contracts: see CHECK-RUST-SURFACE.md and try:

assura check-rust demos/check-rust/ok

1. Install

Preferred (crates.io): requires Rust 1.88+ (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
# Optional standalone LSP binary (same release channel as the CLI):
cargo install --path crates/assura-lsp --locked

The VS Code extension in editors/vscode/ is not published to the Marketplace or Open VSX yet. Build it from that folder, or use the LSP binary above.

To embed the compiler instead of shelling out, depend on assura-pipeline. See that crate’s README and CRATES-IO.md. Use a git path dependency only when tracking unreleased main.

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 and builds the CLI). A warm container requires Codespaces prebuilds enabled for the repo. Without them the first cargo command compiles. Then:

   cargo run --bin assura -- check demos/zip-crate-audit.assura   # counterexamples (intentional)
   cargo run --bin assura -- check demos/heartbleed.assura        # clean proof
   

   The workspace has three binaries, so cargo run needs --bin assura. The same form works on any machine that already has Rust 1.88+ and a built workspace. libz3-dev (or the z3 crate’s prebuilt download) is required to compile.
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)