Assura

Write what it should do. AI proves it does.

A contract-first language for the AI era. You write behavioral contracts. AI writes the implementation. An SMT solver proves it correct, or hands you the exact input that breaks it. Ships as Rust.

Docs · Getting started · Try in browser · What we prove · Contributing

A test tells you it failed. Assura tells you why.

Here is a real invariant from the zip crate's central-directory parser. The archive offset is computed as cd_offset - relative_cd_offset, an unchecked subtraction on a u64:

contract FindCdSubtractSafe {
    input(cd_offset: Nat, relative_cd_offset: Nat, eocd_offset: Nat)

    requires { cd_offset <= 18446744073709551615 }
    requires { relative_cd_offset <= 18446744073709551615 }
    requires { eocd_offset <= 18446744073709551615 }
    requires { cd_offset <= eocd_offset }

    // archive_offset = cd_offset - relative_cd_offset (unchecked)
    ensures { cd_offset >= relative_cd_offset }
}

Run it:

$ assura check demos/zip-crate-audit.assura

  FindCdSubtractSafe:
    ensures              ... COUNTEREXAMPLE
      | cd_offset = 0, eocd_offset = 0, relative_cd_offset = 1

This file has no implementation body. The check asks whether those preconditions imply the ensures. They do not. For this linear query the solver returns one input inside the preconditions that underflows: a crafted archive whose central directory claims a relative offset larger than its absolute one. A fuzzer might find this. A complete decision procedure for this fragment does not miss it. Where the encoding is incomplete, the result is Unknown, not a green check.

The human line keeps the raw digits. A value on a width bound, within 32 of one, or an exact power of two from 2^8 up also gets a note, for example 18446744073709551586 (u64::MAX - 29). --json leaves variables as the raw digits.

You get Verified, a Counterexample, or an honest Unknown.

Regenerate: vhs assets/demo/assura-check.tape (requires VHS and assura on PATH).

Related MCP server: CSL-Core

Try it without installing anything

The devcontainer installs Rust and libz3-dev. The first build takes a few minutes. A warm start needs Codespaces prebuilds enabled in the repo settings. Without that, the build still runs when the container is created. After the build:

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

Install

cargo install assura --locked

Needs a Rust toolchain (edition 2024 / rustc 1.88+). Z3 comes prebuilt via the z3 crate. No manual Z3 install for a normal build. See Getting started for Homebrew, the LSP, and the unpublished VS Code extension.

Prefer a binary? Use the shell installer (Linux x86_64, macOS arm64/x64):

curl --proto '=https' --tlsv1.2 -LsSf \
  https://github.com/assura-lang/assura/releases/latest/download/assura-installer.sh | sh

Then:

assura init my-project
cd my-project
assura check contracts/lib.assura    # prove the scaffold (add --json for agents)
assura build contracts/lib.assura    # emit Rust

Full command reference, LSP, VS Code extension, and library embedding: Getting started · Cheatsheet

MCP server

This repository contains the MCP server. The implementation is the Rust crate crates/assura-mcp. It uses the rmcp SDK with the server and transport-io features. There is no separate assura-mcp binary. The assura command starts that server on stdio:

assura mcp

{
  "mcpServers": {
    "assura": {
      "command": "assura",
      "args": ["mcp"]
    }
  }
}

The process speaks MCP on stdin and stdout. With no host attached, the terminal looks idle.

crates/assura-mcp registers these tools:

A check returns Verified, a Counterexample, or Unknown. Unknown means the solver did not decide. Stop when there is no Counterexample. Do not keep rewriting because a clause is Unknown.

The official MCP Registry name is io.github.assura-lang/assura. Agent details: For AI agents.

Why this exists

AI writes a lot of new code, and reviewing it is the bottleneck. AI-generated tests are especially weak here: they tend to mirror the implementation. If divide(10, 0) returns 0 because of a bug, the generated test asserts == 0. The test passes. The bug ships.

Assura replaces that trust with proof. Contracts state what must hold. With an implementation (IR, synthesized body, or check-rust), Z3/CVC5 checks that body against the contract. With no body, as in the zip example above, it checks whether the ensures follows from the requires. Either way you get a counterexample the AI can fix against, for the fragments the solver can model. A loop can close without a human guessing at edge cases.

Property tests and fuzzing sample the input space. A solver reasons over all of it, for the fragments it can model. Where it cannot, Assura says Unknown rather than pretending. The honest map of that boundary is What we prove.

How it works

contracts (.assura) ──► AI generates implementation
                              │
                              ▼
                     Assura verifies (Z3 / CVC5)
                              │
        ┌─────────────────────┴──────────────────────┐
        │                                            │
   counterexample ──► back to the AI            proof holds
        ▲                    │                       │
        └────────────────────┘                       ▼
                                          Rust source ──► rustc ──► binary / WASM

Three tiers, fastest first:

Real CVEs, as contracts

More in demos/ and one worked example per feature in examples/. Case studies: docs/CASE-STUDIES.md.

Contributing

New here? Good first issues are kept stocked and scoped. Each one names the file to open and how to verify it.

Bug reports are just as valuable as patches. If assura check gives you a wrong answer, a confusing counterexample, or an Unknown you think should verify, open an issue. Those reports are how the solver encoding gets better.

Start with CONTRIBUTING.md. Architecture and crate map: docs/INTERNALS.md.

Documentation

Site: assura-lang.github.io/assura (not assura.dev, a different product)

A project activates only the categories it needs. CORE is always on.

License

Dual-licensed under MIT or Apache-2.0, at your option.