> formal, verifiable modernization

Would it be possible to do the same to modernize a Kotlin program becoming legacy in the future to something even more modern?