Originally reported by @jaylorch on #2794.
I've since learned even more details about the issue I was having. It seems it was deeper than just mtime issues.
What was actually going on was that verus-mode in emacs was using flycheck. This was making it so that whenever I saved a file, it would run a partial verification on just the module in that file (cargo verus verify -- --verify-module <m>). That module-only run succeeded and poisoned Cargo’s freshness cache. The subsequent full cargo verus verify reused it and reported success. After cargo clean, full verification failed correctly.
So the issue is that a --verify-module run poisons Cargo's freshness cache, making it think that every module is OK when only the verified module is.
In other words, this PR fixes the mtime issue (which I'm not sure was ever the actual underlying cause of the issues I was facing). But be aware that the PR doesn't fix what the real issue turns out to be, which is partial verification polluting Cargo's freshness cache.
Originally reported by @jaylorch on #2794.