The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough.
What formal correctness proof will detect that?