FVLearn Formal Verification

Courses

Level 5

Verification of Real Systems

Verify realistic software with the training wheels off. Each project hands you a system and its requirements, then someone else's verified code, and finally a system and a brief: you decide what it must do.

This course is for engineers who want to use verification on software like their own. Each project is a realistic system, such as a login service, a bank ledger, or a distributed lock. The requirements come from the people who run it, and some of the code comes from someone else. You decide what the system must do, write that down, and Dafny or TLC checks it.

How a project works

Each project has three stages, and each stage gives you less to start from.

  1. Verify it — you get the system and a list of its requirements. Make the specification say them, and fix the code where the verifier shows it falls short.
  2. Audit it — someone else wrote the next part, and it verifies. Check it against the requirements, not against its own contract.
  3. Specify it — there is no list of requirements, only a brief: a product memo, an incident report, or support tickets. You work out what the system must do. In the Dafny projects, an assistant then implements your specification, and you see what it lets through.

Every project is open from the start, and its stages open in order. In the first three projects, the Verify it stage names each hidden check. Every other stage reports only how many passed.

The projects

  • Projects 1–3, one service — authentication, a bank ledger, and a rate limiter, in Dafny.
  • Projects 4–7, several parties — payments, access control, a token contract, and an automated market maker, in Dafny.
  • Projects 8–9, several machines — a distributed lock and consensus, in TLA+ with TLC.

You can take them in any order. In order, 1 to 9, the systems grow from one service to a cluster. Level 4 shows how to work with the assistant used here, and it is worth taking first.

Where this leads

Level 5 is the last level of this path. These are the specializations we plan to offer after it. None of them is open yet.

  • Proof engineering — larger Dafny proofs, and keeping them fast and stable.
  • Lean — proofs that no solver finishes on its own.
  • TLA+ for distributed systems — protocols, refinement, and bigger models.
  • Verus — verified Rust.
  • Security — what an attacker must never be able to do.
  • Cryptography — protocols and their implementations.

0 of 9 projects done · 0 of 27 stages verified

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. 01Authentication

    Sign-in, sign-out, and changing a password. A lockout policy to verify, an assistant's session code to audit, and an incident report to turn into a specification.

    • Lock the account after five failuresTurn a login policy into a specification, and find the two places where the code does not follow it.locked
    • Review the sign-out patchAudit an assistant's session code against what sign-out has to mean, and repair the contracts and the code that fall short.locked
    • Specify the password changeRead an incident report, decide what changing a password must require and what it must do, and write that as a specification.locked

  2. 02Bank ledger

    Money moves between accounts and the total never changes. A transfer to verify, a refund an assistant proved half of, and a week of support tickets about closing accounts.

    • Verify the transferWrite a bank's transfer rules as a specification, including the total of all balances, and repair the code it exposes.locked
    • Review the reversal patchAudit an assistant's refund operation, see that a proof about the total says nothing about who gets the money or how often, and repair it.locked
    • Specify closing an accountTurn a week of support tickets into the rules for closing an account, and use generated code to find the rules you left out.locked

  3. 03Rate limiter

    How many requests, per whom, and per what clock. A token bucket to verify, an assistant's per-user limiter to audit, and a pricing page and support queue to turn into rules.

    • Verify the token bucketSpecify a token-bucket rate limiter, including what happens when the clock goes backwards, and repair the refill.locked
    • Review the per-user limiterAudit an assistant's per-user rate limiter, notice a contract that only talks about one user, and repair what it let through.locked
    • Specify the plan limitsWork out a rate limiter's rules from a pricing page and a support queue, including retries, and check them against generated code.locked

  4. 04Payment processor

    A card payment's life: authorized, captured, voided, refunded, and told about by webhooks. Capture and void to verify, an assistant's refunds to audit, and a webhook handler to specify from incidents.

    • Verify capture and voidSpecify the two operations that end a card authorization, and find the orders of events the code gets wrong.locked
    • Review the refund patchAudit an assistant's refund with idempotency keys, and find what a retry does that the contract never mentions.locked
    • Specify the capture webhookWork out from an integration guide and two incidents how a handler must treat events that arrive twice or out of order.locked

  5. 05Access-control service

    Who may do what, and who may change that. Role changes to verify, an assistant's invite and remove to audit, and a document's share dialog to specify from a help-center page and support tickets.

    • Verify role changesSpecify who may change a member's role in a workspace, and find the people the code lets do it anyway.locked
    • Review the membership patchAudit an assistant's operations for inviting and removing members, and find the ways they let a workspace lose control of itself.locked
    • Specify document sharingTurn a help-center page and three support tickets into the rule for sharing a document, and test it against generated code.locked

  6. 06Token contract

    A token where every balance is money and the code is public. A transfer to verify, an assistant's allowances to audit, and minting to specify from an issuance policy and a post-mortem.

    • Verify the token transferSpecify a token's transfer as the token standard does, and find the transfer that creates tokens out of nothing.locked
    • Review the allowance patchAudit an assistant's delegated transfer, and find out whose permission it checks and how often it can be used.locked
    • Specify mintingWork out from a token's issuance policy and an incident post-mortem what minting must do, and test it against generated code.locked

  7. 07Automated market maker

    A pool that trades two tokens at a price its reserves set. A swap to verify, an assistant's withdrawal to audit, and fees and deadlines to specify from launch documents.

    • Verify the swapSpecify a constant-product swap, including the trader's minimum and the direction of rounding, and repair the code it exposes.locked
    • Review the withdrawal patchAudit an assistant's withdrawal for liquidity providers, and find whose money it pays out and which way it rounds.locked
    • Specify the swap with feesWork out from the launch documents what a swap with a fee and a deadline must do, and test the rule against generated code.locked

  8. 08Distributed lock

    Several clients, one resource, and clients that pause or crash at the worst moment. Leases to verify, an assistant's fencing tokens to audit, and two incidents to turn into a safety property and a liveness property.

    • Verify the lease lockState mutual exclusion for a lock built on leases, and find the moment at which the design lets two clients in.locked
    • Review the fencing patchAudit an assistant's fencing tokens, and find the pause after which a stale client's write still gets through.locked
    • Specify the lock serviceWork out from two incident reports what the lock service must guarantee, including what it must eventually do, and make the design keep it.locked

  9. 09Consensus

    A cluster that must agree on one leader and one value, even when nodes give up, crash, and come back. A majority vote to verify, an assistant's election terms to audit, and two incidents to turn into the guarantees of a replicated config store.

    • Verify the leader electionState what a leader election must guarantee, and find the cluster size at which the vote count lets two candidates win.locked
    • Review the election termsAudit an assistant's election terms, and find which votes a candidate counts when it claims a term.locked
    • Specify the config storeWork out from two incident reports what a replicated config store must guarantee, and make a new leader respect what the cluster already accepted.locked