There is quite a bit of documentation on the design but I haven't seen anything more specific along the lines of a TLA+, Lean, etc specification. There are ple

There is quite a bit of documentation on the design but I haven't seen anything more specific along the lines of a TLA+, Lean, etc specification. There are plenty of projects like this and I'm curious how they go about creating specifications, checking their designs, etc. Would the project benefit from a formal model or proofs? A colleague and I started a side project to provide specifications for core Openstack components but we're keeping our minds open to other projects as well.