[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18104265#comment-18104265
]
Ivan Andika edited comment on HDDS-15926 at 8/13/26 3:47 AM:
-------------------------------------------------------------
Thanks [~smeng] for the info and the update. Let's continue using Specula
first, it is open source and actively developed. We can raise patches to
Specula if needed.
was (Author: JIRAUSER298977):
Thanks [~smeng] for the info and the update. Let's continue using Specula
first, it is open source and actively developed.
> Umbrella for Ozone TLA+ verification effort
> -------------------------------------------
>
> Key: HDDS-15926
> URL: https://issues.apache.org/jira/browse/HDDS-15926
> Project: Apache Ozone
> Issue Type: Task
> 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]
