FVLearn Formal Verification

Courses

Level 3

Specification Engineering

A green check says the code meets the specification, not that the specification says what you needed. Find what is missing, strengthen it, and stop it from asking for too much.

This course is for engineers who check code they may not have written, including generated code. A green check says the code meets its specification. It does not say the specification asks for the right thing. Here every proof passes, and your job is to find what the specification fails to say.

What “break the specification” means

You will find a concrete wrong behavior that the specification accepts: a transfer where the sender keeps the money, a withdrawal by someone who does not own the account, a system that never does anything. Then you write the missing requirement, and check that you did not rule out a behavior that is correct. Hidden tests run against your specification and report what it still allows.

What you will practice

Four questions to ask of any specification, whoever wrote it.

  • Who may call this? — who is allowed, and who sees the result?
  • What happens on failure? — what does a refused request leave behind, and when is a refusal the right answer?
  • What must not change? — which accounts, fields, and records does this leave alone?
  • What is conserved? — which totals and uniqueness rules hold before and after every step?

The early units tell you what kind of gap to look for and name each hidden test. Later units only list the requirements, and the capstone shows how many hidden tests pass, not what they are. Units are numbered 1–7, followed by the capstone. You do not need to finish Level 2 first, but Level 2 explains the Dafny used here.

0 of 7 units done · 0 of 33 exercises verified · capstone not finished

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.

  1. 01Verified is not correct

    Dafny proves the code meets its specification. It does not check that the specification says what you needed. Find the wrong answers a specification lets through.

    • Money from nowhereSee a transfer verify while the sender keeps the money, then write the missing half of the specification.locked
    • Any upper boundBreak a specification by writing an input and a result that it accepts although the requirement rejects them.locked
    • The largest elementRepair the specification you just broke, and the code that only satisfied the weak version.locked
    • Sorted is not enoughAdd the property that makes "sorted" mean "the same numbers, in order", without ruling out equal numbers.locked

  2. 02Edge cases

    Most wrong behavior sits at the edges: negative amounts, the same account twice, the exact limit, duplicates. Test a specification there.

    • A negative amountNotice that a precondition lets in inputs the requirement never meant, and tighten it without locking out legal ones.locked
    • Paying yourselfTest a specification on the case where two inputs are the same, and fix the code the stricter specification rejects.locked
    • Exactly one hundred dollarsCover the boundary value that a pair of strict inequalities skips.locked
    • Two of the same itemSay which item is removed, and that exactly one copy goes, in a cart that can hold duplicates.locked

  3. 03When an operation fails

    A specification for success is half a specification. What does failure leave behind, and when is failure the right answer?

    • A failed withdrawal that still takes moneySpecify what a failed operation leaves behind, not only what a successful one does.locked
    • A bank that never paysShow that a specification can be satisfied by an implementation that refuses every request.locked
    • Succeeds exactly when it canTie success to the condition that justifies it, so that refusing everything no longer satisfies the specification.locked
    • Two payments, all or nothingSpecify an operation that has several steps so that a failure part-way leaves no partial effect.locked
    • A retry that charges twiceSpecify an operation that may be called twice with the same request, and fix code that charges both times.locked

  4. 04Who is allowed

    Correct arithmetic is not enough. Who may call this? Who may see this result? Specify who is allowed, and what a refused request leaves behind.

    • Whose money?Break a specification by finding an actor it lets do something the requirements reserve for someone else.locked
    • The account ownerWrite the requirement that only the owner can withdraw, without making the owner's own withdrawals fail.locked
    • Granting accessSpecify who may change a permission, and what a refused change leaves behind.locked
    • Who gets to lookSpecify who may learn a value, not only what value they get.locked

  5. 05What must always hold

    Some rules belong to the whole system: totals, uniqueness, who else is left alone. A specification for one operation has to carry them through.

    • Minting tokensState a rule that must hold of the whole system after every operation, and carry it through a method.locked
    • Everyone elseSay what an operation leaves alone, not only what it changes.locked
    • Renaming a userKeep a uniqueness rule true through an operation that can break it, and decide what the operation does when it would.locked

  6. 06Requirements over time

    Some requirements are about order: once, before, after, eventually. Write them as properties of a system, and see which designs the property catches.

    • A gift card, redeemed twiceWrite the property a design must keep, and find that the model checker catches the design that breaks it.locked
    • Redeemed after it expiredWrite a time-based requirement as a property of every state, with its boundary in the right place.locked
    • Pay, ship, refundWrite the requirements on the order of events as one property, then repair the design that allows each wrong order.locked
    • A system that does nothingSee that a system that never acts satisfies every safety property, and state a property of progress.locked

  7. 07Too strong, contradictory, ambiguous

    A specification can also ask for too much: more than the requirement, an impossible combination, or one answer where many are correct. Loosen it without letting a wrong answer in.

    • Two rules that cannot both holdNotice that a specification can be impossible to meet, and decide which requirement gives way.locked
    • Find a positionWeaken a specification that demands one answer to one that allows every correct answer, and no wrong one.locked
    • A precondition that asks too muchCheck a precondition for the legal calls it refuses, not only for the illegal ones it allows.locked
    • Splitting a bill three waysReplace a requirement that cannot always be met with the closest one that can, without losing the part that matters.locked

  8. CapCapstone: audit a generated wallet

    An assistant wrote a wallet and every proof passes. The only thing you get is the list of requirements. Find what the specifications do not say, and fix both specifications and code.

    • Part 1: DepositReview a generated deposit whose specification is green and incomplete, with no hint about what is missing.locked
    • Part 2: WithdrawReview a generated withdrawal for what it is allowed to do, and for what it is allowed not to do.locked
    • Part 3: TransferReview a generated transfer between two accounts for the ways two accounts can be the wrong two accounts.locked
    • Part 4: FreezeReview a generated freeze for who may do it, and for everything else it must leave alone.locked
    • Part 5: Full auditReview the wallet as a whole, where one entry point serves every operation and the rest of the wallet has to be left alone.locked