Wir realisieren einen einfachen Ansatz, eine logische Typtheorie zur Spezifikation und Verifikation von nebenläufigen Programmen und Systemen zu nutzen. Bisher wurden Typtheorien mit Erfolg im Bereich funktionaler Programme zur Sicherstellung partieller oder vollständiger Korrektheit eingesetzt. Hier stellen wir eine Einbettung von nebenläufigen Programmen und Systemen in den Calculus of Inductive Constructions vor, die nicht nur einfach und natürlich ist, sondern es uns erlaubt, die Typtheorie in voller Allgemeinheit zu nutzen. Als Basis verwenden wir die zugrundeliegende Idee der UNITY Methode, entwickelt von Chandy und Misra, Programme und Systeme als unbeschränkt nichtdeterministische iterative Transformationen darzustellen. Als Spezifikations- und Verifikationssprache verwenden wir eine Variante der temporalen UNITY-Logik in dem ausdrucksstarken Rahmen der Logik höherer Ordnung, die uns die Typtheorie nach der Propositions-as-Types-Interpretation zur Verfügung stellt. Als erster Schritt und Ausgangspunkt für Anwendungen wurde eine verifizierte Temporal-Logik Bibliothek für den Beweisassistenten COQ entwickelt, die zur Spezifikation und Verifikation von nebenläufigen Programmen und Systemen eingesetzt werden kann. Der konkrete Einsatz der Bibliothek wird an einem kleinen Beispiel vorgeführt. Die Bibliothek ist offen für Erweiterungen und wird entsprechend der Erfahrung aus zukünftigen Fallstudien weiterentwickelt.