Beneficial AI Foundation
Popular repositories Loading
-
-
-
formal-verification-skills
formal-verification-skills PublicFormal verification of Rust code with AI-assisted specification and proof.
-
-
curve25519-dalek-lean-verify
curve25519-dalek-lean-verify PublicVerifying curve25519-dalek using Lean
Repositories
-
- ref-impl-simulation Public
Can Lean prove that a real Rust implementation simulates a Rust reference implementation of the same RFC, with both translated by Aeneas? Three studies: ChaCha20, X25519, HPKE.
- SparsePostQuantumRatchet-verify Public Forked from signalapp/SparsePostQuantumRatchet
Project to formally verify SPQR using Lean
- KeyedVerificationAnonymousCredential-model Public
Formalization of keyed-verification anonymous credential (KVAC) framework of Orrù, Revisiting Keyed-Verification Anonymous Credentials (IACR ePrint 2024/1552)
- dalek-lite Public Forked from dalek-cryptography/curve25519-dalek
A pure-Rust implementation of group operations on Ristretto and Curve25519
- spqr-sm-bridge Public
Lean 4 proof that transfers secure-messaging's SPQR correctness bound to the extracted SparsePostQuantumRatchet code (conditional on four open facts)
- formal-verification-skills Public
Formal verification of Rust code with AI-assisted specification and proof.
- self-healing-fv Public
Self-healing CI for verified Rust: an agent repairs Lean proofs after Rust/Aeneas/Lean changes, behind mechanical gates (SCI-1706)
- libsignal-verify Public Forked from signalapp/libsignal
Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.
- curve25519-dalek-fork Public Forked from dalek-cryptography/curve25519-dalek
Staging verification work in preparation for upstreaming
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…