Testing non-deterministic systems is challenging due to unpredictable behaviours arising from timing, concurrency, and random inputs. This paper explores the application of model-based testing (MBT) to tackle these challenges, leveraging formal methods and tools to ensure systematic test coverage. We employ ProB, a model checker for the B method, to analyse a formal model of the system under test (SUT) and generate test scenarios from the formal B model. As a proof of concept, we apply MBT to the TLS 1.3 protocol, a widely used complex cryptographic standard, and test one of its implementation using the BouncyCastle OpenSSL Java API. While the TLS handshake is primarily deterministic, it includes non-deterministic components like cipher selection and random value generation, making it an excellent candidate for evaluating MBT’s effectiveness. We present the design and logic of our proof of concept, showcasing its flexibility to support various models and SUTs. This study demonstrates that combining formal methods, non-deterministic analysis, and state-based testing can effectively address the challenges of non-deterministic systems, enabling improved testing strategies and greater system reliability.