Dynamis Formal Specifications

TLA+ specifications for the Dynamis Agentic Operating System.

This repository contains 30+ formally verified specifications covering consensus, safety, economics, and agent coordination. Each specification has been model-checked using TLC and/or Apalache.

---

Overview

Dynamis uses TLA+ for formal verification of all safety-critical protocol components. Every specification is accompanied by a .cfg configuration file and has been verified to satisfy its stated invariants and temporal properties.

Why TLA+?

Standard testing catches bugs in code. Formal verification catches bugs in design. TLA+ lets us prove that our consensus protocol, token economics, and safety systems are correct at the mathematical level, before writing the first line of implementation code.

---

Specifications

Consensus and Coordination

Spec	Description	Checker
PoHConsensus.tla	Proof-of-History consensus with 1kHz BLAKE3 clock ticks	TLC
AnchorSync.tla	Cross-node state synchronization and anchor commitment	TLC + Apalache
GPCTController.tla	Global Protocol Clock and time-based coordination	TLC + Apalache
AgentEconomics.tla	Agent staking, rewards, and capacity allocation	TLC + Apalache

Safety and Security

Spec	Description	Checker
Soteria.tla	Dual-factor authentication (passkey + cryptographic signature)	TLC
Sentinel.tla	Autonomous AI threat detection with risk scoring	TLC + Apalache
Guardian.tla	Social recovery with threshold signatures	TLC + Apalache
TimeLock.tla	Time-delayed transaction vaults with emergency freeze	TLC + Apalache
RateLimiter.tla	Adaptive rate limiting with inductive proofs	TLC
ShieldedPool.tla	Privacy-preserving transaction pools	TLC

Token and Asset Management

Spec	Description	Checker
DRC20.tla	Token standard with transfer, approval, and burning	TLC + Apalache
AtomicLedger.tla	Double-entry ledger with conservation invariants	TLC
TokenTransfer.tla	Core token transfer with balance safety	TLC
Staking.tla	Validator staking and delegation	TLC + Apalache
Escrow.tla	Time-bound escrow with dispute resolution	TLC + Apalache

Inscriptions and Data

Spec	Description	Checker
EtchProtocol.tla	Permanent on-chain data inscription	TLC
InscriptionBatcher.tla	Batched inscription processing	TLC + Apalache
ConfidentialInscription.tla	Client-side encrypted inscriptions	TLC
NFTPrivacy.tla	Privacy-preserving NFT operations	TLC

Reputation and Governance

Spec	Description	Checker
ReputationSystem.tla	5-actor-type dimensional reputation	TLC
DimensionalReputation.tla	Multi-axis reputation with decay	Apalache
SocialRecovery.tla	Account recovery via guardian network	TLC

Layer 2

Spec	Description	Checker
L2StateCommitment.tla	L2 state commitment and challenge resolution	TLC + Apalache

---

Proofs

The proofs/ directory and various *Inductive.tla files contain inductive invariant proofs that verify safety properties hold across all reachable states, not just bounded model checking.

Key inductive proofs:

• RateLimiterInductiveProof.tla : Rate limiter safety is inductive
• SoteriaInductive.tla : Dual-factor authentication correctness
• ShieldedPoolInductive.tla : Privacy pool conservation
• DRC20Inductive.tla : Token supply conservation

---

Running Verification

Prerequisites

• Java 17+ (for TLC)
• TLA+ Tools (tla2tools.jar)

Model Check a Specification

java -jar tla2tools.jar -config PoHConsensus.cfg PoHConsensus.tla

Run with Apalache (bounded model checker)

apalache-mc check --config=SentinelApalache.cfg SentinelApalache.tla

---

Verification Status

See VERIFICATION_STATUS.md for the current pass/fail status of all specifications.

---

License

Apache 2.0

Copyright 2026 Dynamis Network. Built by Cryptozoa.