C has no memory safety and never will. Twelve weeks inside the retrofits engineers built to bolt some on anyway, and what each one gives up to get it.
What you will do
Twelve weeks, one retrofit a week: Cyclone, Checked C, separation logic, Frama-C, CompCert, MISRA-C and static analysis, and the academic borrow-checking prototypes chasing Rust's guarantee inside plain C. You'll annotate and verify real (small) C functions with at least three of these tools across the semester, run a real CVE through several of them side by side, and finish with a report that argues — on your own evidence, not on vibes — which tool you'd actually ship with.
Who it is for
You should already be comfortable reading and writing C, and unbothered by a little formal notation — you don't need prior exposure to Hoare logic or separation logic, but week 6 assumes you can follow a proof once it's explained, not that you've never seen a `∀`. If "C has no memory safety" is news to you, start with week 1's reading list before you enrol.