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.
Generate portable C code from high-level models. Executable code is automatically checked against its specification and for undefined behaviour.