Teaching rigorous distributed systems with efficient model checking

What I like about the paper is that (a) the DSLabs framework and all assignments are available in open source, and it looks like it would be a lot of fun to play with, and (b) the challenges students have to face in building reliable, testable, distributed systems under time pressure look pretty much like the challenges many practitioners have to face to me! Hence the DSLabs framework integrates model checking into a holistic distributed systems development environment (based on Java as the implementation language – it would be neat to see a Rust version!) In the core programming model, students provide implementations of subclasses which specify the behaviour of individual nodes in their distributed systems.

Source: blog.acolyer.org