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:
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.
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.
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.
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.
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.
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.
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!
Debugging Rust applications can be difficult, especially when users experience issues that are hard to reproduce. If you’re interested in monitoring and tracking the performance of your Rust apps, automatically surfacing errors, and tracking slow network requests and load time, try LogRocket.
LogRocket is like a DVR for web and mobile apps, recording literally everything that happens on your Rust application. Instead of guessing why problems happen, you can aggregate and report on what state your application was in when an issue occurred. LogRocket also monitors your app’s performance, reporting metrics like client CPU load, client memory usage, and more.
Modernize how you debug your Rust apps — start monitoring for free.
Hey there, want to help make our blog better?
Join LogRocket’s Content Advisory Board. You’ll help inform the type of content we create and get access to exclusive meetups, social accreditation, and swag.
Sign up nowSOLID principles help us keep code flexible. In this article, we’ll examine all of those principles and their implementation using JavaScript.
JavaScript’s Date API has many limitations. Explore alternative libraries like Moment.js, date-fns, and the new Temporal API.
Explore use cases for using npm vs. npx such as long-term dependency management or temporary tasks and running packages on the fly.
Validating and auditing AI-generated code reduces code errors and ensures that code is compliant.