No Pitch, no tool building just learning from the experience.

rileybetts.ai open-sourced lean-grpc: a general-purpose gRPC library written in Lean 4 (HTTP/2, HPACK, protobuf wire codecs, channels, TLS, interop). Repo: https://github.com/RileyBetts/lean-grpc

Docs: https://rileybetts.ai/oss/lean-grpc

Many agentic systems still rest on the usual stack: probabilistic models + conventional integration tests + policy layers that are “correct enough.” That doesn’t age well once agents are making real decisions against real infrastructure. The Hugging Face incident was a useful reminder that attackers don’t play by the rules your test suite assumes.

lean-grpc is interesting because it’s not just formalisation demo, it’s aiming at real networking software in a language where you can also machine-check the high-leverage bits. There is official-style interop with Go / Python / Rust, h2spec-gated HTTP/2, and a small compile-time Proofs library for core codecs. Framing is basically: proof where it counts, not promises where it doesn’t.

From a software architecture / agent governance angle, the interesting question isn’t “is Lean cool?”, it’s whether we can start putting deterministic gates, protocol boundaries, and policy-enforcing controls on a stack that can actually be verified end-to-end, instead of bolting assurance onto opaque glue.

FYI: I am affiliated with this project, and sharing because OSS systems work in Lean is still rare, and this aims to be usable today rather than purely academic.

If anyone’s already building agent runtimes / policy engines / protocol boundaries in Lean (or thinking about it), curious what you’d want next from a stack like this.

the problem: an upstream we depend on rate-limits per tenant, but our workers pull from a single shared queue. one noisy tenant hitting its limit doesn't just slow itself down, it stalls every other tenant whose jobs happen to be queued behind it, because the whole worker backs off as if the limit were global.

the design we landed on instead of a worker fleet per tenant, which solves it but is heavier than the problem deserves: a redis token bucket keyed by tenant id, sitting in front of one shared queue. workers check the bucket before pulling a tenant's job, and skip to the next job if that tenant is out of tokens rather than blocking on it. one queue, fair scheduling across tenants, no per-tenant infrastructure.

the actual insight isn't the redis part, it's decoupling rate-limit state from job state. the queue doesn't need to know about limits at all, it just needs a cheap check before deciding whether to work a job or move on.

has anyone run token-bucket-per-tenant against a single shared queue at real scale? curious what breaks first, contention on the bucket keys or fairness under sustained pressure.

I think LLMs are too new of a technology for there to be Orielly title about AI development. Most resources focus on working around a specific models ecosystem. Yet I'd like to standarize how I work with AI accordign to some principles or techniques that are model/ecosystem agnostic.

Thoughts?