Software Development,
by Describing it in Sentences

Tau advances formal methods by removing coding from the process, while expanding its industrial capability, reliability and ease of maintenance. Tau enables you to automatically create the most complex, provably correct software, by simply writing sentences about what you want the software to do.

Tau is a world-class software development tool capable of covering a wider and more complex scope than current and formal development methods.

Prof. Enrico Franconi, Founder of KRDB Research Centre, Principal Investigator of applied research projects at European Space Agency; former Vice-Rector for Research, and current Director of the Computer Science and Artificial Intelligence Institute of the Faculty of Engineering at Free University of Bozen-Bolzano, Italy

“Tau Pro is designed for those who understand the significance of model-based software development and are committed to pushing its boundaries. It is a precision tool, supporting in a streamlined fashion the requirements, design, analysis, verification, and validation of complex software systems, and finely tuned for engineers and developers.”

Software as Sentences™

Executable Specifications

Specifications on Tau take the form of sentences, improving clarity and precision in your software descriptions. These sentences are directly executable, making your description the software itself. As your team collaborates on describing the software, you define what agreement means, which Tau detects. The agreed description is executable software, simplifying development by letting you focus on “what” the software should be, while Tau handles the “how”.

Specify Software Completely

The full system behavior of a wider scope and higher complexity of software are expressible in Tau compared to common formal languages, and directly executable in Tau itself.

Software Correctness on Another Level


Software you develop is correct-by-construction and error-free according to your description, so it is guaranteed that your requirements are met.

Verification, Removed

Formal verification is not necessary on Tau, it is a fully correct-by-construction process with directly executable specifications and automatic contradiction detection over a wider and more complex software spectrum than common formal languages. This reduces the risk of design errors and redevelopment costs across a broader range of software than ever before.

Built-in Consistency

Tau detects the contradictions in your specification. Tau guarantees whether a valid program that meets the specification exists, meaning that for any input at any point in time, exists a memory state or output as specified.

Validation Simplified

As the software requirements are working software in sentence form, it’s easier to simply read the entire software. Further, you may query the software’s behavior and receive accurate responses on its functionality and possible outcomes. This overall makes traditional validation simpler.

Heavy Duty Solution for Any Software Complexity

Tau is for rapid and rigorous software development, allowing specification of a wider scope of programs than common formal languages, from complex systems to simple applications. It is for industries that demand precise and safe software development while also requiring efficient development speed.

Language Extension

Tau is able to embed and extend a wide variety of other formal languages, in particular KRR Languages, to describe states, inputs and outputs in the specification.

The abilities of Tau Language are open-ended, allowing you to continually add more powerful languages to the system, making it even stronger. Further, you’re able to add a level of interoperability between languages, by extending multiple languages at once. This enhances the usability, communication and collaboration in the development process.

Refer to Sentences in the Same Language

Inputs, outputs, and memory registers in a Tau specification can hold Tau specifications themselves, and a Tau specification can have statements about Tau statements.

Infinite States & Transitions

Tau supports certain infinite state machines, enhancing its expressiveness. There are infinitely many possibilities for input / output / state, per each time step, so each position carries a data value from an infinite domain of sentences.

Tau vs  Other Formal Methods

Tau outperforms conventional formal methods with its inherent expressiveness, infinite data values and its extensibility to add more languages. It allows complete system specification of a wider and more complex range of software, while ensuring correct-by-construction output. The use of Software as Sentences™, removes code and verification steps, offering an intuitive and straightforward approach to developing software.

Reinventing The Development Process

Development by Agreement

Enable simultaneous development by multiple people on the same part of the software, including non-technical and end-users. Defined agreements allow you to combine requirements and ideas to create software solutions that bridge the gap between stakeholder desires and a successful outcome.

Scaling Development Teams & Discussions

Scale your development team without development and communication bottlenecks. The high-level requirements given by contributors are operational software based on your agreement, with deep collaboration and governance across departments and end-users, enabled by complex rule setting. Further, Tau facilitates large-scale discussion with consensus detection, using ontologies and logical reasoning to clarify decisions & agreements.

Super Version Control

Easily create, switch between and compare software versions by using different definitions of agreement from which software is created. Using multiple agreements, engineers simultaneously work on multiple versions of your software, with clear management, version tracking, one-click implementations and instant merging.

Universal Software Accessibility

Simply read the software description in sentences. Tau supports knowledge representation languages, allowing you to capture real-world concepts and knowledge in software descriptions and improve the software’s readability.

Cut Traditional Testing Cycles

Testing is no longer for bugs as each description is an executable specification, resulting in correct-by- construction software, according to your description. Testing is now ensuring your description is as desired. Traditional testing is obsolete.

$312 bn/Annum

Traditional testing cycle costs using traditional methods


Traditional testing cycle costs using Tau

Tau ensures high system reliability by guaranteeing the conditions you expressed in Tau Language are met throughout execution.

This capability provides an assurance that every consistent specification is executable without errors for any input, ensuring the software never breaks and always produces an output. This guarantees that computational resources are not wasted waiting for an answer, contributing to a robust and dependable software solution.

Software Control You've Never Seen
Control Software Behavior & Updates Indefinitely

Extensive Behavior Control

Specify prohibitive and obligating constraints over any part of your software with deeply complex rules, which Tau will satisfy.

Tau’s behaviour is also specifiable with constraints, enabling you to design the perfect tool for software development. This simultaneous development of software and the tool itself produces a positive feedback loop in utility & performance gains.

Post Release Control

Have full control over post-release updates and define complex rules for accepting changes in any configuration indefinitely. Tau enables you to specify exactly what updates or changes you will accept post-release.

Any update or tampering that doesn’t comply with your expressed rules is automatically rejected by your software, providing an added layer of security.

Tau Knowledge Market

Combine your team’s Knowledge into a knowledgebase to deduce insights and highlight solutions.

Automatically discover external users to your business who hold the precise knowledge your solution requires.

Automatically monetize the combined knowledge of your team in the Tau marketplace.

Instantly import requirements by sharing custom knowledge forms with external stakeholders.

Logical Properties


Tau has superior reasoning ability as its logic is able to fully simultaneously reason over its own software, the software you create and all formalized information within its system. This enables Tau to handle a wider and more complex scope of software compared to current formal languages, ensuring seamless integration and performance across various types of software applications.


You have guaranteed ability to constructively prove the correctness of all software operations in finite time, since Tau Language is a decidable, vastly expressive, variant of temporal logic. This ensures computational resources are not wasted.
Ontologies Enabling Domain Specific Knowledge

Use existing domain specific ontologies or define your own terms and build industry-specific software solutions with unparalleled accuracy and efficiency.

From healthcare to finance, education, manufacturing, and beyond, any industry can design bespoke ontologies that precisely capture much of their unique knowledge structures and requirements.


1. Tau is decidable, therefore it cannot express all possible programs. However, Tau has advanced expressiveness compared to common specification languages while maintaining its decidability, and it will be a challenge to find real-world software that cannot be specified.

2. Formal Languages & Controlled Natural Languages (CNLs) are not simple to use. Tau uniquely combines formal specification and knowledge, while making it simpler to use by applying Natural Language Processing techniques to the specification process.

3. Logical reasoning typically requires high computational resources, however Tau uses novel and better algorithms along with extremely strong engineering expertise.

4. Tau is not a universal solution. There are cases where it may not be the optimal choice for a software project. However, virtually any software project will find parts that are suitable for Tau use.