After watching at the &Truth intro video (https://www.youtube.com/watch?v=OU29x5TZ0w0), it seems clear that they are attempting to "verify" so much SW that it is no longer possible for humans to even read the function-level separation logic specs for the entire C ecosystem, never mind write them. The only logical conclusion is then that they are producing slop specs and then proving these slop specs using slop proofs. I really have nothing against slop proofs (and think they are a natural consequence of proofs being finitary syntactic objects), but one of the sadder things about the proliferation of LLM coding/proving is that after a while, people stop caring about the specs, theorem statements, etc. as well.