Consider adding a chapter on profiling

[jonnadal]

Model checking is computationally expensive, and helping people optimize their models enables them to validate larger state spaces. For example, by eliminating an expensive backtrace creation, one model's checking time dropped from 142 seconds to 3 seconds, a 47X speed increase. See https://discord.com/channels/781357978652901386/781357978652901389/810499507149340702 for that example.

It would also be worth highlighting that the model checker can serve as a supplementary stress test for the system, helping identify bottlenecks that would otherwise limit performance in production scenarios as well.