The open-source library for

formally verified code

Showing 1–16 of 1,757
Sort by
Rust
Aeneas Verified ✓

Summary: curve25519-dalek-lean-verify

Repo: https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify

Rust
Aeneas Verified ✓

Summary: SparsePostQuantumRatchet-verify

Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify

Rust
Aeneas

Summary: libsignal-verify

Repo: https://github.com/Beneficial-AI-Foundation/libsignal-verify

Rust
Dafny

Summary: Testing | small boxes

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Dafny

Summary: RustSignalMay15Sofia

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Dafny

Summary: Rust Signal Github Sofia

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Dafny
Dafny

Summary: Dafny bignums, 20250612, 1109

Rust
Rust

Summary: RustLibSignal

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Rust

Summary: LibSignal

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Rust

Summary: Sofia Testing Rust Libsignal App

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Rust

Summary: LibSignalRust_Sofia

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Rust

Summary: NO AUTOMIZATION - NO GRAPH LibSignalRust

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Verus

Summary: LibsignalAug11

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Verus

Summary: libsignal focus on dalek_lite

Repo: https://github.com/Beneficial-AI-Foundation/libsignal_focus_dalek_lite

Dafny
Dafny Verified ✓

Summary: Dalek Lite

Repo: https://github.com/Beneficial-AI-Foundation/dalek-lite/

Lean
Lean

Summary: Simple Mondas #2

Repo: https://github.com/leanprover-community/lean4-samples/tree/main/SimpleMonads