on part de la proposition métier de Arnaud Bailly https://abailly.github.io/posts/dependently-typed-accounting.html

une version (dont l'objectif pedagogique est différent néanmoins) est ici https://github.com/music-action/how-to-test-the-hexagon-kotlin-2024