[
https://issues.apache.org/jira/browse/RATIS-2542?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18102273#comment-18102273
]
Ivan Andika commented on RATIS-2542:
------------------------------------
The Specula run for Ratis has been published in
[https://github.com/specula-org/specula-case-studies/blob/main/systems/ratis/overview.md]
, we can evaluate these and see if we can fix some issues.
> Distributed System Testing in Ratis
> -----------------------------------
>
> Key: RATIS-2542
> URL: https://issues.apache.org/jira/browse/RATIS-2542
> Project: Ratis
> Issue Type: Test
> Components: test
> Reporter: Ivan Andika
> Assignee: Ivan Andika
> Priority: Major
>
> This is a parent task for the effort to introduce distributed system testing
> to test the correctness of Ratis implementation as well provide proofs for
> Ratis-specific implementation (e.g. notifyInstallSnapshot correctness,
> repliedIndex linearizability proof, metadata entry, ratis group remove, etc).
> This would help to catch distributed system regressions and formalize
> implementation.
> Distributed system testing tools:
> * Jepsen, Ellen, Maelstorm
> * Fray
> * Hypothesis (Hegel)
> * Antithesis (paid)
> Distributed system proofs
> * TLA+
> ** Specula (https://github.com/specula-org/Specula) : AI generated TLA+
> already used to find some Raft bugs
> * Lean4
> * P frameworks
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
