LeanRPC

Serve Lean 4 functions as RPC methods over HTTP

Key Features

Attribute-Based RPC: Mark functions with @[rpc] to expose as JSON-RPC endpoints via HTTP server
Type-Safe Serialization: Automatic JSON handling with compile-time type checking
Multi-Monad Support: IO, Except, StateT, ReaderT, and Lean elaboration contexts

Usage

Installation

Add LeanRPC as a dependency to your lakefile.toml and run lake update:

[[require]]
name = "LeanRPC"
git = "https://github.com/oOo0oOo/LeanRPC.git"
rev = "main"

Quick Start

import LeanRPC
import LeanSerde.SnapshotTypes

open LeanRPC.Server

-- Mark functions as RPC methods
@[rpc]
partial def collatzSequence (n : Nat) : IO (Except String (List Nat)) := do
  let rec go n acc :=
    if n == 1 then (1 :: acc).reverse
    else go (if n % 2 == 0 then n / 2 else 3 * n + 1) (n :: acc)
  if n == 0 then pure (.error "Start number must be positive")
  else pure (.ok (go n []))

-- Initialize the function registry
init_RPC

def main : IO Unit := do
  IO.println "Interactions to try:"
  IO.println "curl -X POST -H 'Content-Type: application/json' -d '{\"jsonrpc\":\"2.0\",\"method\":\"collatzSequence\",\"params\":[50],\"id\":1}' http://localhost:8080\n"

  -- Start server (buildRPC is created during init_RPC)
  startRPCServer { port := 8080 } buildRPC

Guide

Defining RPC Functions

Functions are exposed as RPC methods using the @[rpc] attribute. Supported signatures: α₁ → α₂ → ... → αₙ → M β where all types have LeanSerde.Serializable instances.

Supported monads M:

Pure (no monad): β
Basic: IO β, Except ε β, Option β
Transformers: StateT σ IO β, ReaderT ρ IO β
Sandboxed: CoreM β, MetaM β, TermElabM β, CommandElabM β
Utilities: Task β

Note: Sandboxed monads execute in isolated environments without access to the current Lean context. Limited and relatively slow.

Examples: String → IO String, Nat → List α → CoreM Bool, StateT Nat IO String

Server Configuration

The server can be configured by passing a ServerConfig record to startRPCServer:

let config : ServerConfig := {
  port : Nat := 8080
  host : String := "127.0.0.1"  -- Currently only supports IPv4
  maxBodySize : Nat := 1024 * 1024
  logging: Bool := true
}

LeanRPC uses LeanSerde for JSON serialization. Many standard types are supported by default. For custom types you can derive LeanSerde.Serializable or implement the LeanSerde.Serializable interface manually. See the LeanSerde documentation for details.

Built-in Methods

list_methods: Returns a list of all registered RPC methods.

Client Examples

Once the server is running, you can send JSON-RPC 2.0 requests.

Lean

import LeanRPC.Client
open LeanRPC.Client

def main : IO Unit := do
  let result : Except String (List Nat) ← callRPC {} "collatzSequence" [50]

curl

curl -X POST -H 'Content-Type: application/json' \
  -d '{"jsonrpc": "2.0", "method": "collatzSequence", "params": [50], "id": 1}' \
  http://127.0.0.1:8080/

Rust

use serde_json::json;

fn main() {
    let response = reqwest::blocking::Client::new()
        .post("http://127.0.0.1:8080")
        .json(&json!({"jsonrpc": "2.0", "method": "collatzSequence", "params": [50], "id": 1}))
        .send().unwrap();
    println!("{}", response.json::<serde_json::Value>().unwrap()["result"]);
}

Python

import requests

response = requests.post(
  "http://127.0.0.1:8080",
  headers={"Content-Type": "application/json"},
  json={"jsonrpc": "2.0", "method": "collatzSequence", "params": [50], "id": 1}
)

Development

Running Tests

lake test

Security Considerations

LeanRPC provides no built-in authentication or support for HTTPS. For production, secure endpoints by placing the server behind an authenticating reverse proxy, such as Nginx or Caddy.

License

MIT

LeanRPC0.2.0