Tau Language

Novel Temporal Logic for Software Specification

Tau Language is able to embed and extend the most powerful decidable knowledge representation languages, logics, and Boolean algebras to describe states in the specification.

What's New
Research and Documentation

The Tau team have recently filed their patents protecting Tau Language, and we’re pleased to announce our disclosure of the research behind our languages NSO, and GSSOTC, decidable conservative extensions to the first order theory of Boolean Algebras, and the related algorithms. The first solves a long-lasting problem of finding a logic that is able to consistently refer to its own sentences, the second is a novel temporal logic.

Key Features

Declarative by Nature

Unlike other declarative programming languages, your specification doesn’t need to pin down a unique program. Instead, many programs can meet the requirements.


Tau Language unifies data and specifications, offering a decidable temporal logic with infinite datawords, theory inclusion, and closed Boolean combinations.

Infinitary Inputs, Outputs & States

Tau Language excels in specifying complex systems and real-world scenarios by effortlessly handling infinite sequences of inputs, outputs, and states.

Infinite Datawords

Tau Language is a temporal logic for specifying, reasoning, and analyzing system behavior over time, ideal for models with infinite data sequences.

Time-Compatible Semantics

Tau Language’s time compatibility ensures consistent and logical element interactions across different times, preserving temporal logic integrity.

Description Logics Support

Tau Language seamlessly supports description logics, enhancing its usability across knowledge-based applications.

Specify your next Project in Tau Language
Executable Specifications

Correct-by-construction software,
improved testing efficiency & coverage

Automated Validation & Verification

No proofs, no manual verification,
reduced human oversights

Expressivity & Language Extension

Improved capture of real-life descriptions and complex domains with the capability to incorporate and extend other formal and KRR-based languages.

Streamlined Compliance

Simplified and more precise compliance assessment with formalized standards

Ideal for Complex Systems

Accommodates infinite data types, provides clear abstractions for managing complexity

Reliability & Robustness

Identification and handling of edge cases that may otherwise be overlooked


Access the Low-Level Overview

Tau Language is a language extension of other classical logics (the “base logics”) intended to be a logic whose formulas denote software specifications. A formula specifies a program having at each point of time inputs, outputs and internal states (memory), which can themselves hold other software specifications…

See What Tau Can Do For You