Songlark

Reactive programming with style
Large-scale programming features with a trustworthy reactive core.

Continuously integrated proofs
Deterministic proof replay for reliable builds. Tools for specifying internal invariants for when you need an escape hatch.

Real-time execution
Generate portable C code from high-level models. Executable code is automatically checked against its specification and for undefined behaviour.