Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Containment for AI agents - user isolation, sandboxed execution, network controls, backup/rollback. TLA+ verified.
An instructional website with progressively worked examples of TLA+ specifications and model checking.
Multi-agent coding orchestrator with quorum consensus and formal verification (TLA+, Alloy, PRISM) for Claude Code, OpenCode, and Gemini CLI. Fewer hallucinations, fewer blind spots, mathematically proven protocols.
A modern specification language and model checker for concurrent and distributed systems. Faster than TLA+/TLC.
Deterministic policy language for AI agents. Z3 + TLA+ dual-engine formal verification. Runtime enforcement <1ms.
The TLA+ Video Course by Leslie Lamport
📜 WIP Hop Protocol TLA+ Specification
MAREF: Multi-Agent Recursive Evolution Framework — Agent Governance Operating System
A collection of various TLA+ examples and helper functions for learning.
Atomic concepts & compositions thereof, expressed as structured natural language. Code is derived; intent is canonical. This is Intent-Driven Design (IDD) — author the intent first, upstream of how any system is built. Named for Grace Hopper, who argued business logic should be readable by the people who understand the business.
Bitcoin layer 2 contracts specifications using TLA+
Mathematical proof of Solana's Alpenglow consensus protocol with 100% verification success.
Transparent fault tolerance for unmodified servers as a byproduct of in-network total-order communication.
Measurement automation framework for physics labs (NMR/ODMR) with AI/MCP control — plus standalone dual-licensed lock-free STM (kamestm) and pool allocator (kamepoolalloc), TLA+/GenMC verified
ASET Seed is the minimal implementation-neutral semantic kernel of ASET Alpha (Local Recognition Algebra), with independently authored operational, relational, and causal representations, formal assurance, mechanically checked three-way congruence, and reproducible release identity.
Authorization and audit kernel for AI agents. Exhaustively model-checked with TLA+. Source-available under PolyForm Noncommercial License.
To associate your repository with the tla-plus topic, visit your repo's landing page and select "manage topics."