Formal verification for message-passing systems using TLA+. Automatically generates TLA+ specifications from TypeScript code.
