Skip to content

Conversation

@rikosellic
Copy link
Collaborator

We will prove some real concurrency proofs with RwLock. VerusSync is useful, but I think it is somewhat restrictive to extend because it is a proc-macro. We will do this in a traditional way, and this is the first step.

@rikosellic rikosellic added the pure proof Exec-unrelated proofs label Jan 8, 2026
@rikosellic rikosellic merged commit c30c798 into asterinas:main Jan 8, 2026
1 check passed
@rikosellic rikosellic deleted the rwarc-proof branch January 9, 2026 06:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

pure proof Exec-unrelated proofs

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant