Using Kani to write and validate Rust code with ChatGPT

It’s no news that many software developers now use ChatGPT as their coding buddy. You can ask it coding questions, to refactor your code, for help with debugging, and almost anything else you can think of.

While ChatGPT can generate these responses for you, there’s no guarantee that the code will run, or that it will be error-free — even though it might seem like valid code. This might result in buggy software or missed issues in your final project.

In situations like these, code verification tools like Kani come in handy.

Kani is designed specifically for Rust code. It uses automated reasoning, a field of computer science that attempts to prove what is possible with a system and what is impossible. This allows it to detect problems in your code in seconds that would otherwise take several hours or even longer to solve manually or via unit testing.

In this guide, we’ll learn how to write Rust code with ChatGPT and prove its validity with Kani. We will cover:

• Setting up Kani in your Rust project
• Using Kani to verify ChatGPT’s Rust code
• Using ChatGPT to fix code errors
• Another example using Kani and ChatGPT
• Considerations while using Kani

To follow along, you should have Rust installed. I suggest you use Rustup to quickly install Rust for your OS. Run the command below to install Rust with Rustup:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

This installation will take a while to complete, but it’ll come with the latest Rust version and complementary tools you’ll need — including Cargo, Rust’s package manager. Once it’s complete, run cargo --version to confirm that your installation was successful.

Setting up Kani in your Rust project

To use Kani, we need to install it. Kani requires that you have Python v3.6 or newer and Rust v1.58 or newer. We’ll just install the latest versions of both Rust and Python.

In case you don’t have Python, start by installing Python from the official website for your operating system. Then, run the following commands to install and set up Kani:

cargo install --locked kani-verifier
cargo kani setup

In the code above, the first command will build and place kani and cargo-kani binaries in ~/.cargo/bin. The second one will download the Kani compiler and other required dependencies, then place them in ~/.kani/.

When the installation is complete, verify that the installation was successful by creating an app.rs file and adding this code snippet to it:

#[kani::proof]
fn main() {
    assert!(1 == 2);
}

Then run kani app.rs on your terminal. The result you see should look like the one below, which indicates that Kani is installed and is working as expected:

Now that we have Rust and Kani installed, let’s explore how we can use Kani to verify Rust code generated by ChatGPT.

Using Kani to verify ChatGPT’s Rust code

Let’s say you want to develop a feature for a fintech application using Rust that enables users to securely transfer funds between different accounts.

To ask ChatGPT, we want to try to be more precise and more descriptive, so we’ll use a prompt like the one below:

Hey ChatGPT, could you write a program in Rust that represents a basic banking system? The system should be able to create individual accounts with names and balances. It should also have the ability to transfer funds between accounts. In the case of insufficient funds, an error message should be displayed. Finally, demonstrate a scenario where funds are successfully transferred between two accounts, and their final balances are then displayed.

Here is an example of the response we might get:

It’s important to note that I used ChatGPT 4 for this example, which is more advanced compared to ChatGPT 3.5.

If you try to run this code, what do you think the result will be? Don’t think about it too much — it should run successfully, and the result should look like so:

But does this code always work as expected? So far, it executes without a hitch. Sure, you could write unit tests for some foreseeable errors, but let’s face it — there might be countless scenarios you haven’t thought of yet.

This is where tools like Kani come into play, helping us tackle those unexpected edge cases. It’s time to put our ChatGPT-generated code to the test with Kani.

To test with Kani, we’ll replace the balance value with kani::any(), which will essentially allow kani to reason the code against all possible cases. If we run it with the initial static value, kani will always return a successful result, which is not what we want.

Here is how we’ll modify the code to use kani:

#[kani::proof]
fn main() {
    let mut account1 = Account {
        name: "Obiageli".to_string(),
        balance: kani::any(),
    };
    let mut account2 = Account {
        name: "Emeka".to_string(),
        balance: kani::any(),
    };
    process_transfer(&mut account1, &mut account2, 100);
    println!("{}'s account balance: {}, and {}'s account balance: {}", account1.name, account1.balance, account2.name, account2.balance)
}

First, we need to add kani::proof to our main function. This tells kani about the inputs we’re using in that function and makes the function Kani-aware 🙂

Then, we run our code using kani. To do this, just type cargo kani. In our case, you should see a lot of success messages, one fail, and some warnings. Here’s a sample of what the Kani analysis might look like:

shell
...
Check 25: std::intrinsics::is_nonoverlapping::<u8>.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: ../../../../runner/.rustup/toolchains/nightly-2023-04-30-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/intrinsics.rs:2547:43 in function std::intrinsics::is_nonoverlapping::<u8>

Check 26: std::intrinsics::is_nonoverlapping::<u8>.assertion.2
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: ../../../../runner/.rustup/toolchains/nightly-2023-04-30-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/intrinsics.rs:2547:74 in function std::intrinsics::is_nonoverlapping::<u8>

SUMMARY:
 ** 1 of 155 failed (3 unreachable)
Failed Checks: attempt to add with overflow
 File: "/Users/{username}/Development/logrocket/usekani/src/main.rs", line 38, in process_transfer

VERIFICATION:- FAILED
Verification Time: 0.8893617s

Summary:
Verification failed for - main
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

As we can see in the error messages, there’s a chance our program might encounter various forms of overflow errors.

Interestingly, Rust operates differently in debug and release modes when handling such errors. In debug mode, Rust throws overflow errors, while in release mode, instead of an error, you’ll find a 0 returned. This differs from languages like C.

Even though this is the case, it’s important to address these overflow issues, as they can result in unexpected behavior. Thankfully, we can use ChatGPT to assist us in fixing the problem.

Using ChatGPT to fix code errors

You just need to provide the error messages and ask ChatGPT to fix the code based on the errors returned. For me, ChatGPT acknowledged that there was an error and gave an explanation:

Then, after the explanation, it gave the solution below:

struct Account {
    name: String,
    balance: u32,
}
fn process_transfer(from_account: &mut Account, to_account: &mut Account, amount: u32) {
    if from_account.balance < amount {
        println!("Error: insufficient funds in account {}", from_account.name);
        return;
    }

    if to_account.balance.checked_add(amount).is_none() {
        println!("Error: transfer would result in an overflow in account {}", to_account.name);
        return;
    }

    from_account.balance -= amount;
    to_account.balance += amount;
}
#[kani::proof]
fn main() {
    let mut account1 = Account {
        name: "Obiageli".to_string(),
        balance: kani::any(),
    };
    let mut account2 = Account {
        name: "Emeka".to_string(),
        balance: kani::any(),  // just for demonstration purposes
    };
    process_transfer(&mut account1, &mut account2, 100);
    println!("{}'s account balance: {}, and {}'s account balance: {}", account1.name, account1.balance, account2.name, account2.balance)
}

Without modifying the code any further, we’ll test it by running cargo kani. The response is all green — in other words, successful — as shown below:

SUMMARY:
 ** 0 of 167 failed (3 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.91400814s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Sometimes, you may need to look at the code yourself — in fact, you should always do so — and change some parts where necessary. Checking your code manually can help you avoid situations where ChatGPT confidently but wrongly makes mistaken guesses, also called hallucinations.

For example, if the codebase is large, it’s better to split your code into parts; if the function is way too large, that might be a problem on its own.

Another example using Kani and ChatGPT

Let’s consider another scenario in which we want to get an item from a vector based on its position in the vector. For example, say you supply a function with a vector and the index of the item in the vector.

When we ask ChatGPT to generate code to solve this problem, it should generate something like the code below:

fn get_value(vec: &Vec<i32>, index: usize) -> Option<&i32> {
    if vec.is_empty() {
        None
    } else {
        Some(&vec[index])
    }
}

fn main() {
    let vec = vec![1, 2, 3];
    match get_value(&vec, 0) {
        Some(value) => println!("{}", value),
        None => println!("No value found."),
    }
}

You may wonder, “What’s the issue with this code?”

Sure, it works as expected most of the time, but it falls short in certain cases. Can you guess when?

If your guess involved a situation where the user inputs an index that is out of bounds, you’re right! We have just three items in the vector, with an index from zero to two. If a user inputs 3, an out-of-bounds error will occur.

It seems like an error like this should be easy to catch, right? But sometimes, you might not figure out the problem early enough. In these situations, a verification tool like Kani can help. Let’s run the code through Kani to see what we can get.

Replace your previous code or comment it out and paste the example above, then run cargo kani to get an output that should look something like this:

We can simply copy the error message and ask ChatGPT to fix it, and it’ll give us a fix. Here is the response I got from ChatGPT:

With that, we’ve successfully used ChatGPT to generate code and then got it to fix the errors in the code it generated, all thanks to Kani.

Considerations while using Kani

While Kani can improve the overall efficiency of your code and reduce the chances of bugs happening, be aware that it can also increase complexity and development time.

Using Kani may add to the overall time-consuming cost of writing code with Rust, as it comes with its own complexity. You’ll have to deal with the Rust compiler, writing tests, and other parts of the software development lifecycle.

As such, for some projects, writing unit or integration tests might be all you need. However, for mission-critical applications, Kani will be extremely useful in helping you ensure that you’ve covered all the edge cases for your code.

Final words

ChatGPT and the rest of the long list of AI code generators are awesome, but they are not perfect. However, we can leverage them to build better software in record time.

In this article, we touched on how you can use Kani, a Rust automated reasoning verification tool, to check code generated using ChatGPT. Leveraging these tools together can help you build better, error-free software programs.

While static analysis tools like rust-analyzer can help you to a large extent when writing Rust code, verification tools like Kani can even take you further. Leveraging a combination of AI developer tools will allow you to write code you’ll be proud of and boost your productivity while you’re at it.

Happy hacking!