What exactly is it that the model models? (What is the "essence" of a file system?)
What sorts of interleaving/concurrency does the model handle? What about two racing writes, can they interleave?
How is the equivalence partitioning and trace generation implemented?
Is it surprising that more bugs weren't found, particularly security bugs?
Why don't you test for concurrent/racy file system bugs?
How was the model constructed?