Moritz Systems are experts in embedded solutions that host innovative solutions in Fintech, Insurtech, Smart Energy, Smart Buildings. Industry 4.0 (IIoT), HealthTech, Medtech, Digital Health, Martech, Sustainability and Waste Management.

Continuing from our previous article, let us take an example of how to write a TLA+ proof for a real-world specification of a distributed system. For this exercise we will go through the Voucher Trading System process as specified by the RFC3506 hosted by IETF. The distributed and concurrent systems require a consensus protocol to achieve overall system reliability and immunity to failures of nodes. We decided to select for this VTS network a simple Two-phase commit protocol.

We are looking for a candidate to fill the position of a BSD/Linux kernel developer. The programmer will be responsible for device drivers and bootloaders for embedded x86_64 and aarch64-based systems.