Course Notes

This table of contents gives the suggested order for the course notes. Work through the sections in order and read each section from top to bottom. Pages marked stub reserve space for planned material; they are not completed lessons. The sequence may evolve as we develop the course project.

Getting Oriented

  1. Verified Programming, Lean, and Proof Agents

  2. Getting Started with Lean

  3. Getting Started with Coding Agents

  4. PL/OS: From a Lean Prototype to Verified RISC Code

Foundations and Workflow

  1. Reading a Lean Project — stub

  2. Programming and Proving in Lean — stub

  3. What Makes a Good Specification?

  4. Operational Semantics

  5. Invariants and Induction

  6. Auditing a Proof — stub

Developing the Queue Warm-Up

  1. Warm-Up: A Verified Queue from Semantics to RISC

  2. An Executable Specification

  3. Representation Invariants

  4. Refinement and Simulation

  5. Testing Alongside Proofs — stub

  6. Finite Arithmetic — stub

  7. Machine Execution in Lean — stub

  8. Verifying a Machine Routine — stub

  9. Preserving Unrelated State — stub

  10. Composing Correctness Proofs — stub

Building Toward PL/OS

  1. Processes and Protection Domains — stub

  2. Synchronous Message Passing — stub

  3. Choice and Cancellation — stub

  4. Scheduling — stub

  5. Channels as Capabilities — stub

  6. Memory Allocation — stub

  7. Context Switching and Traps — stub

  8. Isolation — stub

  9. Replacing a Verified Component — stub

Cross-Cutting Questions

Revisit these throughout the earlier sections: safety and failures when specifying the queue, nondeterminism when studying semantics and scheduling, and the trust boundary and proof maintenance as implementations develop. The order below is a final review path.

  1. Safety, Progress, and Termination — stub

  2. Nondeterminism — stub

  3. Failures as Specified Behavior — stub

  4. From a Machine Model to Hardware — stub

  5. Maintaining Proofs as Code Changes — stub

Course Updates

  1. Welcome to CMSC 818C

Categories