As someone who works exclusively in typed languages for formal methods, what is it you find lacking about modern Python + PyLance? IMO there's still a tiny verbosity issue, and there's no real replacement for fancier polymorphism or (G)ADTs, but I'm very satisfied with it for most things. In particular, null checks are trivial.
However, in principle any dynamically typed language can be tolerable to me if it can be turned into a statically typed language ;)
But I think I'd still prefer the ergonomics of a language designed that way from the start vs having bolt-ons. My favorite language for the past several years has been F# and I think ML-family languages in general strike a great balance of being able to write terse code when you want to, and being able to model a domain really well with types when you want to.