$AGRS is the token ↗

Tau language

Tau synthesizes software from formal specifications: instead of machine instructions, simply say what conditions must hold.

A rule, as the network holds it REAL
always o1[t] <= 2000
Illustrative: the outgoing amount never exceeds 2,000.

Tau Language overview

A declarative, decidable, and executable formal language. You write sentences that must hold over time. Tau synthesizes correct-by-construction programs from realizable specifications. Programs can reason over one another, this is unique to Tau.

Under the hood
LTL+Past modulo the first-order theory of atomless Boolean algebras. Specifications are elements of such an algebra, so the language can quantify over and refer to them, therefore it is the only language that can reason over its own sentences.
Temporal operators
next, finally, globally, until, release, yesterday, once, historically and since
Benefits

Development with Tau language

Development is like writing the tests a program must pass, and automatically getting the program that passes them.

01
Know before you run
Know if a spec will hold before you run it. Tau checks that valid outputs exist for every input sequence, so failures surface at design time rather than in production.
02
Get a program from the spec
You only write the specification. Tau synthesizes a correct-by-construction program that realizes it.
03
Updates on the Spec's Terms
A spec can state its modification conditions, which the resulting program checks against updates to decide which parts of it to apply, reject, and modify before applying, and then acts accordingly.
04
Rules about rules
A rule or larger specification can set the terms for its own amendment, as specifications are values the language reasons over.
Capabilities

A combination of properties no other language has

Decidability

Tau computes rules so you catch any that conflict

Satisfiability is logically inferred rather than sampled, so the solver's output is fully guaranteed to be correct. Testing covers the cases written as tests; a decision procedure answers over the model as a whole.

Solver output
Real
Suitable outputs can be produced for every input sequence, without depending on future inputs.
Method Realizability
Tau is built around a decidable specification logic. Its implementation checks supported specifications subject to practical resource limits.
If unsat You learn before it ships
Self-reference

A specification can reason over specifications

Tau Language has a type whose values are specifications, so a rule can set update conditions on the rules that may replace it. In other languages, a smart contract cannot hold another contract’s meaning, however they can with Tau.

A rule over a rule
3 approvals · 30 days
Raising the spending limit takes 2 approvals. Changing this rule takes 3 approvals and a 30-day delay.
Mechanism Specs as first-class values
Governs Which updates are admissible
Used for Rule chains, governance
POINTWISE REVISION

Revise specifications during execution

An update can be given as just an additional requirement. Tau can merge an update into a running specification, retain requirements that do not contradict the specification, and modify the update according to the specification before applying it.

Update path
check → revise
A program can reject and selectively accept updates upon given rules.
Checked first Unrealizable updates refused
Merged by Pointwise revision, in place
Applies to The running spec and the update
What you can build

Better software, built in a better way

A few examples of what is possible.

01
Systems that answer for themselves
Because the system is based in logic, questions about it are decided rather than estimated: what a rule permits, whether a change is safe, whether two rules can conflict.
Property — decidable, within the supported fragment
02
User-programmable systems
People using a system can change it by providing just the new requirements. The admission conditions are part of the specification rather than a separate approval process.
Property — a change is admitted only if it is satisfiable
03
High-assurance everything
An upgraded class of formal methods used in high-assurance systems, but applied to everyday software with Tau's properties. What must hold is decided before anything runs, rather than inferred from test coverage.
Property — decided, rather than sampled by tests
VS CONVENTIONAL DEVELOPMENT

The better path to correctness

The differences below come from Tau's specification-first design, decidable reasoning, and runtime revision mechanisms.

 
Conventional development
A Tau specification
What you write
An implementation — the steps the machine takes
A requirement — what must be true over time
The language itself
Turing-complete languages. Undecidable, with static analysis and formal verification applied to the implementation afterwards
A Turing-incomplete, decidable specification logic, checked subject to practical resource limits and synthesis of realizable programs
Consistency
Audits, test suites and model checking, covering the properties chosen for review
Synthesis from formal specifications: correct-by-construction
Changing it later
A development cycle: patch the code, hunt for what the change broke, re-test, redeploy, maintain
Pointwise revision. Apply the change while keeping everything else intact 
Rules about rules
Simple things such as numerical parameters
Specifications the language reasons over
Get started

Run the interpreter yourself

Start writing specifications with Tau Language now. 

Paradigm State what must hold
Decision problem Realizability
THEORY LTL+Past
Patents and research

Read the research

Much of the research on Tau Language and its solver is public. Here are a few of the papers.

© 2026 IDNI AG. All rights reserved.
Rules enforced in logic, not your device.