Choose a tool by the question you want to answer. These tools use JavaScript and WebAssembly; no local broker installation is required.
Cluster Lab is view-only on phones. Use a wider screen for editing and fault controls. The first lab visit downloads its broker module; keep the page open while it loads.
Try the broker
Run real krabka brokers, producers, consumers, and apps. Inspect records and traffic, then inject a network fault.
First step: Start a producer and consumer scenario. Check that the acknowledged and consumed record counts increase.
Brokers run in Web Workers with a virtual clock and network. Phone mode is view-only; use a wider screen to edit nodes and inject faults.
Understand leader election
Explore KRaft elections, message delivery, and network partitions in a consensus simulation.
First step: Choose a cluster, press Settle, and inspect its leader and followers.
This models consensus events. Use Cluster Lab to inspect a running broker and Kafka records.
Evaluate a decision kernel
Give selected production decision functions an input and read the result beside their contracts.
First step: Open majority size, choose a preset, and compare the result with the stated contract.
A kernel result applies to that function and its preconditions. It does not establish whole-system correctness.
Inspect proof evidence
Browse recorded Why3 sessions, source contracts, proof obligations, and prover results.
First step: Select a session and follow its tree to a prover result.
Recorded proof results apply to the listed contracts and assumptions. See the verification page for the formal boundary.
Run the broker locally and produce and read a record with the containerized Kafka tools. Read how krabka is verified for the proofs, bounded models, and what those checks cover.