You might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.i...

		hwayne on May 4, 2019 \| parent \| context \| favorite \| on: TLA+: design, model, document, and verify concurre... You might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.inria.fr/tlaps/content/Home.html There's also this essay on proving TLA+ specifications in Isabelle: https://davecturner.github.io/2018/02/12/tla-in-isabelle.htm...