[tlaplus] Design Validation using TLA+/TLC Model checker

I'm trying to develop a specification for a distributed system. When I use some temporal properties in the specification and run the model checker, it runs successfully without any issues/errors. However, I have a question: how do I know/validate that the design I made has been proper or optimal? For example, my system design consists of uploading and downloading shared files. I simulated several scenarios with a different number of files, e.g., 10, 20, 50, and 100, the termination state was reached and the files were all successfully consumed by several downloaders. I see that the number of states being executed is proportional to the number of files being processed. But how to tell whether the design has been optimal? How do I measure that based on the TLC model checker's results?
In addition, if I want to compare several different approaches/designs for the same system and measure how good their performance is, can this be achieved by analyzing the results of the TLC model checker? If yes, what could be considered to determine whether one design has better performance than the others? Thank you for your attention and I really appreciate your opinion and suggestions.

Best regards,
Putrama