Cure’s headline is:
Dependent Types. SMT Verification. Native FSMs. On the BEAM.
I can’t be the only one wondering what these are and what benefits they would bring us (and how that might influence when we might want to reach for Cure) 
I know you said it’s on your radar @mudasobwa so no rush, but if anyone else want’s to chime in that would be cool too!
SMT Verification means Satisfiability Modulo Theories and it’s a technology for constructing programs that can proove properties of programs. There are several free SMT solvers out there.
Native FSMs in Cure means explicit syntax for finite state machines and that the compiler knows they are FSMs and can check (or generate verification conditions for) FSM properties Dependent types are types there the type of a function result can depend on an argument, for example being able to say in the type system that appending a list of length m and a list of length n gives you a list of length m+n or that adding two vectors requires them to be the same size and gives a result the same size.
Basically, as an outsider, it’s about restricting the language so that you can make stronger guarantees about what youcdo with it.
I did my best to put some stuff regarding SMT-solvers all together: Why SMT Solvers? A Deep Dive into Formal Verification - Cure Documentation
There are links at the bottom I mostly used (Alessandro Gianola’s thesis and works.) Please tell if it anyhow answers your doubts.
Also. both LSP and MCP work, I followed Idris’ holes approach to fullfil said “holes” with what SMT-solver suggests. I am to record kinda short video and announce v0.5.0 soon.