> Note that they claim performance similar to TensorFlow in CPU only. But a direct translation of this to Python TensorFlow code could run in GPU, and is probably easy to make. It wouldn't be proven, but it would be much more likely to be correct than the code you have constructed for your research just now.
They are wrapping unverified C++ code (Eigen) for the primitive kernels anyway, such as gemm, so AFAIK it could be extended to launch kernels on GPUs without any modification to the part in Lean that they proved correct.
Since most ML users are happy to trust TensorFlow, one could also wrap (unverified) TensorFlow and then use their approach to prove properties about real TensorFlow programs, e.g. that various model-transformations are sound.