It's true that TLA+ doesn't rely on types to specify properties, but it's still untyped. You could implement similar arbitrary properties in any programming lan

It's true that TLA+ doesn't rely on types to specify properties, but it's still untyped. You could implement similar arbitrary properties in any programming language as predicates.