[FStar] Prove panic freedom without hand-edits
Open
- Dominant language
- F*
- Stars
- 138
- Forks
- 5
- PR merge metrics
- No merged PRs in 30d
Description
The F* verification currently requires hand-edits to the generated F* code.
We would like to eliminate these hand-edits and prove panic-freedom.
We would also like to prove panic freedom for all the core code.
Contributor guide
Assessment
This issue has not been assessed yet.