[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18103898#comment-18103898
]
Ivan Andika edited comment on HDDS-15926 at 8/12/26 2:56 AM:
-------------------------------------------------------------
[~smeng] Would you mind sharing your methodologies? Seems it can find some
interesting bugs, this way the community can also apply it to our workflow, we
can also amortize the token spending to more people instead of one person
spending all their tokens.
Also, since we already HDDS-15501, how about we make this (HDDS-15926) to be a
story or task under HDDS-15501 and make it focused on TLA+. Other testing under
HDDS-15501 can include things like linearizable checker, etc.
Btw good work on this, I'm glad that formal methods are being adopted.
was (Author: JIRAUSER298977):
[~smeng] Would you mind sharing your methodologies? Seems it can find some
interesting bugs, this way the community can also apply it to our workflow, we
can also amortize the token cost to the community instead of one person
spending all their tokens.
Also, since we already HDDS-15501, how about we make this (HDDS-15926) to be a
story or task under HDDS-15501 and make it focused on TLA+. Other testing under
HDDS-15501 can include things like linearizable checker, etc.
Btw good work on this, I'm glad that formal methods are being adopted.
> 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]
