Cure: A strongly-typed, dependently-typed programming language for the BEAM with built-in FSMs and SMT verification