Describe who sends what to whom, and in what order.
Hibana is a Rust library for choreographic programming. You write one shared protocol and each participant's Rust code. Hibana derives the communication steps for each participant and checks its sends and receives at runtime.
Participants can be tasks in one program or programs on different
machines. The core uses no_std, requires no heap allocator,
and runs on stable Rust 1.95 or newer. Your program supplies its memory.
Status: hibana 0.9.9 is published on crates.io.
use hibana::{
Endpoint, EndpointError,
g::{self, Msg},
runtime::program::{RoleProgram, project},
};
fn ping_pong() -> (RoleProgram<0>, RoleProgram<1>) {
let choreography = g::seq(
g::send::<0, 1, Msg<1, u32>>(),
g::send::<1, 0, Msg<2, u32>>(),
);
(project(&choreography), project(&choreography))
}
async fn client(endpoint: &mut Endpoint<'_, 0>) -> Result<u32, EndpointError> {
endpoint.send::<Msg<1, u32>>(&7).await?;
endpoint.recv::<Msg<2, u32>>().await
}One global protocol
Describe messages, choices, parallel communication, and repetition in one shared protocol. Each role follows its part through an endpoint.
Endpoint projection
Rust's const evaluation derives local protocols for each role. Projection produces communication data. You write the participant functions in Rust.
Endpoint operations
A successful send or receive advances a permitted step. Previewing a branch, rejecting an operation, or dropping it before commit does not advance the protocol.
no_std and no heap allocation
The core uses memory supplied by your program and borrowed buffers. The same API runs on hosted and embedded targets.
Choices and errors
Roles must learn choices before acting differently. The transport supplies deadlines. A transport error ends the current session run without advancing the failed operation.
Verification
The Lean proofs cover stated protocol models and assumptions. Deadlock freedom also requires an accepted protocol, conforming transport, matching codecs, and fair scheduling. See the guarantees.
Core and Integrations
hibana remains protocol-neutral. Integrations own deployment-specific behavior without expanding the core API.
hibana Core
Write a global protocol and drive each participant through an endpoint. Hibana projects the protocol at compile time and checks communication at runtime.
hibana-quic QUIC / HTTP/3
QUIC v1/v2 and HTTP/3 using Hibana 0.9.9. Its protocol describes communication among packet processing, TLS, transmission, and timers. Applications can also write a shared protocol for messages sent over QUIC.
The hello-quic example sends numbers from a client and returns their squares from a server. Both use endpoints derived from the same application protocol.
hibana-tls TLS 1.3
TLS 1.3 handshake and authentication for hibana-quic, using Hibana 0.9.9. Its protocol describes the order of transcript checks and key handoff. It provides TLS for QUIC, with no TCP TLS records or TLS socket API.
QUIC and TLS are experimental. Hibana's protocol proofs do not prove the correctness of these implementations.
hibana-pico Integration
Cargo-native projection, attach, and run integration for raw Hibana choreography, including WASI P1 examples driven through endpoint and carrier progress.
hibana-mgmt Management
Ordinary management choreography prefixes and payload owners kept outside the protocol-neutral Hibana core.
hibana-epf Evidence
Compact typed evidence images, ingestion, evaluation, and replay built from Hibana observation records outside the core crate.