Hibana

What if your compiler could prove your protocol is deadlock-free?

Hibana is a #![no_std] multiparty session types engine that brings established type-theoretic guarantees into everyday systems. Write your global choreography once, project it at compile time, and get affine cursors that make protocol violations impossible.

                use hibana::g::{self, Msg, Role};

type Controller = Role<0>;
type Worker = Role<1>;
type Ping = Msg<1, ()>;
type Pong = Msg<2, ()>;

const PINGPONG: g::Program<_> = g::seq(
    g::send::<Controller, Worker, Ping>(),
    g::send::<Worker, Controller, Pong>(),
);

const CONTROLLER: g::RoleProgram<'static, 0, _> =
    g::project::<0, _, _>(&PINGPONG);
const WORKER: g::RoleProgram<'static, 1, _> =
    g::project::<1, _, _>(&PINGPONG);

let controller = cluster.attach_cursor::<0, _>(rv, sid, lane, &CONTROLLER)?;
let worker = cluster.attach_cursor::<1, _>(rv, sid, lane, &WORKER)?;

let (controller, _) = controller.flow::<Ping>()?.send(&()).await?;
let (worker, Ping(())) = worker.recv::<Ping>().await?;
let (worker, _) = worker.flow::<Pong>()?.send(&()).await?;
let (controller, Pong(())) = controller.recv::<Pong>().await?;
            

Const Projection as Effect

g::Program composes protocols with g::send, g::seq, g::par, g::route—projecting to RoleProgram without code generation. Runtime uses only 4 methods: flow/send for output, recv/offer for input

Session-as-Effect Control

Every cursor step is a CpEffect; CapFlow tokens ensure cancel, checkpoint, commit, and rollback remain affine and message-driven

Deterministic Observability

16-byte tap ring + streaming checker makes crash-stop behavior auditable; EPF (Effect Policy Filter) VM executes session-aware policies through the same capability channel

Zero Polling Transport

Drop-in transport traits let Hibana drive any async runtime without background threads or busy loops

Embedded First

#![no_std] and no_alloc by default—runs on bare metal with deterministic resource usage

Crates

Compile-time MPST with const projection, CapFlow control, and deterministic observability

hibanaworks/hibana

hibana-quic (Coming Soon)

QUIC choreography with distributed splice support for connection migration

Will be published at hibanaworks/quicworks

hibana-h3 (Coming Soon)

HTTP/3 on top of QUIC streams with typed request/response choreography

Will be published at hibanaworks/quicworks

HibanaOS (Coming Soon)

A #![no_std] unikernel with type-safe async executor and WASI host, driven entirely by Hibana session protocols

Get Started

[dependencies]
hibana = { git = "https://github.com/hibanaworks/hibana" }

GitHub · Discussions · Issues

HIBANA