Projects

These projects explore the core ideas of verified systems programming on small, self-contained examples before applying those ideas to PL/OS. Each project develops an executable model, precise contracts, and proofs, with agents assisting in implementation and proof construction.

1. A Small Allocator: allocation invariants, finite addresses, freshness, failure, and preservation of unrelated state.

2. A Bounded Queue: representation invariants, circular buffers, refinement, and composition over sequences of operations.

3. A Small RISC Machine: instruction semantics, finite arithmetic, execution traces, loop invariants, and termination.

4. A Small Verified Compiler: source semantics, code generation, branch layout, and compositional compiler correctness.

5. Protected Memory and Isolation: whole-access authorization, failure atomicity, byte frames, and isolation across command sequences.

6. A Cooperative Scheduler: context ownership, live and saved state, scheduling invariants, and simulation across context switches.

We then apply these ideas to components in PL/OS:

7. Verified RISC Lookup: assembly, encoded execution, table representations, calling conventions, and read-only refinement.

8. Persistent RISC Handle Tables: bounded append, exact byte effects, preservation of executable code, and persistent component invariants.

9. A Runnable RISC Queue: encoded dequeue, circular storage, reuse of verified writes, persistent FIFO refinement, and the kernel queue contract.