Interface-based Programming with TLA+ (+Dependency Injection with auto-wiring)

 Implementing the algorithm with TLA+ can output interfaces in any languages together with tests agains this interface. Implementing these interfaces connects an implementation with the algorithm. The wiring of the interfaces via DI is generated by the model/algorithm. The database of implementation is provider by the implementer.