Verified pre and post conditions would be nice. Especially in the era of LLM's, which can usually fill in the implementation given a sufficiently clear specification.