They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify

They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code). See https://github.com/awslabs/shuttle https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3 https://www.amazon.science/publications/using-lightweight-fo... Disclaimer: used to work at AWS and had some involvement in this stuff