About Songlark

Songlark is the work of Amos Robinson, who is based in Sydney, Australia. Amos did his PhD at the University of New South Wales, on streaming programming languages.

While verifying control systems at an autonomous vehicle company, Amos saw firsthand the real productivity and safety gains that can come from applying light-weight formal methods such as model checking. There was a definite gap in the tools, however: the existing languages are not as expressive as they could be, which limits where they can be applied. It can also be difficult to predict whether existing properties will be able to be proved when changing the software: sometimes even changes as minor as renaming variables will cause properties to time out.

The Songlark toolchain aims to solve these two problems by providing a more expressive source language with a more predictable theorem prover. The toolchain is a concrete embodiment of Songlark's philosophical vision to help engineers to be more productive and write safer software.