This is what we did for our KV store at S3: https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-ama

This is what we did for our KV store at S3: 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... Using https://github.com/awslabs/shuttle https://github.com/awslabs/shuttle which works on our real Rust code.