zlacker

I have been working on that direction with Lean Theorem Prover (https://leanprover.github.io). There is also works using Coq (https://link.springer.com/chapter/10.1007/978-3-642-35786-2_...)