Dependent type theory doesn't directly model the concepts of TLA+ (e.g., an eventually modality), so this doesn't really answer the question.