Siyao Meng created HDDS-15926:
---------------------------------
Summary: Umbrella for Ozone formal and semi-formal verification
effort
Key: HDDS-15926
URL: https://issues.apache.org/jira/browse/HDDS-15926
Project: Apache Ozone
Issue Type: Epic
Reporter: Siyao Meng
Assignee: Siyao Meng
This aims to track the effort on formal/semi-formal verification each aspect of
Ozone, with [TLA+|https://github.com/tlaplus/tlaplus],
[P|https://github.com/p-org/P], etc.
Readings:
*
[https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/]
*
[https://zfhuang99.github.io/github%20copilot/formal%20verification/tla+/2025/05/24/ai-revolution-in-distributed-systems.html]
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
