[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-15926:
------------------------------
Description:
This aims to track the effort on formal/semi-formal verification of each aspect
in 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]
was:
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]
> 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
> Priority: Major
>
> This aims to track the effort on formal/semi-formal verification of each
> aspect in 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]
