[docandrew]

Feels like maybe this is retreading ground covered by Why3ML, but perhaps I’m missing something.

https://www.why3.org/doc/whyml.html

[lgas]

Presumably this is aimed at people that want to take advantage of it in Lean.