Skip to content

@Beneficial-AI-Foundation Beneficial AI Foundation

Change the repository type filter

All

    Repositories list

    128 repositories

    • slides

      Public
      Lean
      •
      MIT License
      •0•0•0•0•Updated May 1, 2026May 1, 2026

    • curve25519-dalek-lean-verify

      Public
      Verifying curve25519-dalek using Lean
      Lean
      •
      Apache License 2.0
      •15•10•17•3•Updated May 1, 2026May 1, 2026

    • signal-shot

      Public
      MIT License
      •0•1•0•0•Updated Apr 30, 2026Apr 30, 2026

    • VCV-io

      Public
      Formalized Cryptography Proofs in Lean 4
      Lean
      •
      Apache License 2.0
      •21•0•0•0•Updated Apr 30, 2026Apr 30, 2026

    • SparsePostQuantumRatchet-verify

      Public
      Project to formally verify SPQR using Lean
      Lean
      •
      GNU Affero General Public License v3.0
      •16•4•3•0•Updated Apr 30, 2026Apr 30, 2026

    • probe-lean

      Public
      Lean
      •
      MIT License
      •0•1•8•0•Updated Apr 30, 2026Apr 30, 2026

    • SVIL2026

      Public
      CSS
      •0•0•0•0•Updated Apr 28, 2026Apr 28, 2026

    • PQXDH

      Public
      HTML
      •
      MIT License
      •1•5•0•3•Updated Apr 28, 2026Apr 28, 2026

    • libsignal-verus

      Public
      Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.
      Rust
      •
      GNU Affero General Public License v3.0
      •719•0•0•0•Updated Apr 24, 2026Apr 24, 2026

    • cslib-protocols-lean

      Public
      The Lean Computer Science Library (CSLib) with protocols
      Lean
      •
      Apache License 2.0
      •128•0•0•0•Updated Apr 22, 2026Apr 22, 2026

    • FP-autoresearch

      Public
      Autoresearch experiment project to automate formal proofs
      Lean
      •
      Apache License 2.0
      •15•0•0•0•Updated Apr 22, 2026Apr 22, 2026

    • libsignal-verify

      Public
      Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.
      Rust
      •
      GNU Affero General Public License v3.0
      •719•5•0•2•Updated Apr 21, 2026Apr 21, 2026

    • probe-aeneas

      Public
      Rust
      •1•1•2•0•Updated Apr 20, 2026Apr 20, 2026

    • probe-rust

      Public
      Rust
      •1•1•2•0•Updated Apr 18, 2026Apr 18, 2026

    • FloatSpec

      Public
      Formally Verified Float Implementation with lean4
      Lean
      •
      Apache License 2.0
      •2•9•0•1•Updated Apr 16, 2026Apr 16, 2026

    • probe

      Public
      Rust
      •0•1•3•0•Updated Apr 16, 2026Apr 16, 2026

    • dalek-lean-bench

      Public
      Lean
      •
      Apache License 2.0
      •0•0•2•0•Updated Apr 15, 2026Apr 15, 2026

    • verified-ironkv

      Public
      Verus-verified implementation of Ironfleet Sharded Hash Table key-value store
      Rust
      •
      MIT License
      •2•0•0•0•Updated Apr 14, 2026Apr 14, 2026

    • dalek-verus

      Public
      A pure-Rust implementation of group operations on Ristretto and Curve25519
      Rust
      •
      Other
      •590•0•0•0•Updated Apr 14, 2026Apr 14, 2026

    • probe-verus

      Public
      Rust
      •
      MIT License
      •0•0•4•0•Updated Apr 14, 2026Apr 14, 2026

    • verus_lemma_finder

      Public
      Python
      •0•0•0•14•Updated Apr 13, 2026Apr 13, 2026

    • formal-verification-skills

      Public
      Formal verification of Rust code with AI-assisted specification and proof.
      JavaScript
      •
      MIT License
      •2•7•6•0•Updated Apr 7, 2026Apr 7, 2026

    • lean-bench

      Public archive
      Python
      •0•0•0•0•Updated Apr 5, 2026Apr 5, 2026

    • eth_certify

      Public
      SMT
      •0•0•2•0•Updated Apr 2, 2026Apr 2, 2026

    • dalek-lite

      Public
      A pure-Rust implementation of group operations on Ristretto and Curve25519
      Rust
      •
      Other
      •590•9•0•2•Updated Mar 26, 2026Mar 26, 2026

    • scip-callgraph

      Public
      TypeScript
      •0•6•3•1•Updated Mar 26, 2026Mar 26, 2026

    • libsignal_focus_dalek_lite

      Public
      Rust
      •1•0•0•0•Updated Mar 24, 2026Mar 24, 2026

    • visuals

      Public
      Visualizations for verification projects
      TeX
      •0•0•0•0•Updated Mar 24, 2026Mar 24, 2026

    • curve25519-dalek

      Public
      A pure-Rust implementation of group operations on Ristretto and Curve25519
      Rust
      •
      Other
      •590•0•0•0•Updated Mar 22, 2026Mar 22, 2026

    • verilib-cli

      Public
      Rust
      •
      MIT License
      •0•2•7•5•Updated Mar 20, 2026Mar 20, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.