[
https://issues.apache.org/jira/browse/RATIS-2542?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Ivan Andika updated RATIS-2542:
-------------------------------
Description:
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
Articles
* https://antithesis.com/blog/2026/finding-bugs-in-raft-implementations/
was:
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
> 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
> Articles
> * https://antithesis.com/blog/2026/finding-bugs-in-raft-implementations/
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
