&gt; You implement a formal spec for a requirement and&#x2F;or high-level function that takes plaintext as input and outputs ciphertext.<p>this misses the relationship between the size of the plaintext and the ciphertext...<p>edit: part of the problem is tooling, to deal with stuff like this you need dependent types and those do exist, but not in a way that &quot;the programmer on the street&quot; can use...