I'm about 90% done with that refinement spec. Should I add a 'proofs' directory to Venice and submit a PR?

Definitely!

Is the proof runnable via Gradle?

Should I also check in leap frog (the spec, not the code)? It's in the data validation closed source right now.

I admit, that spec currently has one case it doesn't cover. It's a case we're not super concerned about, but it nags at me that it reduces the specs 'thoroughness'

I don’t think we should open source the proof for leap frog until we also open source leap frog… otherwise it doesn’t make much sense, IMHO

And I do hope we open source LF/LP soon 😄 …

Makes sense. We need to do some tech debt on that front. Put it through it's rounds across more prod stores

Also. Gives me an inDay or two to fix it up a bit

https://github.com/linkedin/venice/pull/56/files @Sushant Mane @Felix GV @Nisarg Thakkar Any of you folks wanna give this a gander? (as the only other folks in this channel)

In case this interests any other folks, I'd kind of been struggling with the notion of Weak/Strong fairness, but this short read actually demystified it pretty well: https://www.hillelwayne.com/post/fairness/

Yahoo! Merged a new subproject called 'specs' to main branch. Thanks @Gaojie Liu for the review. Looking forward to see what else shows up there

Oh man. I forgot about the message truncation here. We should probably pin a link to the spec directory to this channel at least so it doesn't look so desolate 😂

For folks in this channel who are interested in this sort of thing, I published VIP-2, which contains a TLA+ spec for LeapFrog. LeapFrog was actually the original motivator for looking into TLA+ for me, and was the first Venice thing we spec'd internally. This is the first time we've talked about it in detail in open source, so please take a look. I'm expecting to add one more spec to this PR when I get time, as the VIP discusses how we'd need to change some of the implementation of LeapFrog, so I need to add a refinement spec to show that the heartbeat approach doesn't break the original invariants of the first spec.

The proofs channel archive is here: https://www.linen.dev/s/venicedb/c/proofs