The World's
Most Powerful
Specification Language
Tau Language is a decidable, declarative, and executable formal language with patented breakthroughs. It is the only language that supports self-referential formal reasoning.
All software and interactions on Tau Net utilize Tau Language.
This rule prevents private data being sent within the network while in effect.
i1[t]:The actual data payload requested to be sent
i2[t]: The data sensitivity tag (0 = public, 1 = private)
always (
If the data sensitivity tag indicates private data
(i2[t] = 1
-> (
Then we must disable the network transmit switch
(o1[t] = 0
)
)
&&
always (
If the data sensitivity tag indicates public data
(i2[t] = 0
-> (
Then we enable the network transmit switch
(o1[t] = 1
)
)
This rule prevents a balance being negative.
i1[t]: the amount to transfer
i2[t]: the balance
always (
If the requested transfer amount is greater than the available balance
(i1[t] > i2[t])
-> (
Then block the transfer
o1[t] = 0
)
)
&&
always (
If the requested transfer amount is less than or equal to the balance...
(i1[t] <= i2[t]) -> (
Then approve the transfer
o1[t] = 1
)
)
Install Tau Language
Get started in three simple steps.
Step 2
Write Your First Specification
Use starter templates or examples to define requirements in logic
Step 3
Write Your First Specification
Use starter templates or examples to define requirements in logic
Tutorials and Examples
Follow hands-on guides to start building in Tau Language.
Define your first requirement
Write adaptive governance logic
Combine app and market logic
Explore examples and real use cases
Auto-building from Specification
Simply write your logical specification, and any conflicting requirement is highlighted.
Tau Language automatically builds formally correct-by-construction software from the specification and generates proofs of correctness for every component.
This rule implements an Escrow mechanism on a specific account.
Funds from the Escrow Account remain locked (o5 = 0) unless a
designated 3rd-party Arbiter approves the release.
Input Stream:
i3[t] : Sender address of the transaction. We use this to scope the
rule globally so it only affects the Escrow Account.
i6[t] : Custom input payload containing the Arbiter's approval signal.
(In this example, the Arbiter must provide {#x01}:bv[8] to release)
Output Stream:
o5[t] : Output signal (0 = Keep funds locked, 1 = Release).
—————
# Replace '#x1111...1111' with the Escrow's public key (96-char hex).
always (
(i3[t] = {#x111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111}:bv[384] && !(i6[t] = {1}:bv[64]))
? o5[t] = {0}:bv[16] : o5[t] = {1}:bv[16]
).
ARCHITECTURE:
Both layers write to the SAME policy output stream o5.
Tau logically composes multiple always(...) clauses via &&,
so a transfer is allowed ONLY if ALL clauses output o5 = 1.
Layer 1 — Immutable hard safety controls (time-lock, abs cap,
approved counterparty). Cannot be revised.
Layer 2 — Revisable per-transfer spending cap.
Pointwise revision replaces ONLY this clause.
ENGINE ENFORCEMENT:
The engine reads o5 after each transfer validation step:
o5 = 0 → block (user policy rejects transfer)
o5 = 1 → allow (user policy approves transfer)
o5 absent → allow (no user policy triggered)
SCOPE:
This contract only constrains the treasury account (i3 match).
All other senders pass through (vacuous truth from '->').
STREAM TYPES:
i1[t] : transfer amount (bv[64])
i3[t] : sender public key (bv[384])
i4[t] : recipient/counterparty (bv[384])
i5[t] : block timestamp (bv[64])
o5[t] : policy guard signal (bv[16]: 0=block, 1=allow)
POINTWISE REVISION INSTRUCTIONS:
To revise ONLY the spending cap (Layer 2), send a SEPARATE
transaction with a new rule that redefines the spending cap
clause on o5. Layer 1 remains untouched because Tau's
Pointwise revision targets the specific clause being replaced.
REVISION EXAMPLE A — Raise cap to 10000:
always (
(i3[t] = {#x111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111}:bv[384]
&& i1[t] > {10000}:bv[64])
? o5[t] = {0}:bv[16] : o5[t] = {1}:bv[16]
).
REVISION EXAMPLE B — Time-dependent cap using 'ex':
always (
ex c (
(i5[t] >= {1800000000}:bv[64] && c = {20000}:bv[64])
|| (i5[t] < {1800000000}:bv[64] && c = {10000}:bv[64]) ) && ( (i3[t] = {#x111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111}:bv[384] && i1[t] > c:bv[64])
? o5[t] = {0}:bv[16] : o5[t] = {1}:bv[16]
)
).
LAYER 1: IMMUTABLE CORE GUARD (o5)
(always (
(i3[t] = {#x111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111}:bv[384])
-> (
# 1. TIME-LOCK: Block all transfers before this timestamp.
(i5[t] < {1750000000}:bv[64] ? o5[t] = {0}:bv[16] : ( # 2. ABSOLUTE CAP: No single transfer may exceed 50000. (i1[t] > {50000}:bv[64]
? o5[t] = {0}:bv[16]
: (
# 3. APPROVED-COUNTERPARTY: Transfers above 1000 require
# the recipient to be a specific approved counterparty.
(i1[t] > {1000}:bv[64]
&& !(i4[t] = {#x222222222222222222222222222222222222222222222222222222222222222222222222222222222222222222222222}:bv[384]))
? o5[t] = {0}:bv[16]
: o5[t] = {1}:bv[16]
))
))
)
)) &&
LAYER 2: REVISABLE PER-TRANSFER SPENDING CAP (o5)
This clause is the TARGET for Pointwise revision.
Tau composes it with Layer 1: transfer allowed only if
BOTH clauses output o5 = 1.
(always (
(i3[t] = {#x111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111}:bv[384]
&& i1[t] > {5000}:bv[64])
? o5[t] = {0}:bv[16] : o5[t] = {1}:bv[16]
)). Decidable and Vastly
More Expressive
Tau Language is vastly more expressive than other specification languages, yet fully decidable. It lets developers define and generate entire systems with formal correctness.
Express complex logic across systems, agents, and interactions
Ensure provable correctness from specification to execution
Build entire applications in one unified, verifiable language
Self-Reference and
Adaptivity
Tau Language supports logical self-reference, allowing systems to reason about and modify their own logic.
This enables adaptive software that evolves with new requirements.
Write rules that update other rules
Reference a specification from within itself
Modify logic without redeploying
Maintain desired behavior across every update
Collaborative On-Chain
Development
Governance, consensus logic, and project updates are all defined in Tau Language. Projects can evolve live, based on user requirements and formal agreement.
Define and update governance logic directly in your app
Evolve systems based on live consensus
Avoid redeployments by using dynamic logic
Launch With
Formal Guarantees
All projects on Tau Net are built using logic that is verifiably safe and adaptable. Whether building apps, DAOs, agents, or full ecosystems, formal guarantees are built in.
Inherit safety,
composability,
and correctness
Build once and
adapt without loss
of reliability
Launch with logic
as the source of
truth
Interoperability by Design
All logic on Tau Net is written in Tau Language. This guarantees seamless interoperability and formal integration between all components, from apps and agents to DAOs and markets.
Share and combine logic between different projects
Build systems that interoperate by design
Define cross-project behavior with formal precision
Try Tau Language
