High-performance cryptographic primitives, quantum-resilient protocols, formal verification, and zero-knowledge infrastructure.
120K+ package downloads·1K+ GitHub stars·11 trusted partners
Cryptographic libraries, secure protocols and zero-knowledge infrastructure, with formal verification as a service.
Open source
A cryptography library for symmetric and asymmetric algorithms. Processor-specific code paths keep it fast on embedded systems and on the architectures most servers run.
Open source
High-performance TLS 1.3 and QUIC with post-quantum key exchange, built so that teams can move off older protocols one step at a time.
Open source
A zero-knowledge VM built on ZK IR, a field-native instruction set over the Baby Bear field. Code in any LLVM-supported language compiles to it through our LLVM backend, and the prover produces succinct STARK proofs.
Service
Machine-checked proofs that cryptographic operations and other security-critical components do what the standard says. We also build AI-assisted tools that check an implementation's behavior against the standard it claims to follow.
OpenZKVM runs programs compiled to ZK IR, an instruction set we designed for STARK proving, and proves that they ran correctly. The design is described in our paper.
Rust, C, C++, Go or any other LLVM language
LLVM backend that emits ZK IR bytecode
Field-native instructions over Baby Bear, few constraints each
Executes the program and proves it with Plonky3 STARKs
Release notes, research and engineering write-ups.
Nov 18, 2025 · Release
OpenCrypt 2.0 adds ML-DSA and ML-KEM implementations that outperform existing solutions by up to 2x. The benchmarks, the design decisions behind them, and how we would approach a migration.
Oct 7, 2025 · Technical
How we designed ZK IR, the 32-bit instruction set of OpenZKVM, for STARK proving efficiency and minimal constraint counts, and how OpenZKVM compares with SP1 and RISC Zero.
Sep 22, 2025 · Research
We write Coq specifications from the standards, prove our Rust implementations equivalent to them, and use AI-assisted tooling to write the proofs faster. GHASH is the worked example.
Tell us what you're working on, or book a call.