Troubleshooting and FAQ

Installation

Install the Assura CLI

Preferred (crates.io):

cargo install assura --locked

Requires a Rust toolchain (edition 2024 / rustc 1.87+). 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

`assura doctor` says z3 / rustc / cargo is not found

This is not a check failure. assura check links Z3 through the z3 crate (gh-release prebuilt at cargo install time). The standalone z3 binary on your PATH is only for inspecting SMT-LIB dumps yourself.

rustc and cargo are needed for assura build (generated Rust). They are not required after the prebuilt shell installer if you only run assura check.

# Optional standalone Z3 CLI (macOS / Ubuntu)
brew install z3
sudo apt-get install -y libz3-dev
z3 --version
assura doctor

Rust toolchain version

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

rustc --version
rustup update stable

Verification

Can Assura verify the Rust standard library (or Kani challenges)?

No. Assura proves contracts you write (.assura or /// @ensures on a modeled Rust body). It does not prove rustc’s library/core against undefined behavior.

The verify-rust-std contest uses Kani, Flux, VeriFast, and ESBMC on the real std sources. Assura is not an accepted tool there. check-rust mapping x.wrapping_add(y) to modular arithmetic restates a spec; it does not check the std implementation.

Use Assura for new contracts and AI-written code. Use Kani or Verus to prove existing unsafe Rust in place. See COMPARE.md.

Solver timeout on a contract

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

Causes and fixes:

Complex quantifiers. Quantifiers (forall, exists) with nested data structures are expensive. Simplify the quantifier body or add trigger annotations.
Large numeric ranges. Constraints like forall x: Int, 0 <= x && x < 1000000 enumerate a huge space. Use tighter bounds or refinement types.
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.
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
```
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. The values depend on the declared types.

Fixed-width example (a: I32, b: I32):

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

That is signed 32-bit division of I32::MIN / -1, which overflows. A matching precondition is:

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

Int and Nat are 64-bit machine integers (i64 / u64) in both the SMT model and generated Rust. Overflow wraps. Write requires { a + b >= a } (or an explicit bound) when a clause needs no wrap. Use U8–I32 when you want a narrower width. See What we prove.

Tips for reading counterexamples:

Z3 picks adversarial edge cases: 0, -1, empty collections, and (for fixed-width types) MIN / MAX.
If the counterexample involves very large numbers on a fixed-width type, the 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:

Missing type import. The generated code references a type that is not in scope. Add it to the contract’s context.
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.
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:

Save the file explicitly (some editors delay writes).
Check that the file path matches exactly (watch tracks the specific file, not the directory).

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

Install the Assura extension from the editors/vscode/ directory.
Install the CLI so assura lsp is on PATH:
```
cargo install assura --locked
```
The extension runs assura lsp when assura.serverPath is unset.
Or set a custom server command (no extra args are added). Point at assura-lsp or a wrapper that already includes lsp. A path to the assura CLI will fail (subcommand required):
```
{
  "assura.serverPath": "/path/to/assura-lsp"
}
```
Install the standalone binary with cargo install --path crates/assura-lsp.
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:

Reload the extension: Ctrl+Shift+P > “Developer: Reload Window”
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
smt-solver = "z3"    # "z3", "cvc5", or "portfolio"
# `solver` is also accepted as an alias for `smt-solver`

[profile]
type = "minimal"     # parsed only; does not set parallel or cache

[profile] only has type. Parallel verification defaults on and the disk verify cache defaults off (VerifyOptions). Choose the solver with [verify] smt-solver or assura check --solver.

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/.

Keyboard shortcuts

Assura Language