The gap between correct code and a verified program
LLMs can write Rust that compiles and even passes cargo test. What they cannot do reliably is write a formal proof that the code is correct for all possible inputs.
The problem is not Rust syntax. Formal verification requires stating what you want to prove, finding the invariant that makes the proof go through, and expressing both in a language the verifier accepts. LLMs are trained on source code, not on the act of proving. They see theorems, but they rarely see the twenty failed attempts that preceded the successful proof.
If you paste a recursive binary search into GPT-4 and ask it to “prove this correct,” you will get something that looks like a proof. It will mention loop invariants and preconditions. It will also probably use syntax from Dafny, reference lemmas that do not exist, and assert invariants that are too weak to establish the postcondition. It looks right until you try to check it.
What formal verification of Rust actually looks like
Rust has several verification tools. Kani is a model checker that exhaustively explores all possible states of a function up to some bound. Prusti and Creusot are deductive verifiers that translate Rust into logic and ask an SMT solver to prove properties. Each requires annotations in a specific syntax.
Here is a simple function and what a real deductive proof looks like in Creusot:
// Requires creusot-contracts crate
use creusot_contracts::*;
#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
&a[0]
}Creusot checks that the precondition a.len() > 0 guarantees the postcondition result == a[0]. This is trivial because the logic is simple. Now make it harder:
use creusot_contracts::*;
#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
let mut i = 0;
let mut s = 0;
#[invariant(i <= n)]
#[invariant(s == i * (i + 1) / 2)]
while i < n {
i += 1;
s += i;
}
s
}The invariants are the hard part. A human writes them by thinking about what stays true on every iteration. An LLM might guess s == i * (i - 1) / 2 because that pattern appears in training data, or it might omit the invariant entirely and let the solver fail.
What happens when you ask an LLM for a proof
I tested this with several models. The prompt was: “Write a verified Rust function that computes the factorial of n using Creusot, with complete preconditions, postconditions, and loop invariants.”
The responses fell into three categories.
First, some models produced plausible-looking annotations that used the wrong syntax. They wrote #[precondition(...)] instead of #[requires(...)], or mixed Prusti syntax with Creusot syntax. The code would not even parse.
Second, some models produced syntactically correct annotations with invariants that were too weak. The factorial function needs an invariant like res == fact(i). Models often wrote res >= i, which is true but useless for proving the postcondition. Creusot would report that it could not establish the goal, and the LLM had no mechanism to fix it.
Third, a few responses got the invariant right but hallucinated a helper lemma. They referenced a math::fact function that does not exist in Creusot’s standard library. The proof only works if you build that logical definition yourself.
None of the models produced a proof that checked on the first try.
Where LLMs actually help in the verification workflow
This does not mean LLMs are useless for formal verification. It means you have to use them for the right tasks.
They are good at generating the boilerplate. Given a function signature, an LLM can usually produce the #[requires] and #[ensures] clauses that capture the obvious contracts. For a function fn divide(a: i32, b: i32) -> i32, it will correctly suggest #[requires(b != 0)] and #[ensures(result * b == a)]. These are not deep insights, but they save keystrokes.
They are decent at explaining verifier errors. If Creusot reports “cannot prove loop invariant,” pasting the error into an LLM often yields a useful explanation of what the invariant is supposed to do. It will not suggest the exact invariant you need, but it will narrow the search space.
They are useful for translating between verification languages. If you have a Dafny proof and want to port it to Prusti, an LLM can handle much of the syntactic mapping. The underlying logic is the same. This is exactly the kind of pattern-matching task LLMs excel at.
The fundamental limitation: proof is search, not completion
Writing a proof is not like writing a web server. When you write a web server, there are many correct answers. When you write a proof, there is exactly one answer, or a small family of answers, and everything else is wrong.
LLMs are next-token predictors. They generate the most likely continuation given the context. A proof step is not the most likely continuation. It is the step that closes the proof obligation, which may be the twentieth most likely option or the two thousandth.
Consider proving that a sorting function returns a permutation of its input. The key insight is usually defining a multiset or counting occurrences. An LLM might suggest comparing lengths, which is necessary but not sufficient. It takes a human to recognize that length equality does not imply permutation, and to introduce the counting invariant.
Model checking with Kani avoids some of this because it does not require invariants. LLMs can generate kani::proof harnesses more reliably because they look like unit tests. But Kani only works for bounded verification. If you need an unbounded proof, you still need the human.
A practical workflow that uses both
If you want to verify Rust today, here is a workflow that actually works.
Start by writing the code normally. Run cargo test. Then add contracts. Use an LLM to generate the #[requires] and #[ensures] clauses from the function signature. Review them carefully. The model will get the easy ones right and the hard ones subtly wrong.
Run the verifier. It will fail on at least one loop. Take the error message and ask the LLM to explain what invariant is missing. Use its explanation as a starting point, not an answer. Write the invariant yourself.
Iterate. The verifier will tell you whether your invariant is strong enough. The LLM will not. Treat the model as a pair programmer who knows the syntax but has never finished a proof.
The honest answer to the question
Can LLMs write formal proofs for Rust? No. Not yet. Not without a human who understands the logic.
They can write the scaffolding, explain errors, and translate between tools. But finding the invariant, the lemma, or the induction hypothesis that makes the proof go through is still a human skill.
If you are looking for a tool that lets you skip learning separation logic or Hoare triples, an LLM is not it. If you are looking for a tool that makes the learning curve less steep by handling the syntax and boilerplate while you focus on the logic, an LLM is worth trying.
Start with Kani if you want bounded checks without invariants. Move to Creusot or Prusti when you need unbounded proofs. Use the LLM to get the syntax right, but expect to write the proof yourself.
Frequently Asked Questions
What is formal verification in Rust?
Formal verification uses mathematical logic to prove that a program satisfies a specification for all possible inputs. In Rust, tools like Kani, Prusti, and Creusot add annotations to functions that describe preconditions, postconditions, and invariants. A verifier then checks whether these properties hold.
Can ChatGPT write proofs for Kani?
ChatGPT can write Kani proof harnesses, which look like unit tests with #[kani::proof] attributes. These harnesses are easier to generate than deductive proofs because they do not require loop invariants. However, complex harnesses with assumptions and assertions still need human review.
What is the difference between Kani and Creusot?
Kani is a bounded model checker. It explores all possible execution paths up to a bound and checks for panics or assertion failures. Creusot is a deductive verifier. It translates Rust into logical formulas and uses an SMT solver to prove properties for all inputs, including unbounded loops, but requires user-supplied invariants.
Why do LLMs struggle with loop invariants?
Loop invariants require reasoning about what stays true across iterations, which is a form of inductive reasoning. LLMs are trained to predict likely text continuations, not to search for the exact logical statement that closes a proof obligation. The correct invariant is often not the most probable next token.