TLA+Property-Based Testing

The Algorithm and the Implementation are two different things. Test (Model-Check) the algorithm and use this model (the specification) to verify that the implementation really implements the algorithm via Property Based Testing which comes up by itself with test-cases. Interesting non-algorithm stuff is still tested via unit-tests.