Yes, they can only logically deduce correctness based on our assumptions of a given system boundary. But I think it is typically a good idea to write them down formally if you need the guarantees. They are also typically smaller and more declarative.