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

Jump to bottom

Meta: Functional Verification for Kyber #143

Closed
12 of 16 tasks
karthikbhargavan opened this issue Dec 4, 2023 · 2 comments
Closed
12 of 16 tasks

Meta: Functional Verification for Kyber #143

karthikbhargavan opened this issue Dec 4, 2023 · 2 comments
Assignees
@W95Psp @karthikbhargavan

Comments

@karthikbhargavan
Copy link
Contributor

karthikbhargavan commented Dec 4, 2023 •
edited
Loading

This is a meta-issue tracking formal functional correctness proofs for the Kyber code.
Currently, all module checked below are fully verified with respect to a high-level spec of Kyber in F*.
@karthikbhargavan karthikbhargavan changed the title Functional Verification for Kyber Meta: Functional Verification for Kyber Jan 10, 2024
@karthikbhargavan
Copy link
Contributor Author

See PR #161

@franziskuskiefer
Copy link
Member

The biggest chunk was done in #161. We'll track the remaining issues from above separately.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@W95Psp W95Psp

@karthikbhargavan karthikbhargavan

Labels
None yet
Projects
libcrux
Status: ✅ Done
Milestone
No milestone
Development

No branches or pull requests
3 participants
@W95Psp @franziskuskiefer @karthikbhargavan