Eiffel is an industrial strength object-oriented language that has influenced other languages such as Java, C# and UML. It is a pure, statically typed OO language, and is used for complex systems where it provides the right paradigms to address the construction of large, high-quality object oriented software systems. Eiffel is more than a language; it is a framework for thinking about, specifying, designing and implementing object-oriented software. It has built-in support for Design By Contract (DbC) that supports the use of specification and validation of designs as part of foundational computational thinking. Students who learn the benefits of principled thinking and see the value of the related tools will retain these lessons throughout their careers.
PVS (Prototype Verification System) is a specification language and theorem prover for validating specifications. PVS helps engineers to design coherent specifications, and to predict the behaviour of systems satisfying the specifications — before implementing them. PVS provides interactive assistance to prove theorems that validate the specifications/models. PVS has been used by OPG to certify nuclear reactors, by NASA for space/avionic systems, and in a large number of other mission critical applications. PVS is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking. You cannot write code (such as Java, Ruby or Haskell). You can only write mathematics. It thus forces one to write specifications of systems (i.e. what systems do free of implementation detail) and not how they do it. Furthermore, PVS can so some automatic syntax, typing and other checks that helps ensure that specifications are meaningful. PVS can then be used to validate the specifications. PVS was featured in the movie The Martian.
TLA stands for the Temporal Logic of Actions. TLA+ is the TLA specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.