[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18104198#comment-18104198
]
Siyao Meng commented on HDDS-15926:
-----------------------------------
[~ivanandika] Yeah, happy to. I changed this to a task.
Right now for the new ones I use Specula, the tool you mentioned earlier. It
reads the code, writes a TLA+ spec + invariants, model-checks it with TLC, then
repros violations back at the code level.
Honestly, my own process probably isn't token-optimal. :) I mostly let Claude
survey a service, point me at the juicy parts, then grind through each target.
Running the model checker itself barely costs tokens. It's just compute. What
burns tokens is Claude reading the service to write the spec, fixing it until
the spec is a valid model, plus the double-check at the end, and that work is
what makes a finding trustworthy.
So far this has produced the sub-tasks under this umbrella and a handful of
confirmed bugs, but most of the catalog is still untouched. I plan to share the
list in the description so people can grab a target and run it themselves. Most
of the token cost comes from reading and understanding a whole service from
scratch on every run, so the idea is to slice Ozone into small targets once and
let people each take one.
> 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]
