6.888: Certified Systems Software

General information

6.888 is a graduate seminar on research in certified systems software. The goal of the class is to get the students to build provably correct software. The structure of the class will consist of students presenting research papers during lecture, and students working on a significant research project. We expect students to start working on the project in the first week or two, and continue for the entire semester, culminating in a draft research paper. Examples of project include building a certified file system, distributed key-value store, in-kernel interpreter, simple OS kernel, etc.

We expect projects will build on tools such as Coq, Dafny, and Bedrock. To get students up to speed with these tools, we will offer a week-long intensive IAP class on Coq (January 26-30, 2015), using parts of the Software Foundations textbook. (The IAP class is not offered for credit, and does not have a subject number.)

If you would like to take this class, please send email to the instructors (6888-staff@csail.mit.edu) and describe: (1) your background, (2) the projects you are thinking of working on, and (3) whether you plan to take the IAP class.


This class will meet TR2:30-4 in 35-310.

Reading list ideas

Final projects


To contact the course staff, send email to 6888-staff@csail.mit.edu.