Here is the whole idea in one example. We want a withdrawal that never leaves a negative balance. The claim sounds right, but one allowed input breaks it. Verification is the habit of finding that gap before the code ships.
The claim
remaining >= 0
A withdrawal must never leave a negative balance.
The missing assumption
balance = 10, amount = 11
The result would be -1. As written, the claim cannot hold for every allowed input.
The core idea
A precise question, not a bigger test suite
A specification is a precise statement of what a program or system is allowed to do. For a function, that means what it can be given and what it must return. For a larger system, it means where it starts, what steps it can take, and what must never happen.
A verification tool then turns the code or model and that statement into mathematical formulas and tries to prove them, usually with an automated solver or a proof checker. If the proof fails, the cause is one of three things: a real bug, an assumption you forgot to write down, or a proof that needs more detail. If it passes, that is relative to what you wrote, not to every requirement you meant to write.
Dafny's official guide describes this as proving that code matches user-supplied annotations. The Dafny team also warns that a specification can verify while missing the intended behavior.
Specification
What must be true?
Implementation or model
What behaviors are possible?
Verification
Does the claim hold, given the assumptions you wrote?
Words you will see
Six terms, in plain language
The rest of this page and the exercises use these. You do not need to memorize them. Come back here if one slips.
- Specification
- The full, precise statement of what the code or system must do.
- Preconditionrequires
- What must be true before the code runs. The caller is responsible for it.
- Postconditionensures
- What the code promises when it finishes.
- Counterexample
- One concrete input that breaks the claim. You debug it like a failing test.
- Invariantinvariant
- Something that stays true while other things change, such as on every pass through a loop.
- Model
- A small, simplified description of a system that a tool can check completely. TLA+ works with models.
A small Dafny example
One method, one missing condition
Suppose a method subtracts an amount from an account balance. The requires line says what callers must give it. The ensures line promises that the remaining balance is not negative. The line in the braces is the code.
method Withdraw(balance: int, amount: int) returns (remaining: int)
requires 0 <= balance && 0 <= amount // callers must give us this
ensures remaining >= 0 // we promise this back
{
remaining := balance - amount; // the code
}The contract allows balance = 10 and amount = 11. Subtraction gives remaining = -1, which breaks the promise.
This input is a logical illustration, not copied verifier output.
Decide what the method means
There are two honest fixes. If overdrafts are not allowed, add a rule about the input. If overdrafts should be handled, change the code and say what it does. Weakening the promise until the check passes is not a fix. It gives up the original requirement.
One possible repair
requires 0 <= amount <= balance
Now every caller has to show the amount is no more than the balance. That rules out the bad input. It does not make the method handle overdrafts. It only refuses to be called that way.
Dafny documents preconditions and postconditions as part of a method's contract. The caller must establish the precondition, and the method must establish the postcondition.
The practical difference
Formal verification vs. testing
Both help find mistakes. They differ in what you can say after a successful run.
A test suite for Withdraw might try (10, 5), (10, 10), and (0, 0), and pass every time. It only catches the bad case if someone thinks to try (10, 11). The verifier does not need anyone to think of it, because the contract already allows it.
| Question | Tests | Verification |
|---|---|---|
| What it covers | The specific inputs you chose to try. | Every case the claim allows: every input for a Dafny method, every reachable state of a TLC model (a small, finite version of the system). |
| A pass means | Those runs gave the results you expected. | The claim you wrote holds, under the assumptions you wrote. |
| Where it can still miss | A case you did not try may behave differently. | A requirement you forgot to write down, or a model that differs from the real system. |
Verification does not replace running software in its real environment. Tests are still valuable for integrations, deployment behavior, and assumptions your specification has not captured.
Two starting points
Check a method or check a design
Dafny: one method and its contract
Write a method alongside claims such as requires, ensures, and loop invariants. Dafny checks whether the code keeps those claims for every input the contract allows. When it cannot prove a claim, look at the missing assumption, the code, or the structure of the proof.
Source: Dafny's official guide.
TLA+ and TLC: how a system behaves over time
Describe where a system can start and which steps it can take, then check a property such as “a bad state is never reached.” TLC explores a model you configure and can return an error trace when it finds a violation. Checking a finite model is not, by itself, a proof about every implementation or an unbounded system.
Source: Leslie Lamport's TLA+ overview.
Read the result carefully
What a passing check does not say
A pass does not certify every behavior you wanted. If the promise says only that the result is not negative, a method that always returns zero can pass, even though callers expected the correct amount. A weak contract is how an unfamiliar or generated implementation gets accepted. State the actual relationship you need, not just a convenient property.
A TLA+ model also leaves out implementation details. TLC checks the behavior of that model. You still need to ask whether the model includes the relevant actions, assumptions, and failure modes of the deployed system.
The Dafny team's discussion of specification problems shows how a successful verification can give false confidence when the contract does not express the intended requirement.
Put it into practice
Start with one property you can state
This matters most for code you did not write. Generated code often looks right and passes a few examples. The claim is what you review it against.
01
Pick something small
One method, or one step of a design.
02
Say what must always be true
Write the assumptions as carefully as the result.
03
Try to break it
Look for an input that would defeat an incomplete claim.
04
Decide what to change
The code, the assumptions, or the claim.
If a loop is involved, move on to the interactive loop invariants guide. It shows how a fact about each pass through a loop helps establish the final result. For a longer sequence of exercises, use the Dafny course.
Frequently asked
Formal verification, plainly answered
Is formal verification the same as testing?
No. Unlike a test, which runs the code on cases you picked and checks the results, formal verification turns the code and a precise claim into mathematical formulas and proves the claim for every case the specification allows. Both are useful. Verification can miss what the specification forgot to say. Tests can expose integration and real-world behavior that a model leaves out.
Does verification prove software has no bugs?
No. A pass shows that the properties you wrote hold, under the assumptions you wrote, in the tool’s model. It does not show that your requirements are complete, that the deployed system matches the model, or that every behavior was specified.
What is a counterexample?
One concrete input, or one sequence of steps, that breaks your claim. In the withdrawal example, balance = 10 and amount = 11 gives -1. You debug it the way you would debug a failing test.
What is an invariant?
A statement that stays true while other things change. A loop invariant is true before the first pass and after every pass. A system invariant is true in every state the model can reach. The loop invariants guide covers the first kind.
Do I need to be good at math?
Not to get started. The ideas are the ones you already use when you review code: what must be true on the way in, and what must be true on the way out. The exercises explain the few symbols they use as they come up.
Which check do I need?
Start with the question you need to answer. Use Dafny to check that a method meets its contract. Use TLA+ and TLC to explore the possible behaviors of a system model, especially when order and concurrency matter. They answer questions at different levels of a system.