Systems verification beyond this class

Here are a few pointers to verification research.

Distributed systems

IronFleet is a good starting point to learn about verifying distributed systems.

Grove extends Perennial with distributed systems reasoning. Add support for reasoning about multiple machines, a network, and reasoning about failures of individual machines.

There's lots of work on reasoning about protocols independently of implementing those protocols. The Ivy paper is a useful starting point. Most of the followup work has been about automating finding inductive invariants to prove safety of a protocol.

New specifications

Iris is well suited to extensions to handle new language features and specifications. For example:

• Verifying randomized algorithms where the probability of an outcome is part of the specification.
• Verifying storage systems that want to reason about crashes at any time (for example due to power failure).
• One part of verifying a system is secure is proving confidentiality. Formalizing confidentiality often involves some form of non-interference specification.
• Weak memory, a fundamental feature of concurrent programs on real hardware.
• Persistent memory is like memory but persists across reboots. These proofs need to combine techniques for crashes with techniques for weak memory.

Note that in each of these areas there is other work not using Iris that tackles the same underlying problem.

Practical verification

The techniques in class require learning quite a bit before you can apply them to real code. One line of research is making verification easier to apply, including scaling up to real code, usable by engineers, and integrated with usual software development.

AWS used verification as a core part of their process for the Cedar policy language.

AWS also uses verification for their distributed protocols. In addition to TLA+ as described by that article, they also use P.

Verus is a new language for verification using Rust.