Filesystems often have 100,000 lines and are not isolated components. Formal verification of the filesystem code would require formal verification of the rest of the kernel. At that point, the amount of code that requires formal verification is on the order of 10 million lines. It is infeasible with current techniques.
With that said, you said verification, not formal verification. The two are different. One can be done with rigorous testing. The other is currently a pipe dream.