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)