Alternatives to Songlark

The domain in which Songlark sits (high-assurance reactive control systems) has been around for a while. There are many alternative projects that cohabit the same space, but few of them solve the whole problem, or have the same goals and principles. This page compares a few of them to the Songlark toolchain.

The main open-source alternatives are Kind2 and Copilot (Galois).

Kind2

Kind2 is a Lustre model checker. As a research project, it has a different objective. The input language is more limited and does not support polymorphic definitions (generics) or bounded recursion. Its support for bounded arithmetic is limited.

The compilation is experimental with Rust as the only target. Compilation of integers is unsound, as they are model-checked as arbitrary-precision integers and compiled to bounded integers.

Kind2 uses advanced invariant generation techniques. Proofs depend on a heuristic invariant generator that can be somewhat unpredictable, however. The invariant generator can also generate invariants that cannot be represented in the source language, which means it's not always possible to manually work around the unpredictable behaviour of the invariant generator when it doesn't find the right ones.

If you are only interested in proving properties about models without compiling them, and you don't care too much about continuous integration, then Kind2 is probably good for you.

Copilot (Galois)

Copilot is a Haskell embedded domain-specific-language for writing real-time safety monitors. It's specifically targeted at runtime verification, which is the dynamic monitoring of signals. (The term can be read as "verification at runtime" rather than "formal verification of runtime".) It supports model checking via Kind2, but this feature was added after-the-fact, rather than being designed-in initially. Bounded-precision integers are model-checked as arbitrary-precision integers.

As it was not designed to be model-checked, Copilot has no contract system to allow for abstracting parts of the system. The produced program is monolithic, in that a function definition in the Haskell meta-language will get inlined into its call-site in the generated code. Without abstraction, you can't break the program into small pieces, prove each correct, and compose them together.

If you have an existing system that you'd like to augment with some runtime monitoring, and you don't want to prove too much, then Copilot is probably good for you.