5 automatic verification tools for Rust and when to use each

Rust is a popular programming language for its emphasis on safety and reliability, as well as how it enforces best practices by default. Despite these amazing features, it’s not perfect — no language is — and your code logic can sometimes cause unexpected behaviors.

It’s possible to write code that is syntactically correct but inherently buggy. For example, an unsuspecting arithmetic overflow could occur. This is where automatic code verification tools come in handy.

Automatic verification is a technique that helps in proving a program satisfies certain properties, such as memory safety and the absence of runtime errors. Moreover, automatic verification tools enable you to verify the correctness of concurrent code, which can be difficult to test manually.

Automatic verification is particularly important for Rust because it can help to ensure that unsafe code is used correctly. In this guide, we’ll discuss five of the top Rust verification tools — in no particular order — and how they can help you build more reliable software.

The tools we will discuss include:pro

• cargo-fuzz
• Kani
• Proptest
• Rust Klee
• Haybale

Keep in mind that while the Rust community is actively working on developing and improving Rust automatic verification tools, the field of automatic verification tools in general is still evolving.

Check out the comparison table at the end of this article to see which of these tools is production-ready at the time of this writing.

cargo-fuzz

The first tool we will discuss, cargo-fuzz, uses a technique called fuzzing for automated software testing. By providing many valid, nearly valid, or invalid inputs to a program, fuzzing can help developers find undesired behaviors or vulnerabilities.

When we write tests, we typically only consider a few inputs and write the tests based on how we imagine the system will react. This approach can lead to missed bugs, especially those caused by unexpected or malformed inputs.

Fuzzing can help you find these missed bugs by providing the program with a wide variety of inputs, including invalid and unexpected inputs. If the program crashes or behaves unusually in response to one of these inputs, it signals a bug.

The cargo-fuzz Rust crate can help you with fuzz-testing Rust code. It works by generating random inputs and feeding them into the function you want to test. If the function panics or crashes, cargo-fuzz will save the input that caused the failure.

Here is an example of how to use cargo-fuzz to fuzz-test a Rust function:

#![no_main]
#[macro_use]
extern crate libfuzzer_sys;
fuzz_target!(|data: &[u8]| {

    let json_string = std::str::from_utf8(data).unwrap();
    let _ = serde_json::from_str::<serde_json::Value>(&json_string).unwrap();

});

The code above tests the JSON parser by feeding it random inputs. The fuzz_target will continue to be called until it encounters an input that triggers a panic and causes a crash.

The crash report tells you where there was a panic and why. For example:

The report above shows that the panic happened when the program tried to call the Result::unwrap() function on an Error value. It panicked with the following error:

Error("EOF while parsing a value", line: 1, column: 0); 

This information can help you investigate further to determine if it was caused by a bad input that was your code didn’t handle. Thanks to cargo-fuzz, you’ll have the opportunity to fix it.

Keep in mind that some of the bugs you find through fuzzing might not be practical or applicable in real life, which means fuzzing can generate false positives. Moreover, fuzzing can be resource-intensive, especially when fuzzing a large or complex codebase.

Kani

Kani is a modern automatic code verification tool that helps you verify the correctness of your Rust code in a matter of seconds. It uses a technique called model checking, a way of exploring all the possible and impossible states of a program, including states that are unreachable through normal execution.

Model checking allows Kani to detect problems in your code that might result from logic with unintended consequences. You can also use Kani to identify other issues that might be difficult or impossible to find with other unit testing, integration testing, or even manual testing methods.

Let’s consider the code below:

fn product(a: i32, b: i32) -> i32 {
    a * b
}

You’ll agree with me that the code above is a valid Rust code, right? Take a moment and look at it again — can you find anything that could possibly go wrong with this code?

Let’s use Kani to find out:

fn product(a: i32, b: i32) -> i32 {
    a * b
}
#[kani::proof]
fn main() {
    let a = kani::any();
    let b = kani::any();
    let result = product(a, b);
    println!("The product of {} and {} is {}", a, b, result);
}

In the code above, we’ve introduced Kani to prove that the code is correct and that there are no bugs. Kani will give us the following response:

Everything seems right, except that Kani detects the possibility of an overflow during the multiplication process.

This is because the product function does not ensure we don’t exceed the max value of i32, which is 2,147,483,647 — anything larger than that will throw an error. Essentially, whatever this function will be used for will not be able to handle numbers larger than two billion.

In this case, using Kani to identify this potential issue allows you to either change the datatype right away or leave it as is and handle the error properly if it’s an expected behavior.

Like every other tool, Kani has its limitations. Fortunately, these limitations are pretty well-documented. They range from undefined behaviors to some unsupported features in Rust.

Proptest

Proptest allows you to test the properties of a function with numerous valid and invalid inputs to find bugs. This differs from classical testing methods like unit testing, where you specify some inputs and add assertions based on the behavior you expect.

Property testing is a form of fuzz testing that’s more controlled and focused on verifying specific properties. This makes it a good choice for testing complex systems where traditional fuzz testing may be too slow or ineffective.

Let’s take a look at how you can use the Rust Proptest crate:

use proptest::prelude::{any, proptest};

fn add_two_numbers(first_number: i32, second_number: i32) -> i32 {
    first_number + second_number
}

proptest! {
    #[test]
    fn test_add_two_numbers(first_number in any::<i32>(), second_number in any::<i32>()) {
        let expected = first_number + second_number;
        let actual = add_two_numbers(first_number, second_number);
        assert_eq!(actual, expected);
    }
}

In the code above, we are testing a simple function that adds two numbers. What could possibly go wrong with such a straightforward function?

Let’s take a look at the test_add_two_numbers function signature:

fn test_add_two_numbers(first_number in any::<i32>(), second_number in any::<i32>())

The any::<i32>() strategy is a Proptest strategy that generates random i32 values, both valid and invalid. This allows us to test the add_two_numbers() function with a wide range of inputs, including edge cases and anomalies.

The Proptest test function will generate a large number of random inputs for the first_number and second_number parameters.

For each input, the test asserts that the actual output of the add_two_numbers() function is equal to the expected output. If any of the tests fail, Proptest will print the failing inputs to the console.

Here’s an example of how Proptest might generate inputs for the test_add_two_numbers() function:

(10, 20)
(-100, 100)
(1234567890, 9876543210)
(0, 0)
(-1, -1)
(std::i32::MIN, std::i32::MAX)

If a test fails with a particular input, Proptest will also shrink the inputs. For example, if a test fails with the input (10, 20), Proptest might try again with the input (5, 10), or even (1, 2). This helps to identify the smallest possible input that causes the test to fail.

When we run the test, we get a failing test report like the one below:

The report shows that there is a possibility of an overflow. It also shows the minimal reproducible input. With this information, we can proceed to fix the bug.

While property testing can work really well for a select range of inputs, it can sometimes miss some edge cases and give you a false positive or false negative result. In other words, it might hallucinate bugs where there are actually none, or not find a bug outside of the specified coverage.

Rust Klee

KLEE is a symbolic execution engine that allows you to intelligently explore all the code paths in your program to discover vulnerabilities or bugs. It’s built on top of the LLVM compiler infrastructure, which is written in C and C++.

As a result, most KLEE implementations are also in C and C++. However, the fundamental concepts of KLEE can be implemented in any programming language.

Rust Klee is an open source Rust implementation of KLEE. Much like other verification tools we’ve discussed in this guide, Rust Klee was designed to check specific properties. In particular, according to the author’s pilot blog post, it was designed for:

• Safety checks
• Invariants
• Parameterized checks
• Checking the functional correctness of Rust programs

This makes it more focused and efficient than some other verification tools that might be more general-purpose.

However, in the same pilot blog post, the author cautions that the goal of his project was never to “create a verification system that is ready to integrate into any project.” In fact, the repository hasn’t been updated for four years, and it seems there are no plans for further progress.

Rather, the author’s purpose for Rust Klee was to explore whether Rust verification tools based on KLEE could be applied to Rust-for-Linux code to check for bugs. The project’s intention is to provide insights into potential challenges and what needs to be done so others can use formal verification tools to check similar code.

As a result, while Rust Klee isn’t ready for production use, it’s still worth mentioning as a cool tool that could help shape the formal verification landscape in the Rust ecosystem.

Haybale

Haybale is also a symbolic execution engine with similar features to those of Rust Klee, except that Haybale is entirely written in Rust and based on the Rust LLVM IR under the hood.

While it’s not trying to be another Rust Klee, it still has similar functionalities. As a symbolic execution engine, it focuses on converting your entire program variables into mathematical expressions and reasoning the execution paths to detect bugs or vulnerabilities.

The best part of Haybale is that it tests your Rust code as is without adding additional test code. Of course, even though we all agree that writing tests is the best thing to do, it’s still considered a boring and tedious task.

Let’s go over an example that checks if a function foo will return an output of zero. First, we write the function that will be analyzed. You can write this in any programming language and then convert it to bytecode:

fn foo(x: f64) -> f64 {
  x * x - 4.0
}

The bytecode will be saved somewhere in your project, and you can reference it in the project variable in your Rust code:

  let project = Project::from_bc_path("/path/to/file.bc").unwrap();

Now we can use the find_zero_of_func method in haybale to discover bugs that exists in our function when it receives a zero input.

use haybale::{find_zero_of_func, Project};

fn main() {
  let project = Project::from_bc_path("/path/to/file.bc").unwrap();
  match find_zero_of_func("foo", &project, haybale::Config::default(), None) {
    Ok(None) => println!("foo() can never return 0"),
    Ok(Some(inputs)) => println!("Inputs for which foo() returns 0: {:?}", inputs),
    Err(e) => panic!("{}", e),
  }
}

Haybale can reason about the entire code, discover bugs, and return a report that helps you prove whether or not your code has bugs, then reproduce and fix them. Although Haybale might not catch all errors, it will most likely catch critical errors that could lead to crashes at runtime and give you a chance to fix them.

Klee and Haybale have their limitations, like every other automatic verification tool. For example, Klee may not be able to find bugs in executables that use complex abstractions.

As mentioned, symbolic execution engines work by exploring all possible paths through a program’s code to find inputs or conditions that could lead to unexpected behavior or bugs. However, a program using complex abstractions, such as intricate data structures or sophisticated design patterns, can create numerous possible execution paths.

This complexity can overwhelm a tool like Klee or Haybale, making it challenging for them to analyze all potential scenarios effectively. As a result, they may give up during the process. In this case, it’s best to use manual or traditional testing methods to test those sections of the code.

Comparison table of Rust automatic verification tools

Let’s review the five Rust verification tools we’ve discussed in this guide in the following comparison overview:

Tool	Popularity (GitHub stars)	Community support	Best used for…	Version compatibility	Production-ready?
cargo-fuzz	1.3k	Active	Finding bugs caused by unexpected or malformed inputs	Rust 1.45 and higher	✅
Kani	1.4k	Active	Finding bugs caused by logic with unintended consequences and other issues that might be difficult or impossible to find with other testing methods	Rust 1.60 and higher	✅
Proptest	1.4k	Active	Testing the properties of a function with lots of valid and invalid inputs to find bugs	Rust 1.47 and higher	✅
Rust Klee	3	Inactive	Checking specific properties of Rust programs, such as safety invariants and functional correctness	Rust 1.47 and higher	❌
Haybale	455	Not so active	Testing the behavior of a program using symbolic values rather than known inputs	Rust 1.47 and higher	Haybale is still under development, but it is already being used by some projects to verify their code.

Remember, Rust verification tools are still in their early days, and more tools will likely be developed over time.

Conclusion

Automatic verification tools are very important for bug discovery in software development, although they might not yet be widely adopted by developers. These tools can help you discover bugs that you may not otherwise find using classical testing methods and can help improve your code reliability.

While not specific to Rust code, there are some other tools available for code verification and bug detection. For example:

• SonarQube is a static analysis tool that can be used to find bugs in Java, C/C++, and other programming languages
• SPIN is an important code verification tool to consider if you’re working with concurrent systems

Happy hacking!