General-purpose Lean 4 gRPC library: HPACK + HTTP/2 + gRPC framing over Std.Async.TCP.
Standalone Lake package (1.3.0). Consumers depend via git tag or, after indexing, Reservoir.
Async model: sockets are Std.Async.TCP. v1.2.0 added a native Async h2c path (serveH2cAsync / unaryAsync) with zero .block on accept/connect/send/recv. v1.3.0 runs blocking OpenSSL on dedicated threads (connectH2Async / serveTlsAsync / ofBlockingOffLoop) so TLS does not stall the UV loop — still not nonblocking BIO; see docs/async-io.md.
Docs: rileybetts.ai/oss/lean-grpc (curated) · docs/ (full in-repo index)
Public libraries: Bytes, Hpack, H2, Proto, Grpc (umbrella LeanGrpc). Tests, examples, and the compile-time Proofs library are not consumer API.
System deps: OpenSSL (libssl-dev / Homebrew openssl + pkg-config). If headers are missing: ./scripts/fetch-openssl-headers.sh. On macOS, set LIBRARY_PATH for Homebrew OpenSSL (see docs/packaging.md).
In your lakefile.lean:
require «lean-grpc» from git
"https://github.com/RileyBetts/lean-grpc.git" @ "v1.3.0"Then import Grpc. After Reservoir lists the package you can use require «lean-grpc» without a git URL. Packaging details and the maintainer release checklist: docs/packaging.md.
| Doc | Description |
|---|---|
| Hosted docs | Curated guides on rileybetts.ai |
| docs/README.md | Full documentation index (source of truth) |
| Getting started | Typed unary helloworld, TLS, Lake dependency |
| Cookbooks | Unary · streaming · interceptors / mTLS |
| Packaging | Lake/Reservoir layout, consumer contract, release checklist |
| Provenance | Independent protocol implementation; third-party interop protos |
| Architecture | Layering and data flow |
| Async IO | Std.Async model, sync adapters, TLS caveat |
| API reference | Module catalogue |
| Protocol mapping | gRPC-over-HTTP/2 mapping for this stack |
| Conformance | Scorecard, interop matrix, allowlists |
| Formal proofs | Compile-time theorems for pure codecs |
| TLS / Envoy | In-process OpenSSL and sidecars |
| CHANGELOG | Version history |
| ROADMAP | What v1.2.0 shipped vs open proof/hardening follow-ups |
| CONTRIBUTING | Dev setup and PR expectations |
| SECURITY | Vulnerability reporting (security@rileybetts.ai) |
| Code of Conduct | Community standards |
Near grpc-go / official interop parity for general-purpose use. Core wire + Go/Python/Rust interop and stress/framing gates are CI-gated. Cloud-edge items (live Google ADC, ALTS) remain mock/allowlisted.
Rough estimates (see conformance.md for detail):
| Axis | Implemented | Tested |
|---|---|---|
| Official gRPC standard | ~95% | ~90% |
| vs grpc-go surface | ~93% | ~88% |
| vs Python (grpcio) peer | ~92% | ~82% |
| vs Rust (tonic) peer | ~92% | ~82% |
| Layer | Package | Notes |
|---|---|---|
| Bytes / slices | Bytes |
Hot-path slice views, BE helpers, buffer pool |
| HPACK | Hpack |
Static + dynamic table, Huffman encode/decode |
| HTTP/2 h2c | H2 |
Full h2spec hard gate; flow control; CONTINUATION; §8.1 |
| Protobuf (minimal) | Proto |
Enums, nested, repeated, Any/map/oneof helpers |
| gRPC | Grpc |
Duplex streams, deadlines, compression, dial/LB/retry, health/reflection/channelz |
| TLS | Grpc.Native.Tls + Grpc.Tls |
In-process OpenSSL ALPN h2 (sidecar optional); mTLS |
| ADC / xDS | Grpc.Adc, Grpc.XdsAds |
SA/metadata Bearer; ADS LDS→EDS chain |
| Codegen | protoc-gen-lean4-grpc |
Text path + real CodeGeneratorRequest path |
Allowlist: ALTS / GCE channel credentials (see Grpc.Gcp).
./scripts/fetch-openssl-headers.sh # if libssl-dev is unavailable
lake build
lake build Proofs # compile-time pure-codec theorems
lake build bytesTests hpackTests h2Tests grpcTests trailersLoopback
./.lake/build/bin/grpcTests
./scripts/build_native.sh # optional zlib_helper for peer gzip (+ tls_proxy)Formal proofs of high-leverage pure codecs (status codes, BE ints, gRPC framing, varints, HPACK integers, …): docs/proofs.md.
./scripts/gen-helloworld.sh # typed stubs → Examples/Helloworld/Generated.lean
lake build helloworldServer helloworldClient
./.lake/build/bin/helloworldServer &
./.lake/build/bin/helloworldClient 127.0.0.1 50051 WorldFull walkthrough: docs/getting-started.md. Cookbooks: unary, streaming, interceptors / mTLS.
./scripts/run-go-to-lean.sh # Go client → Lean server
GRPC_PORT=10001 ./scripts/interop-go-lean.sh
./scripts/run-python-to-lean.sh # Python client → Lean
GRPC_PORT=10001 ./scripts/interop-lean-python.sh
./scripts/run-rust-to-lean.sh # Rust (tonic) client → Lean
GRPC_PORT=10001 ./scripts/interop-lean-rust.sh
./scripts/interop-compress-go-lean.sh # gzip both directions (Go gzip server)
./scripts/interop-tls-go-lean.sh # in-process TLS Lean → Go
./scripts/run-adc-smoke.sh # ADC against local mock
./scripts/run-xds-ads-smoke.sh # Fake ADS chain → unary
./scripts/run-codegen-fixture.sh
./scripts/run-soak.sh
./scripts/h2spec.shlake build helloworldServer helloworldClient benchSoak
./.lake/build/bin/helloworldServer &
./.lake/build/bin/helloworldClient 127.0.0.1 50051 World
./.lake/build/bin/benchSoak 127.0.0.1 50051 30SPDX Apache-2.0 — see LICENSE (full terms) and NOTICE (copyright + third-party interop protos). Independent protocol implementation note: docs/provenance.md.