Ah, they're trying to specify file system recovery, which exposes the internals.

I did that once, as part of a very old secure operating system project, KSOS.[1] The specs were in SPECIAL, a forgotten language from SRI International.[2] The file system had two key invariants. The weak invariant was true at the end of every write. The strong invariant was true when the file system was clean and unmounted. The job of file recovery was to take a file system for which the weak invariant was true and make the strong invariant true.

We had a spec, but nobody could prove anything about it at the time. The tools didn't exist in the early 1980s. And trying to cram KSOS into a PDP-11 didn't really fit. It ran, but was too slow. All of this was just too early. Today you can do it.

[1] https://seclab.cs.ucdavis.edu/projects/history/papers/ford78...

[2] https://www.sciencedirect.com/science/article/abs/pii/016412...