see also https://lean-lang.org/use-cases/aeneas/ https://github.com/AeneasVerif/aeneas (by Microsoft)