tlaps

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

agentic skills to write TLA+ specs or TLAPS proofs

Examples for TLAPS (TLA+ Proof System)

Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

Jupiter Refinement Project

Markdown to LaTeX. Specs in TLA+

Research on reusable state-machine abstractions for building systems across domains, with explicit contracts, composition rules, and machine-checked proofs.

Markdown to LaTeX

Web tool that turns TLA+ specs into actionable requirements, rewrites NFRs into TLA+ monitors, and runs proof checks via a backend.

TLA+ model checking and TLAPS theorem proving for the Paxos implementation in PaxosStore by WeChat

ASET Network extends ASET Seed with distributed evidence admission while preserving local recognition authority, with independently authored operational, relational, and causal assurance representations.

ASET Runtime is the bounded execution lifecycle extension for ASET Seed. Execution may produce material; recognition remains local to Seed.

Minimal proposal layer over ASET Seed with formal assurance and reproducible release verification.

Formal Methods