Open source · Lean 4
lean-grpc
HPACK, HTTP/2, and gRPC framing on Std.Async.TCP — an interop-tested Lake package for typed services in Lean 4.
An interop-tested Lake package for building typed unary and streaming services in Lean 4. Version 1.0.0. Selected pure-codec theorems ship under Proofs/; OpenSSL remains a trusted computing base — not an end-to-end TLS/gRPC proof.
Depend via Lake
require «lean-grpc» from git
"https://github.com/RileyBetts/lean-grpc.git" @ "v1.0.0"Then import Grpc. After Reservoir indexes the package you can use require «lean-grpc» without a git URL.
System deps: OpenSSL (libssl-dev / Homebrew openssl) and pkg-config.
Documentation
| Page | Topic |
|---|---|
| Getting started | Typed helloworld, TLS, Lake dependency |
| Cookbook: unary | Generated stubs, deadlines, metadata |
| Cookbook: streaming | Server/client/bidi streams |
| Cookbook: interceptors | Logging, bearer tokens, mTLS |
| TLS | In-process OpenSSL and sidecars |
| Architecture | Layering and data flow |
| API reference | Module catalogue |
| Protocol mapping | gRPC-over-HTTP/2 mapping |
| Conformance | Scorecard and allowlists |
| Packaging | Consumer contract and Reservoir |
| Roadmap | Release history and follow-ups |
| Security | Reporting and posture |
Full in-repo index (including stress demos, provenance, and the security audit): docs on GitHub.
Maturity
v1.0.0 is an interop-tested general-purpose stack with CI hard gates (h2spec, Go/Python/Rust peers, security tests) and a compile-time Proofs library for high-leverage pure codecs. Prefer defense in depth for high-risk deployments.
License
Apache-2.0. Copyright Riley Betts Ltd.