thinking about lil short term potential feasible services i could offer if next phase of stuff works out: would ppl be interested in a TLA+ models from impls as a (paid!) service thing??? this is still at *least* a few weeks out but maybe longer but it should be manageable for certain targets