For software engineers · Exercise-first
Say what your code must do. Then have a tool check it.
This is called formal verification. You write down exactly what a function or a design must always do. A verifier then turns your code and that claim into mathematical formulas and proves them, so the claim holds for every input it allows. A test only checks the inputs someone thought to try.
What it looks like
A claim is a few lines above the code
This function returns the absolute value of a number. The line that starts with ensures is the claim: whatever number goes in, the result is never negative. The verifier reads that line and the code, and checks that the code keeps the promise.
method Abs(x: int) returns (y: int)
ensures y >= 0 // the claim: the result is never negative
{
if x >= 0 {
y := x;
} else {
y := -x;
}
}Hit Verify and you get one of two answers. Either the code keeps the promise for every number, or the verifier shows a number that breaks it. The first exercise has you write this claim yourself.
01
Write the claim
Say in a few lines what the code must always do. For a function that returns a balance after a withdrawal, one claim is: the balance is never negative.
The exercise is the claim itself, not a lecture about it.
02
Run the checker
A program called a verifier reads your claim and the code. It either says the code meets the claim, or it shows one input that breaks it.
That input is called a counterexample. You debug it like a failing test.
03
Fix what it found
Fix the code if the code is wrong. Fix the claim only if the claim was wrong. Then run the checker again.
A green result covers the claims you wrote. It says nothing about the ones you forgot.
A real failure
The claim was right. The code was wrong.
In the exercise “Debug with a counterexample,” the ensures lines below are already correct: the new balance is never negative, and it equals the old balance minus the amount. The body subtracts one too many. Dafny 4.11 rejects the code and prints the inputs that break each claim.
method Withdraw(balance: int, amount: int) returns (newBalance: int)
requires amount >= 0
requires amount <= balance
ensures newBalance >= 0
ensures newBalance == balance - amount
{
newBalance := balance - amount - 1;
}Error: a postcondition could not be proved on this return path Related counterexample: WARNING: the following counterexample may be inconsistent or invalid. initial state: assume 0 == balance && 0 == amount; assume 0 == balance && 0 == amount && -1 == newBalance; Related location: this is the postcondition that could not be proved ensures newBalance >= 0 Error: a postcondition could not be proved on this return path initial state: assume 1 == balance && 0 == amount; assume 1 == balance && 0 == amount && 0 == newBalance; Related location: this is the postcondition that could not be proved ensures newBalance == balance - amount Dafny program verifier finished with 0 verified, 2 errors
First error
balance = 0, amount = 0
The code returns -1. That breaks newBalance >= 0, because a balance is never supposed to be negative.
Second error
balance = 1, amount = 0
The code returns 0, but taking out nothing should leave 1. That breaks newBalance == balance - amount.
Both inputs point at the same line: the code subtracts an extra 1. The fix is in that line, not in the claims. Weakening a claim until the bug passes would hide the problem. The exercise is graded in the browser with this same verifier, not by matching patterns in your source.
Three tools
Each tool checks a different kind of claim
Units 1–5
Dafny
Checks one function against a promise.
You write what must be true before the function runs and what must be true after. Dafny checks the function body against both. Failures come with a counterexample.
Meet DafnyUnits 6–9
TLA+
Checks a design where many steps happen over time.
You describe the states a system can be in and the steps that move it between them. A tool called TLC tries every state the model can reach. Failures come with a trace: the list of steps that led to the bad state.
Meet TLA+Unit 10
Lean
Finishes a step the other tools could not.
Sometimes a checker stops with one claim still unproved. Lean lets you write the missing steps yourself, and it only says yes if they hold. This is a short unit near the end, not the focus of the course.
Meet LeanKnow the limits
What a green check does not mean
A passing check means the code meets the claims you wrote. It does not mean the code is correct in every way you care about.
Dafny. Dafny’s guide describes verification as checking code against the annotations you supplied. A claim that only says the balance stays nonnegative can pass for a function that always returns zero. The claim has to say enough.
TLA+. TLC checks a model of your design, not the real system. Leslie Lamport’s overview separates the spec from the implementation. An error trace is a path through the model. It is not, by itself, a bug report from production.
Lean. A finished proof only establishes the theorem you stated. If Lean says a goal is unsolved, that step is not finished yet. It does not mean Lean found a broken example.
Counterexamples. Dafny also warns that an extracted counterexample may be inconsistent or invalid. Check the values against the claim that failed before you treat them as the only bug.
Learn Formal Verification Pro · One-time payment of $49
Go from understanding formal verification to specifying, verifying, and supervising real software.
Pro covers Levels 2 to 5 and every course, exercise, project, and challenge we release. The levels build on each other, so they are sold together and not one at a time. Level 1 is free.
See the pathway and pricingCommon questions
What is formal verification, in one sentence?
You write down exactly what a piece of code or a design must do, and a verifier turns the code and that claim into mathematical formulas and proves them. Unlike a test, which runs the code on a few inputs, a verifier proves the claim for every input it allows.
Do I need to know math or proofs?
No. You need to be able to read code. Each exercise explains the few terms it uses, and you learn keywords as you need them. The course is not training to become a proof specialist.
What do you practice?
You state what a function or a design must do, then check an implementation against that claim. If the check fails, you repair the code or the claim. That is how you review code you did not write, including generated code.
What is a counterexample?
One concrete input that breaks your claim. For example, balance = 0 and amount = 0 gives a result of -1, which breaks “the result is never negative.”
Which tool checks which claim?
Dafny checks that a function meets its contract. TLC checks a finite model of a system. Lean is for a leftover step a checker could not finish. A hint can explain a failure. Only the verifier decides that an exercise passed.
What does a passing check prove?
It shows the claims you wrote hold, under the assumptions you wrote, in the tool’s model. It does not show your claims are complete, or that the real system matches the model.