Yes apart from it's not pseudocode but mathematical formulas.

Your building blueprints aren't made from bricks and mortar because it would just take way longer and be expensive to experiment with, however with software when designing we often use the same tools as building without thinking of the cost like that.

TLA+ and other lightweight modelling languages allow you to experiment with your design and verify that it works without all the tedium of programming languages and their environments / libraries / compilers etc.

huh, I guess I’m going to have to try it because I just realized that I had a hidden assumption that code was definitionally the lightest way to describe a problem

A lot of people use PlusCal, which is basically pseudocode that compiles to TLA+. Depending on what you're modeling, PlusCal or directly writing TLA+ might be a better fit.

I think that's fair. It's been described elsewhere as 'exhaustively testable pseudocode'.