If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisions around representing concurrency, and there's an opportunity cost to that. I'd consider a code-level formal verification language, like Liquid Haskell or Dafny.