Add Tool: Flux

[nilehmann]

Tool Name

Flux

Description

Flux is a refinement type checker for Rust that lets you specify a range of correctness properties and have them be verified at compile time. Specifically, Flux lets you write pre- and post-condition contracts much like Kani, Prusti, Verus, etc., but uses type structure to simplify the specification and verification when possible, and to support various Rust idioms like closures, iterators, traits, and so on. More details can be found at https://flux-rs.github.io/flux/

Tool Information

Does the tool perform Rust verification? YES
Does the tool deal with unsafe Rust code? YES, in a conservative manner, i.e. without tracking the values of data written through pointers.
Does the tool run independently in CI? YES
Is the tool open source? YES
Is the tool under development? YES
Will you or your team be able to provide support for the tool? YES

Comparison to Other Approved Tools

Compared to Kani and GOTO Transcoder, Flux performs unbounded verification (as opposed to bounded model checking).

Compared to Verifast, Flux is aimed to (1) be a more “lightweight” verifier, meaning that all verification is automated via SMT solving, (2) support more Rust features including traits, closures etc.

Licenses

Flux uses the MIT license so we do not expect any conflict with the Rust standard library license(s).

Steps to Use the Tool

1. Download and Install z3 or cvc5
2. Download and install liquid-fixpoint following instructions here, e.g., cabal install liquid-fixpoint
3. Download and install Flux

   $ git clone https://github.com/flux-rs/flux
   $ cd flux
   $ cargo xtask install
   

4. Configure Flux to run on the desired crate by adding the following to the crate’s Cargo.toml

   [package.metadata.flux]
   enabled = true
   

5. Run Flux

   $ cargo flux
   

Artifacts & Audit Mechanisms

You can see how Flux runs on this demo repository https://github.com/flux-rs/flux-demo. A more substantial example is using Flux to verify process isolation in the Tock OS kernel (paper in submission, available on request) https://github.com/PLSysSec/tock/tree/master/kernel

The Flux repository itself contains about 740 tests that are run in CI, in addition to the entire Tock kernel linked above.

Flux is described in the following papers

• “FLUX: Liquid Types for Rust”, PLDI 2023 https://dl.acm.org/doi/10.1145/3591283
• “Generic Refinement Types”, POPL 2025 https://dl.acm.org/doi/10.1145/3704885

Versioning & CI

We implemented a proof of concept that runs Flux on the standard library by using Cargo’s --build-std flag and the __CARGO_TESTS_ONLY_SRC_ROOT environment variable to point to a local copy of the std. We believe Kani uses the same strategy.

We don’t currently do releases, but Flux can be easily built on CI, so the proposal is to pin a specific commit. One potential issue is that, like Kani, Flux has to be built against a specific toolchain, which has to be updated lockstep with the local copy of the std.

[tautschnig]

Thank you very much for your tool application! Please go ahead and create a pull request that introduces Flux into CI. That said: what challenges do you foresee in applying Flux to the standard library?

[nilehmann]

Thank you for the fast reply. We'll start working on the pull request!

We are considering 8: Contracts for SmallSort and 17: Verify the safety of slice functions. But for the time being, we have been fixing issues to make Flux run on the std, so we haven't looked at the challenges in great detail.