Re: [tlaplus] On a type of TLA+ contract

I think Irwan's comment is about many industrial TLA+ specs not being made available, so no-one writes about them, making it harder to gauge who uses them and/or use those examples to become a new TLA+ contractor.

That said, it's not like there are no industrial-scale specs out there. Here are some I know about:

What I'm being paid to work with right now, and actively growing (I'm using them not writing them, though): https://github.com/muratdem/MDBTLA/tree/main
I wrote the simple-model sub-folder here (I'm actually proud of how many doc comments it has): https://github.com/tlaplus/azure-cosmos-tla
Confidential Consortium Framework specs https://microsoft.github.io/CCF/main/architecture/raft_tla.html
etcd consensus work (related to above, sort of) https://github.com/etcd-io/raft/tree/main/tla

Of course I'm not a contractor (at least the way we mean it here), and none of these were open sourced from contract work (research orgs and open source contribs mostly). So, perhaps Irwan's point stands when it comes to contract work. Just wanted to share some actual production-scale examples that are available right now. Maybe they are an under-used teaching resource, if someone wanted to / had time to make heavily annotated versions of these specs, showing how they are structured and how to work with them.

Best,

-Finn

On Fri, Jul 4, 2025 at 3:14 PM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote:

Hi Andrew,

That is just my hypothetical question to find the root problem. Forgive me if it is incorrect.

Irwan

On Saturday, July 5, 2025, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
Hi Irwan, what do you mean by there being no incentive to open the knowledge to the public?

On Fri, Jul 4, 2025 at 4:04 PM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote:
Hi Andrew,

I believe the root questions need to be answered are:

Why a company have to asked you for the short term contract?

Because, they don't have staff that knows TLA+.

Why they don't have the staff?

Because TLA+ engineer is hard to find

Why TLA+ engineer is hard to find?

Because it is hard for non math person to learn TLA+

Why it is hard for non math person to learn TLA+?

Because there is no complete and easy to read books teaching TLA+ in real world usage?

Why there is no complete and easy to read books teaching TLA+ in real world usage?

Because there is no incentives to open the knowledge to public

Why there is no incentives to open the knowledge to public?

Because...

Irwan

On Saturday, July 5, 2025, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
Hi all,

I wrote a post on a type of TLA+ contract I've done a few times, why it never worked out as well as hoped, and what could be changed so future contracts see more success:

https://ahelwer.ca/post/2025-07-04-tla-contracts/

Andrew Helwer

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/76851a09-632a-4b93-9e5c-96dfbfa9dc21n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4z7AZzXn5P35ehhd6OGGx1ZA9ykj6FxN74L5H-rtEWrBQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVz7aT57aS1imCJ9PwgEcNKeawrJneRh7aFSriTbDpHYA%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4y8PTTO7EgNaP%3DT8NMAJZ6fgBAvrQOJkFZ%2BZ9iFBp5pcA%40mail.gmail.com.