Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add future work item about proving other properties #92

Merged
merged 1 commit into from
Dec 13, 2024
Merged

Add future work item about proving other properties #92

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions reports/future.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,11 @@

\begin{enumerate}

\item \emph{Prove some of the other properties guaranteed by 3SF.} This project focused on verifying AccountableSafety, arguably the most critical property that the 3SF protocol must satisfy.
However, it is also arguably the most challenging to verify through model checking, as it is the only property involving all honest participants that must hold true under fully asynchronous network conditions.
In contrast, proving that honest nodes never commit slashable offenses (a non-distributed system property dependent only on the behavior of a single node) or properties reliant on network synchrony, such as reorg-resilience and dynamic-availability, is expected to be simpler, albeit this would require extending the \tlap{} encoding to include the behavior of honest nodes, which was unnecessary for verifying AccountableSafety.


\item \emph{Generating inputs to the Python specification.} As we have noted,
the power of our~\tlap{} specifications is the ability to generate examples
with Apalache. This would help the authors of the Python specification to
Expand Down
Loading