Installing and Running Flux

You can install and then run Flux either on a single file or on an entire crate.

Quick Install (Linux / macOS)

curl -fsSL https://raw.githubusercontent.com/flux-rs/flux/main/install.sh | bash

Requirements

rustup

Rustup is required because Flux needs access to the source code of the Rust compiler, which we grab from rustup.
liquid-fixpoint

Nightly binary builds are avilable on GitHub Releases. If there is no binary available for your platform, you will need to build it from source.
z3 4.15 or later

You can download a binary for your platform from Z3 GitHub Releases. We recommend downloading the latest version, but older version should also work.

Note: Make sure that the liquid-fixpoint and z3 binaries are in your $PATH.

Install

The only way to use Flux is to build it from source.

First you need to clone the repository

git clone https://github.com/flux-rs/flux
cd flux

To build the source you need a nightly version of rustc. We pin the version using a toolchain file (more info here). If you are using rustup, no special action is needed as it should install the correct rustc version and components based on the information on that file.

Next, run the following to build and install flux binaries

cargo xtask install

This will install two binaries flux and cargo-flux in your cargo home. These two binaries should be used respectively to run Flux on either a single file or on a project using cargo. The installation process will also copy the Flux sysroot (the driver and precompiled libraries) to $HOME/.flux/sysroot.

Flux Home

The Flux home is the directory $HOME/.flux. Its location can be changed by setting the FLUX_HOME environment variable. It contains:

config.toml — Your personal configuration, which applies to every invocation of cargo flux. It is never modified by Flux.
sysroot/ — The Flux sysroot, i.e., flux-driver and the precompiled Flux libraries. It is managed by cargo xtask install and cargo xtask uninstall, which replace or remove the whole directory, so it is safe to delete. Use the FLUX_SYSROOT environment variable to use a sysroot in a different location.

Running on a package: `cargo-flux`

The most common way to use Flux is to run it on a Cargo package. This allows you to check an entire crate in one command, cargo flux.

Step 1: Install Flux

Install Flux as described above.

Step 2: Enable Flux for the Package

By default, Flux won't verify a package unless it's explicitly enabled in the manifest. To do so add the following to Cargo.toml:

[package.metadata.flux]
enabled = true

Now you can run cargo flux to check the package.

In step 2, you will likely get some refinement errors, and to remove those you will need to add some refinement annotations to your code. To do so, add the following to your Cargo.toml, which adds the procedural macros Flux uses to your project

[dependencies]
flux-rs = { git  = "https://github.com/flux-rs/flux.git" }

Then, import attributes from flux_rs and add the appropriate refinement annotations.

#![allow(unused)]
fn main() {
use flux_rs::attrs::*;

#[spec(fn(x: i32) -> i32{v: x < v})]
fn inc(x: i32) -> i32 {
    x - 1
}
}

Running on a File: `flux`

You can use flux as you would use rustc. For example, the following command checks the file test.rs.

flux path/to/test.rs

The flux binary accepts the same flags as rustc. You could for example check a file as a library instead of a binary like so

flux --crate-type=lib path/to/test.rs

When running flux on a file with flux path/to/test.rs, refinement annotations should be prefixed with flux::.

For example, the refinement below will only work when running flux which is intended for use on a single file.

#![allow(unused)]
fn main() {
#[flux::spec(fn(x: i32) -> i32{v: x < v})]
fn inc(x: i32) -> i32 {
    x - 1
}
}

A tiny example

The following example declares a function inc that returns an integer greater than the input. We use the nightly feature register_tool to register the flux tool in order to add refinement annotations to functions.

#![allow(unused)]
fn main() {
#[flux::spec(fn(x: i32) -> i32{v: x < v})]
pub fn inc(x: i32) -> i32 {
    x - 1
}
}

You can save the above snippet in say test0.rs and then run

flux --crate-type=lib path/to/test0.rs

you should see in your output

error[FLUX]: postcondition might not hold
 --> test0.rs:3:5
  |
3 |     x - 1
  |     ^^^^^

as indeed x - 1 is not greater than x as required by the output refinement i32{v: x < v}.

If you fix the error by replacing x - 1 with x + 1, you should get no errors in the output (the output may be empty, but in this case no output is a good thing).

Read these chapters to learn more about what you specify and verify with flux.

A note about the flux-driver binary

The flux-driver binary is a rustc driver (similar to how clippy works) meaning it uses rustc as a library to "drive" compilation performing additional analysis along the way. Running the binary requires dynamically linking a correct version of librustc. Thus, to avoid the hassle you should never execute it directly. Instead, use flux or cargo-flux.

Editor Support

This section assumes you have installed cargo-flux.

Rust-Analyzer in VSCode

Add this to the workspace settings i.e. .vscode/settings.json

{
  "rust-analyzer.check.overrideCommand": [
    "cargo",
    "flux",
    "--workspace",
    "--message-format=json-diagnostic-rendered-ansi"
  ]
}

Note: Make sure to edit the paths in the above snippet to point to the correct locations on your machine.

Configuration

A package is configured in two places:

The [package.metadata.flux] table in Cargo.toml describes properties of the crate, i.e., what is verified. See The Manifest Format.
.flux/config.toml files control how cargo flux runs, e.g., caching, timeouts or extra output. See Configuration.

Flux Flags

The flux binary accepts configuration flags in the format -Fname=value. For boolean flags, the value can be one of y, yes, on, true, n, no, off, false. Alternatively, the value can be omitted which will default to true. For example, to set the solver to cvc5 and enable qualifier scraping:

flux -Fsolver=cvc5 -Fscrape-quals path/to/file.rs

For all available flags, see https://flux-rs.github.io/flux/doc/flux_config/flags/struct.Flags.html

When running cargo flux, flags defined in the FLUXFLAGS environment variable are passed to all packages checked by Flux, for example, to print timing information:

FLUXFLAGS="-Ftimings" cargo flux

See how flags are combined for how these flags interact with the manifest and the configuration files.

Verbose Flag

One particularly useful flag is

FLUXFLAGS="-Fflux-verbose" cargo flux

This will make flux print out a log of what it is upto, e.g. the name of the last function checked. This is helpful, e.g. if flux ICEs (hits an internal error), so you can see which function's code caused the issue, so you might mark it as trusted, so flux can skip checking its body, and hence, live to fight another day...

The Flux Book