The part about S3 using lightweight formal methods in their ShardStore rust codebase is ongoing and operates on the system itself, not a model