While I do think TLA+ is relatively easy to pick up (especially compared to Isabelle or Coq), and I think it's pretty awesome, I'm hesitant to say it's as "easy to pick up as Python". You need a basic understanding of set theory and state machines to even get started, and more advanced concepts like algorithm refinement to get into the really useful juicy stuff.
When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter for most of my engineering colleagues. I don't think my coworkers are stupid by any stretch, but they are decidedly uninterested in re-learning any discrete math (if they ever learned it in the first place, which isn't a guarantee). For an engineer LARPing as an academic like me, TLA+'s notation isn't really hard at all, but I will often forget that most engineers only think in code.
Would they be interested in Quint?[0] If I understand correctly, Quint is very similar to TLA+, but with a more "code-looking" notation. And it has some nice dev tooling, like an LSP, which also lowers the barrier to entry.
It’s still an uphill battle, because the comparison to unit tests always comes up, and I have to explain how they’re not equivalent.