Yes. it's guaranteed to be sound.
As per what makes it unique, from the paper:
We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching