I have written complex proofs for distributed system using verus which are certainly not expressed by clippy