Ask HN: Is anyone using KeYmaera X for Cyber-Physical Systems?

I have been studying CPSs Cyber-Physical System as a natural progression from my embedded experience and MBSE (Model-Based Simulation Engineering)for fun and self-study and as it applies to my work. I purchased the book (PDF is free from Springer) Logical Foundations of Cyber-Physical Systems by André Platzer. It uses KeYmaera X described as "An aXiomatic Tactical Theorem Prover for Hybrid Systems". I have played with Coq and I was self-studying realtime systems and high-integrity applications using Ada and SPARK2014, and I find KeYmaera X to be inline with my other studies. There seems to be an approach of using algorithmic vs. dynamic logic verification systems (which is what KeYmaera X is). Can anyone share their experience with using any verfication system as it applies to CPSs or autonomous driving systems? Thanks!