[
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:52 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.
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.
Btw good work on this, I'm happy 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]