It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy t

It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes. There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.