v0.4.0

Assura 0.4.0

Assura is a contract-first language: you write what the program must do,
SMT solvers check it, and the toolchain generates Rust you can build and run.

0.4.0 is the release where everyday ensures prove more often, onboarding
stops requiring hand-written IR, and check-rust models a much wider slice
of real Rust bodies. Install from crates.io, follow the guide, and get
Verified on contracts that used to stall on Unknown or body_not_modeled.

Highlights

• Synthesis-first contracts: assura check synthesizes implementation
  bodies in memory for many ensures shapes (identity, nested arith, bounds,
  And chains, abs/min/max/clamp/signum free or method form, fields, length,
  Bool logic, if/match/let). You often get Verified without writing a
  .ir file.
• Multi-ensures that pick a real body: prefers result == e over
  if/match and pure bounds; combines multi-clause bounds with a lower-bound
  witness; residual clauses are named under check -v and in JSON.
• Dual track for residuals: offline assura build --write-ir, then
  --auto-implement (heuristics first, LLM only for leftovers).
• check-rust body proof surface: checked/wrapping/saturating arithmetic,
  bit ops, rotates, powers, unwrap_or peels, and more, so annotated Rust
  is proven against the body instead of skipped as body_not_modeled.
• Flagship demos stay green: libwebp-huffman and taint-tracking
  check with no A05102 noise; SHOWCASE demos are labeled for first runs.

What's new

Contracts that verify without hand IR

assura check auto-synthesizes analyzable ensures when no co-located IR
exists:

Family	Examples
Equality	result == x, nested arith, -x
Builtins	free or method abs / min / max / clamp / signum
Bounds	result >= e, And chains, multi-clause bounds (prefer lower witness)
Multi-ensures	Prefer result == e when mixed with bounds or if/match
Structure	fields, tuples, result == xs.length(), Bool logic, if/match/let

Use the residual ladder when a shape is not synthesizable:

1. Simplify ensures toward the table above, or
2. assura build file.assura --write-ir (offline heuristic IR), or
3. assura build file.assura --auto-implement (offline first, then LLM).

result.length() >= 0 on extern / unconstrained result verifies via length
axioms without a body (common SEC.1 pattern).

Docs: GETTING-STARTED.md,
demos/README.md.

Multi-ensures and transparency

When a contract has several ensures clauses:

• The planner prefers a top-level result == e body over if/match and
  pure bound witnesses.
• Pure bound-only multi-ensures share one lower-bound witness.
• Unplannable clauses no longer block a later equality plan.
• assura check -v prints the body driver and residual ensures
  (not body driver).
• assura check --json exposes the same surface under
  file_info.ir (colocated, synthesized, synth_notes) for agents.

Dual-track build path

Command	Role
assura check	In-memory synthesis + SMT
assura build --write-ir	Persist analyzable IR next to source (no API key)
assura build --auto-implement	Offline heuristics first, then LLM for residuals
assura build --bin	Runnable main for the primary contract

--auto-implement no longer requires the model for shapes the offline
planner already understands.

check-rust: prove against real Rust bodies

A large expansion of body encoding so @requires / @ensures on Rust
are checked against the implementation, not left as body_not_modeled:

• Arithmetic peels: checked_*, wrapping_*, saturating_*,
  overflowing_* (including .0 / .1 and unwrap_or / unwrap_or_default)
• Bit and shift surface: and/or/xor, not, rotates, leading/trailing
  zeros and ones, reverse/swap bytes, const and variable masks
• Powers and roots: small pow / wrapping_pow / checked_pow,
  isqrt, ilog2 / ilog10, next_power_of_two
• Control flow: if/match/let folding, distribution over binary ops,
  identity match guards
• Widths: u8 through u64/i64 paths, NonZero divisors for rem_euclid /
  div_ceil, u128/i128 bounds where supported

Wrong bodies still produce counterexamples. Division by a zero-including
path divisor is refused rather than silently modeled.

Agent and CLI polish

• Pure JSON across check, build, fmt, ir, check-rust, init, audit,
  infer, and related commands (machine output without human noise).
• Vacuous success is marked in human and JSON (file_info.vacuous) so
  empty or requires-only files are not mistaken for full proof.
• MCP / REPL failures report structured JSON when requested.
• assura fmt accepts directories of .assura files.
• Project-mode check runs SMT verify, not only types.

Demos and first green run

Prefer SHOWCASE demos for install smoke:

assura check demos/heartbleed.assura
assura check demos/showcase-echo.assura
assura check demos/libwebp-huffman.assura   # zero-warning on 0.4.0
assura check demos/taint-tracking.assura   # read_blob length ensures verified
assura check demos --showcase-only

EXPECT FAIL demos remain intentional (audit / attack models). See
demos/README.md.

Try it

cargo install assura --locked

# Tiny contract path (see GETTING-STARTED.md for full copy-paste files)
assura check ShowcaseEcho.assura
assura build ShowcaseEcho.assura --write-ir --bin --output generated
cd generated && cargo test && cargo run -- 42

From a monorepo clone: bash scripts/smoke-getting-started.sh.

Embedders: assura-pipeline on crates.io (compile / compile_full /
verify_typed). Ops notes: docs/CRATES-IO.md.

Upgrading from 0.3.0

cargo install assura --locked --force
# or pin crates to 0.4.0 in Cargo.toml for assura-pipeline and friends

• Re-run demos you used as smoke tests; libwebp and taint should now report
  check passed (no errors) without determinism / length skips.
• Prefer synthesizable ensures (table above) before hand IR.
• For CI, keep assura check --strict if you want Unknown limitations to fail.
• check-rust: more bodies verify; review any previous body_not_modeled items
  that may now prove or CE against the real body.

No intentional breaking CLI renames in 0.4.0. Pre-1.0 APIs may still evolve
in minor releases.

Links

• Guide: docs/GETTING-STARTED.md
• Demos: demos/README.md
• Compare: v0.3.0...v0.4.0
• Install / crates: docs/CRATES-IO.md

Dual-licensed MIT OR Apache-2.0.

v0.3.0

Assura 0.3.0

Assura is a contract-first language: you write what the program must do, the
compiler and SMT solvers check it, and the toolchain generates Rust you can
build and run.

0.3.0 is the release where install, check, prove, and run line up. You can
install the real CLI from crates.io, follow the getting-started guide,
and get real Verified results on result-bearing contracts without fighting
the toolchain first.

Highlights

• cargo install assura --locked installs the real compiler CLI (and
  related frontends co-publish with the library stack).
• A single documented path: write a tiny contract, assura check,
  optional IR, assura build, then cargo test or cargo run.
• Smarter proofs for everyday ensures: identity, arithmetic, and call
  shapes verify more often; co-located IR and offline --write-ir close the
  loop into generated Rust.
• Labeled demos and clearer check UX: showcase files for first green
  runs; expected-fail demos are labeled so audit files do not look like a
  broken install.

What's new

Install the CLI from crates.io

You can install Assura the way most Rust tools install:

cargo install assura --locked
assura --help

GitHub Release installers (cargo-dist) remain available for prebuilt
binaries. Embedders still use assura-pipeline on crates.io as the
public library entry (compile / compile_full / verify_typed).

See docs/CRATES-IO.md
and the FAQ.

Contract to check to build to run

New guide: docs/GETTING-STARTED.md
(linked from the README and tutorial).

Typical flow:

# Check (often Verified on synthesizable result ensures)
assura check ShowcaseEcho.assura

# Persist IR + inject bodies + optional binary
assura build ShowcaseEcho.assura --write-ir --bin --output generated
cd generated && cargo test
cargo run -- 42

Repo smoke (from a clone): bash scripts/smoke-getting-started.sh.

Result postconditions that actually prove

ensures { result == ... } is first-class, not a dead end:

• In-memory synthesis on check: for synthesizable shapes (identity,
  simple arithmetic, known if/match/call patterns), assura check builds
  an implementation body in memory when co-located IR is missing, so you
  often get Verified without writing a .ir file first.
• Offline IR without an LLM: assura build --write-ir writes co-located
  {ContractName}.ir from the same heuristics and injects it into generated
  Rust.
• Runnable binary: assura build --bin emits a small main for the
  primary contract so you can cargo run a demo end-to-end.
• Clear refusal: unanalyzable shapes (for example bare result > 0
  with no body) stay Unknown with guidance, not a silent counterexample
  and not a fake identity proof.

Call-shaped contracts and multi-contract files

• Call IR: same-file pure helpers (including multi-arg arithmetic
  shapes) get non-identity sibling IR instead of empty plumbing stubs.
• Ensures equating: result == double(x) lines up with the helper's
  functional ensures under Z3 and CVC5 when the helper is in-file and pure.
• Multi-contract verify_ir: matches the IR module name to a contract,
  or asks you to name the contract instead of silently validating against
  the first declaration only.

Demos you can trust for a first green run

Demos are labeled SHOWCASE (must-pass) vs EXPECT FAIL (intentional
counterexamples / audit models). Prefer:

• demos/heartbleed.assura
• demos/showcase-echo.assura (result-bearing path)
• other SHOWCASE entries in demos/README.md

Directory check can filter demos:

assura check demos --showcase-only

Fixed-width integers that compare correctly

Signed fixed-width types (I8, I32, and friends) use proper signed
bitvector ordering in Z3 and CVC5, so comparisons and bounds on fixed-width
values match what you wrote in the contract.

Check and build flags that match real workflows

Flag	What it does
assura check --strict	Treat SMT Unknown (including known limitations) as failure (great for CI)
assura check --showcase-only	In a directory, only files marked SHOWCASE
assura build --write-ir	Write co-located heuristic IR (no LLM)
assura build --bin	Add a runnable binary target for the primary contract
assura build --auto-implement	LLM path when configured (still optional)

Try it in under a minute

cargo install assura --locked

mkdir hello-assura && cd hello-assura
cat > ShowcaseEcho.assura << 'EOF'
contract ShowcaseEcho {
  input(x: Int)
  output(result: Int)
  ensures { result == x }
}
EOF

assura check ShowcaseEcho.assura
# Expect: ensures ... verified

assura build ShowcaseEcho.assura --write-ir --bin --output generated
cd generated && cargo run -- 7
# Expect: 7

From a monorepo clone without installing:

cargo run -q --bin assura -- check demos/showcase-echo.assura
bash scripts/smoke-getting-started.sh

After you upgrade

1. Prefer crates.io 0.3.0 (cargo install assura --locked or
   assura-pipeline = "0.3") over tracking unreleased main unless you need
   unreleased work.
2. Re-run assura check on your contracts. Synthesizable result ensures may
   flip from Unknown/skipped to Verified without new files.
3. For generated code and cargo run, use co-located IR or
   assura build --write-ir so implementations land in the crate (check
   synthesis alone does not write disk IR).
4. For CI gates that mean "no Unknowns," use assura check --strict.
5. Start new users on SHOWCASE demos and
   GETTING-STARTED,
   not *-audit.assura files.

Full history

Machine-generated commit list:
CHANGELOG.md
(and the release-please section for 0.3.0 on the release PR).

Notable product work in this window includes co-publish of the CLI (#845),
getting-started and call/IR onboarding (#868 to #870), CVC5 equating parity
(#871), and in-memory IR synthesis on check (#872), plus fixed-width signed
ordering and multi-contract IR selection fixes.

v0.2.0

Assura 0.2.0

Assura is a contract-first language: you write what code should do, the compiler and SMT solvers check it, and the toolchain generates Rust.

This release improves what you can name and prove in contracts, how assura check reports partial work, and how reliable the published library crates are for embeds and downstream tools.

What's new

Named limits that resolve and verify

feature_max constants are registered in name resolution, so contracts and demos can use named bounds (for example buffer caps and length limits) without unresolved-name noise. CVE-style demos, including zlib inflate, use those bounds with input-only ensures that Z3 can prove without an IR implementation body.

Incremental contracts you can actually parse and check

Top-level incremental Name { ... } blocks are real declarations (state machines, steps, transitions). The SMT path verifies a practical subset:

• block invariants
• step / resume / on bodies when requires and ensures re-parse as ordinary boolean predicates

The zlib inflate demo verifies the InflateDecoder invariant and related ensures end-to-end. Rich typestate in some on clauses may still be skipped as a known limitation warning rather than a false hard failure.

Honest feedback from assura check

Sparse contracts (for example requires-only) no longer look like a full green verify with nothing useful reported. Human output and JSON expose vacuous / no-obligation cases more clearly, and long verification names are truncated so terminals stay readable.

Stronger library packaging

crates.io co-publish is more robust for the public library stack (dependency order including dev path deps, rate-limit retries, skip already-uploaded versions, IR prompt templates inside assura-smt, and a CI cargo package gate). That reduces “works in the monorepo, fails as a tarball” regressions for anyone depending on assura-pipeline and friends at 0.2.0.

Get Assura

Compiler CLI: installers on the v0.2.0 GitHub Release (cargo-dist shell installer and platform builds).

Embed the compiler in Rust: depend on 0.2.0 crates from crates.io. Prefer assura-pipeline as the public entry point (compile / compile_full / verify_typed). Details: docs/CRATES-IO.md.

From a workspace checkout, contributors can still build the full tool with cargo build -p assura or cargo install --path crates/assura-cli.

After you upgrade

• Run assura check on your contracts and demos. SMT known-limitation skips use A05102 and the marker not yet encoded in SMT; those are warnings when that marker is present, not a broken install.
• Incremental state machines with heavy typestate may still show gaps; simple boolean step/resume and invariants are the supported subset in 0.2.0.

Full commit list

Machine-generated history: CHANGELOG.md (v0.1.0 → v0.2.0).

v0.1.0

Assura 0.1.0

First public release of Assura: a contract-first language that type-checks and verifies what code should do, then generates Rust.

This release ships the compiler libraries on crates.io and CLI installers on this GitHub Release.

Highlights

• End-to-end pipeline: parse → name resolution → type-checking with domain checkers → SMT verification → Rust codegen
• SMT-backed contracts: Z3 is the default solver and is included for normal builds; CVC5 is available as an optional second solver
• AI-native workflow: write contracts, verify them, generate Rust; demos under demos/ show real vulnerability patterns as contracts
• Embeddable compiler: add assura-pipeline from crates.io to compile and verify from your own tools
• Dual license: MIT OR Apache-2.0

Install the CLI

Use the prebuilt binaries and installers attached to this GitHub Release (cargo-dist). That is the supported install path for 0.1.0.

From a full source checkout you can also build the CLI with:

cargo install --path crates/assura-cli

Solvers:

• Z3 (default): included for normal builds. No separate Z3 install for the usual path.
• CVC5 (optional): enable with the cvc5-verify feature when you want the second solver. See CONTRIBUTING.md and scripts/setup-cvc5.sh if you build that path from source.

Use as a library

Depend on the public entry point:

assura-pipeline = "0.1.0"

That crate pulls in the published compiler stack (assura-parser, assura-types, assura-smt, and related crates). Details: docs/CRATES-IO.md.

Try it

assura check demos/libwebp-huffman.assura
assura check demos/libwebp-huffman.assura --verbose

Documentation

• README
• Tutorial
• crates.io publish notes
• Contributing