[
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:50 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.
In the long-term, we should try to store the TLA+ instead in the codebase
instead of using Specula to generate a one-off TLA spec (which might not be
correct). However, I don't think the community has the expertise for this yet,
so the current one-off TLA+ to find bugs are good (at least there are
actionable fixes).
was (Author: JIRAUSER298977):
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.
> 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]
