  Distributed algorithms offer challenges in checking that they meet their
specifications. Verification techniques can be extended to deal with the
verification of safety properties of distributed algorithms. In this paper, we
present an approach for combining correct-by-construction approaches and
transformations of formal models (Event-B) into programs (DistAlgo) to address
the design of verified distributed programs. We define a subset LB (Local
Event-B) of the Event-B modelling language restricted to events modelling the
classical actions of distributed programs as internal or local computations,
sending messages and receiving messages. We define then transformations of the
various elements of the LB language into DistAlgo programs. The general
methodology consists in starting from a statement of the problem to program and
then progressively producing an LB model obtained after several refinement
steps of the initial LB model. The derivation of the LB model is not described
in the current paper and has already been addressed in other works. The
transformation of LB models into DistAlgo programs is illustrated through a
simple example. The refinement process and the soundness of the transformation
allow one to produce correct-by-construction distributed programs.
