Courses

Level 4

AI-Assisted Verification

Use an AI assistant without trusting it blindly. You own the requirements and the specification. The assistant writes code and proof annotations. The verifier checks one against the other, and you audit what it cannot.

This course is for engineers who work with an AI assistant. The assistant is fast and sounds sure of itself. The verifier is the only thing in the loop that checks. You decide what is required and what the specification says, the assistant proposes code and proof annotations, and Dafny or TLC says whether the one satisfies the other. A green result still says nothing about whether the specification is right.

How the assistant works here

Each exercise has an Assistant tab with what it was asked and what it replied. In some exercises you press Generate and a scripted assistant implements your specification. In the later ones you can also try a live model. Whatever an assistant writes, the grade comes from the verifier and the hidden checks, and never from a model.

What you will practice

• Read the verifier, not the summary — what did the patch change, and what does a green result cover?
• The specification is the prompt — an assistant does what the specification allows.
• Audit what it wrote — a specification fitted to the code, and a proof fitted to the contract.
• Close the loop — specify, generate, look for what it got away with, and tighten.

Units are numbered 1–5, followed by the capstone. The first unit is open without Level 3. Level 3 explains why a passing proof is not enough, and it is worth taking first.

0 of 5 units done · 0 of 27 exercises verified · capstone not finished

1. 01Read the verifier, not the assistant

   An assistant hands you a patch and says it works. Run the verifier, read the diff, and ask what the green result was asked.

   • "All proofs pass"Run the verifier on an assistant's patch before believing its summary, and fix the code it left wrong.locked
   • The check that went missingNotice that a green result can come from a contract that lost its teeth, and restore what the requirements say.locked
   • A precondition nobody asked forRecognize an assistant that makes a failure disappear by refusing the input that exposes it.locked
   • The specification was rewrittenCheck the specification itself when an assistant touched it, and repair both the specification and the code.locked
   • A proof with a check switched offSee that a verifier can be told to stop checking, and that a green result then proves less than it appears to.locked
   • The model got smallerNotice that a model checker only looked at the model it was given, and restore the configuration the requirement is about.locked

2. 02The specification is the prompt

   An assistant implements exactly what your specification allows. Read what it builds from a loose specification, and tighten the specification until the best answer is the one you meant.

   • Whatever fitsRead what an assistant builds from a loose specification, and tighten the specification until its best answer is the one you meant.locked
   • Remove the repeatsSee an assistant satisfy a specification by returning almost nothing, and require that no value is lost.locked
   • Where is it?Specify a search so that "not found" is only a legal answer when the value is not there.locked
   • A rate limiter that remembers too muchSpecify a stateful rule, including the part that resets it, and see which easy implementations a partial specification admits.locked

3. 03Audit a specification the assistant wrote

   Assistants write the specification and the code together, and the two can agree for the wrong reason. Check that the specification says the requirement.

   • The spec that copied the codeNotice a specification that was written by reading the code, and rewrite it from the requirement.locked
   • A spec that asks the helperSee that a specification written in terms of the assistant's own helper is only as right as the helper.locked
   • If, but not only ifRead an implication in the right direction and write the other half of a rule.locked
   • A policy no password can meetCheck that a specification can be satisfied at all, and that its quantifiers and bounds mean what the requirement says.locked

4. 04Audit a proof the assistant wrote

   Assistants are good at making Dafny go green. Read the lemmas, the invariants and the ghost state they added, and check that the proof is of the requirement.

   • A lemma that is simply assumedSpot a proof that rests on an assumption instead of a proof, and replace it by making the code right.locked
   • A proof of something smallerNotice that the invariants and the postcondition were chosen to match each other, and restore the claim the requirement makes.locked
   • A model that was never tied downSee that a proof about ghost state says nothing about the real state until the two are connected.locked
   • Three claims, one fileCheck each claim in an assistant's summary against the proof, and fix the proof so that it supports the requirement.locked

5. 05The verification loop

   Write the specification, let an assistant implement it, look for what it got away with, and tighten the specification. Four rounds on a password reset, with a scripted assistant and a live model.

   • Round 1: a link works onceWrite a specification, read what an assistant builds from it, and close the gap it exposes.locked
   • Round 2: fifteen minutesSpecify a time limit with an explicit boundary, and use generated code to find the boundary you left open.locked
   • Round 3: whose passwordNotice that a specification must name the result you care about, not only the yes or no.locked
   • Round 4: only the newest linkAdd a rule that refers to state outside the token, and check the generated code against it.locked

6. CapCapstone: an event ticketing system

   Everything in one system. Review a patch, specify an operation and see what an assistant builds, audit a specification and a proof the assistant wrote, and review a whole class. You get the requirements and nothing else.

   • Review the Book patchReview an assistant's patch to a booking method, find what its summary leaves out, and repair it.locked
   • Specify Cancel firstWrite a specification from the requirements alone, then use generated code to find where it is loose.locked
   • Audit the Move specificationRewrite a specification that an assistant wrote for a seat-moving operation so that it is complete, and repair the code that was written to fit it.locked
   • Audit the seat counter's proofFind the proof that was fitted to the code and replace it with a proof of the requirement.locked
   • Review the whole Event classReview a complete assistant-written class: its invariant, its contracts and its code, against a list of requirements.locked