Research projects should be in one of the following forms:

• Specify and implement a system using verification tools such as Z3, Rosette, Dafny, and Coq, and formally verify that the implementation meets the specification.
• Build a tool that systematically uncovers correctness issues of existing software or system configurations.
• Conduct an empirical study of formally verified systems and analyze their assumptions and specifications in end-to-end systems.

The project may be done individually or in a group of two to three. You’ll turn in your code and a paper describing the design and implementation, which we will post on the course website (unless you explicitly talk to us about why you want to keep it confidential). Use the OSDI’16 submission format for your paper.

• April 15: submit your project proposal, up to one page.

• May 13: checkpoint: please upload a PDF describing your progress on achieving the goals you included in your proposal. Clearly explain any changes you have made to the goal of your project based on your experience so far. Include examples that your prototype can already handle. Provide a clear, concrete plan of what you will need to accomplish in the remaining weeks to complete your project and what we can expect to see in the presentation.

• June 9/10: demo.

• June 10: project report due.

Here is a list of ideas to get you started thinking. Feel free to pursue your own ideas.

• Specify and do something useful with hardware primitives, such as Intel’s SGX, transactional memory, and virtualization.
• Build a verified storage system, such as a key-value store, a SQL database, and a file system.
• Bootstrap a verified compiler through self hosting.
• Implement and verify a cryptographic protocol, such as TLS and tcpcrypt.
• Implement and verify a distributed hash table.
• Implement and verify Bitcoin’s scripting system for transactions.
• Replicate FSCQ in Dafny. Report on what was easier and what was harder.
• Take a large collection of lemmas from a verified system, such as Ironclad or Verdi. Prove them using another tool.
• Build a message fragmentation layer for Ironclad/Verdi. Prove it correct. Bonus: Prove it live.
• Specify and verify the safety and liveness of some variant of Paxos. Relatively easy examples include: Mencius, Egalitarian Paxos, Disk Paxos, or Fast Paxos. Harder examples include BFT, or Stellar.
• Build and verify a high-performance B (or B+) tree implementation. Compare with unverified versions.
• Check out the challenge problems in assignments.
• Check out the ideas and projects from Penn’s CIS 670 and MIT’s 6.888.