Abstract: “An approach to generating provably correct sequential code from for- mally developed algorithmic designs is presented. Given an algorithm modelled in the Event-B formalism, we automatically translate the design into the SPARK programming language. Our translation builds upon Abrial’s approach to the development of sequential programs from Event-B models. However, as well as generating code, our approach also automatically generates code level specifications, i.e. SPARK pre- and post-conditions, along with loop invariants. In terms of the SPARK proof tools, having the loop invariants increases verification automation. A prototype, known as E-SPARK, has been implemented as a plugin for the Rodin Platform (Event-B toolkit), and tested on a range of examples, i.e. searching, sorting and numeric calculations.”