Songlark

This website describes the Songlark research project for formal verification of real-time systems. The project aimed to provide programming languages and tooling for proving correctness of safety-critical systems, such as the many computer-based controllers in a modern car.

The project is not currently being actively developed. The information here is provided for historical context.

The project contains two main artefacts:

• Songlark, an embedded language for verifying programs and compiling them to real-time C;
• Pipit, a verified toolchain for such programs; as a verified toolchain, any properties proved about the program hold on the compiled program too (up to certain assumptions).

Publications

• Pipit on the Post: proving pre- and post-conditions of reactive systems (Amos Robinson, Alex Potanin. ECOOP 2024, distinguished artefact award)
• Pipit: reactive systems in F* (Amos Robinson, Alex Potanin. TyDe 2023)

Blog posts

• Pipit: verifying reactive systems in F* (2023)
• Introduction to the Songlark model checker (2022)
• Applicative invariants for Lustre (2022)

Resources

• Amos Robinson’s personal website
• GitHub organisation