Thank you all very much for your inputs! To summarise: I asked about
the possibility of adding ACSL annotations to the codebase and the
responses ranged from nonplussed on one end of the spectrum to some
degree of enthusiasm on the other. It was suggested that libpsql would
be a better initial target than the internals. I appreciated the good,
brisk discussion and if anyone else has any other ideas please let us
all know.
Regards,
Colin