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.1||Macros By Example||Yes|
|4||Crates and source files||Yes|
|8.2.6||Array and index expressions||Yes|
|8.2.7||Tuple and index expressions||Yes|
|8.2.10||Method call expressions||Yes|
|8.2.11||Field access expressions||Yes|
|8.2.15||If and if let expressions||Yes|
|8.2.18||Await expressions||No||See Notes - Concurrency|
|10.1.11||Function item types||Yes|
|10.1.12||Closure types||Partial||See Notes - Advanced features|
|10.1.13||Pointer types||Partial||See Notes - Advanced features|
|10.1.14||Function pointer types||Partial||See Notes - Advanced features|
|10.1.15||Trait object types||Partial||See Notes - Advanced features|
|10.1.16||Impl trait type||Partial||See Notes - Advanced features|
|10.1.17||Type parameters||Partial||See Notes - Advanced features|
|10.1.18||Inferred type||Partial||See Notes - Advanced features|
|10.2||Dynamically Sized Types||Partial||See Notes - Advanced features|
|10.5||Subtyping and Variance||Yes|
|10.6||Trait and lifetime bounds||Yes|
|10.7||Type coercions||Partial||See Notes - Advanced features|
|11||Special types and traits||Partial|
|15.3||Behavior considered undefined||Partial|
|Data races||No||See Notes - Concurrency|
|Dereferencing dangling raw pointers||Yes|
|Dereferencing unaligned raw pointers||No|
|Breaking pointer aliasing rules||No|
|Mutating immutable data||No|
|Invoking undefined behavior via compiler intrinsics||Partial||See Notes - Intrinsics|
|Executing code compiled with platform features that the current platform does not support||No|
|Producing an invalid value, even in private fields and locals||No|
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
statement followed by an
assume(false) statement when compiling any
assert(false) will cause verification to fail if the
statement is reachable during the verification stage, while
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
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.
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.
Kani overrides a few common functions (e.g., print macros) to provide a more verification friendly implementation.
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
Varianttype 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.
Rust has two different strategies when a panic occurs:
- Stack unwinding (default): Walks back the stack cleaning up the data from each function it encounters.
- 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.
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.
Kani supports floating point numbers, but some supported operations on floats are "over-approximated."
These are the trigonometric functions like
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
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.