[jira] [Commented] (HDDS-15926) Umbrella for Ozone formal and semi-formal verification effort

["Ivan Andika (Jira)" <ji...@apache.org>]

    [ https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18098356#comment-18098356 ] 

Ivan Andika commented on HDDS-15926:
------------------------------------

Also related to HDDS-15501

> 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org