Rust feature support

The table below tries to summarize the current support in Kani for the Rust language features according to the Rust Reference. We use the following values to indicate the level of support:

  • Yes: The feature is fully supported. We are not aware of any issue with it.
  • Partial: The feature is at least partially supported. We are aware of some issue with with it.
  • No: The feature is not supported. Some support may be available but analyses should not be trusted.

As with all software, bugs may be found anywhere regardless of the level of support. In such cases, we would greatly appreciate that you filed a bug report.

3.1Macros By ExampleYes
3.2Procedural MacrosYes
4Crates and source filesYes
5Conditional compilationYes
6.2Extern cratesYes
6.3Use declarationsYes
6.5Type aliasesYes
6.9Constant itemsYes
6.10Static itemsYes
6.13External blocksYes
6.14Generic parametersYes
6.15Associated ItemsYes
8.2.1Literal expressionsYes
8.2.2Path expressionsYes
8.2.3Block expressionsYes
8.2.4Operator expressionsYes
8.2.5Grouped expressionsYes
8.2.6Array and index expressionsYes
8.2.7Tuple and index expressionsYes
8.2.8Struct expressionsYes
8.2.9Call expressionsYes
8.2.10Method call expressionsYes
8.2.11Field access expressionsYes
8.2.12Closure expressionsYes
8.2.13Loop expressionsYes
8.2.14Range expressionsYes
8.2.15If and if let expressionsYes
8.2.16Match expressionsYes
8.2.17Return expressionsYes
8.2.18Await expressionsNoSee Notes - Concurrency
10.1.1Boolean typeYes
10.1.2Numeric typesYes
10.1.3Textual typesYes
10.1.4Never typeYes
10.1.5Tuple typesYes
10.1.6Array typesYes
10.1.7Slice typesYes
10.1.8Struct typesYes
10.1.9Enumerated typesYes
10.1.10Union typesYes
10.1.11Function item typesYes
10.1.12Closure typesPartialSee Notes - Advanced features
10.1.13Pointer typesPartialSee Notes - Advanced features
10.1.14Function pointer typesPartialSee Notes - Advanced features
10.1.15Trait object typesPartialSee Notes - Advanced features
10.1.16Impl trait typePartialSee Notes - Advanced features
10.1.17Type parametersPartialSee Notes - Advanced features
10.1.18Inferred typePartialSee Notes - Advanced features
10.2Dynamically Sized TypesPartialSee Notes - Advanced features
10.3Type layoutYes
10.4Interior mutabilityYes
10.5Subtyping and VarianceYes
10.6Trait and lifetime boundsYes
10.7Type coercionsPartialSee Notes - Advanced features
10.9Lifetime elisionYes
11Special types and traitsPartial
Operator TraitsPartial
Deref and DerefMutYes
15.1Unsafe functionsYes
15.2Unsafe blocksYes
15.3Behavior considered undefinedPartial
Data racesNoSee Notes - Concurrency
Dereferencing dangling raw pointersYes
Dereferencing unaligned raw pointersNo
Breaking pointer aliasing rulesNo
Mutating immutable dataNo
Invoking undefined behavior via compiler intrinsicsPartialSee Notes - Intrinsics
Executing code compiled with platform features that the current platform does not supportNo
Producing an invalid value, even in private fields and localsNo

Notes on partially or unsupported features

Code generation for unsupported features

Kani aims to be an industrial verification tool. Most industrial crates may include unsupported features in parts of their code that do not need to be verified. In general, this should not prevent users using Kani to verify their code.

Because of that, the general rule is that Kani generates an assert(false) statement followed by an assume(false) statement when compiling any unsupported feature. assert(false) will cause verification to fail if the statement is reachable during the verification stage, while assume(false) will block any further exploration of the path. However, the analysis will not be affected if the statement is not reachable from the code under verification, so users can still verify components of their code that do not use unsupported features.

In a few cases, Kani aborts execution if the analysis could be affected in some way because of an unsupported feature (e.g., global ASM).


Kani does not support assembly code for now. We may add it in the future but at present there are no plans to do so.

Check out the tracking issues for inline assembly (asm! macro) and global assembly (asm_global! macro) to know more about the current status.


Concurrent features are currently out of scope for Kani. In general, the verification of concurrent programs continues to be an open research problem where most tools that analyze concurrent code lack support for other features. Because of this, Kani emits a warning whenever it encounters concurrent code and compiles as if it was sequential code.

Standard library functions

Kani overrides a few common functions (e.g., print macros) to provide a more verification friendly implementation.

Advanced features

The semantics around some advanced features (traits, types, etc.) from Rust are not formally defined which makes it harder to ensure that we can properly model all their use cases.

In particular, there are some outstanding issues to note here:

  • Sanity check Variant type in projections #448.
  • Unexpected fat pointer results in #277, #327 and #676.

We are particularly interested in bug reports concerning these features, so please file a bug report if you're aware of one.

Panic strategies

Rust has two different strategies when a panic occurs:

  1. Stack unwinding (default): Walks back the stack cleaning up the data from each function it encounters.
  2. Abortion: Immediately ends the program without cleaning up.

Currently, Kani does not support stack unwinding. This has some implications regarding memory safety since programs sometimes rely on the unwinding logic to ensure there is no resource leak or persistent data inconsistency. Check out this issue for updates on stack unwinding support.

Uninitialized memory

Reading uninitialized memory is considered undefined behavior in Rust. At the moment, Kani cannot detect if memory is uninitialized, but in practice this is mitigated by the fact that all memory is initialized with nondeterministic values. Therefore, any code that depends on uninitialized data will exhibit nondeterministic behavior. See this issue for more details.


At present, we are aware of some issues with destructors, in particular those related to advanced features.


Please refer to Intrinsics for information on the current support in Kani for Rust compiler intrinsics.

Floating point operations

Kani supports floating point numbers, but some supported operations on floats are "over-approximated." These are the trigonometric functions like sin and cos and the sqrt function as well. This means the verifier can raise errors that cannot actually happen when the code is run normally. For instance, (#1342) the sin/cos functions basically return a nondeterministic value between -1 and 1. In other words, they largely ignore their input and give very conservative answers. This range certainly includes the "real" value, so proof soundness is still preserved, but it means Kani could raise spurious errors that cannot actually happen. This makes Kani unsuitable for verifying some kinds of properties (e.g. precision) about numerical algorithms. Proofs that fail because of this problem can sometimes be repaired by introducing "stubs" for these functions that return a more acceptable approximation. However, note that the actual behavior of these functions can vary by platform/os/architecture/compiler, so introducing an "overly precise" approximation may introduce unsoundness: actual system behavior may produce different values from the stub's approximation.