Research Project: Guidelines and Deliverables

This page outlines the goals of the project part of the module, discusses their assessment and lists some high-level ideas. The projects are meant to be completed in teams of one or two.

This part of the course is open-ended: you are encouraged to explore your own ideas in the space of specification and verification of systems and algorithms.

The most important part for the project is to be interesting, related to specification and verification of a mathematical problem or an algorithm/system, and to be developed to a certain level of maturity. For instance, if you are specifying a textbook algorithm in Velvet, make sure that there are no similar versions of this algorithm formalised already in Lean, Rocq, Ivy, Dafny or any other popular proof assistant.

Grading

The research project amounts to 40% of your grade. This score is combined from:

• Written report: 10% (evaluated based on structure, clarity)

• Code quality: 5% (well-documented, corresponds to the text in the report)

• Presentation: 15% (you should be able to explain your design choices)

• Self- and peer evaluation: 10% (based on the peer feedback in case of teams of two)

At some point after the end of the lectures, we will arrange an online meeting for project presentations and Q&A.

On Incomplete Deliverables

If your project turned out to be a larger undertaking than you were planning, it is acceptable to have it not fully completed. That said, your final artefact should still present some amount of non-trivial effort, possibly packaged with instructions on how one could build on it; your report should clearly list the obstacles that prevented you from finishing your initially planned agenda.

Project Ideas

You are encouraged to come up with your own project proposals and discuss them with the instructor!

Alternatively, you can also find some project ideas below (I will try to add more of them later).

Specifying and Verifying Concurrent/Distributed Systems in Veil

The public archive of TLA+ examples is a good source of concurrent/distributed protocol formalisations that come within a proof of their safety properties. Feel free to adopt one of them (make sure it’s not featured already in the examples provided by the Veil repository!).

If you want to try out something more challenging, here are more ideas. At the time of this writing the following published distributed systems did not have a machine-checked formalisation, so you can formalise a simplified version of one of these protocols.

• Bullshark: DAG BFT Protocols Made Practical

• A Fast Confirmation Rule (aka Fast Synchronous Finality) for the Ethereum Consensus Protocol

• All You Need is DAG

• Autobahn: Seamless high speed BFT

• Narwhal and Tusk: A DAG-based Mempool and Efficient BFT Consensus

It’s okay to use LLMs for auto-formalisation of the protocols given in Rust/Go/Java/pseudocode.

Specifying and Verifying Imperative Algorithms in Velvet

A typical case study in Velvet would be an “interesting” verified data structure with a number of methods/functions along with their non-trivial specifications. The list of such data structures includes (but is not limited to):

• Link-Cut Trees

• Fenwick Tree

• Split-Join strategy for batch-parallelism

• Splay trees and Splaysort

• Zippers

A good source of data structures to specify and verify can be found in the literature on databases.

As an alternative to that, you may want to pick a “hard” problem from LeetCode, implement it in Velvet and verify its solution with regard to logical specification paraphrasing its description given in plain English.