This repository is home of the Leios R&D project whose purpose is to define a specification of the Ouroboros Leios protocol.

Caution

This project is in its very early stage and is mostly experimental and exploratory. All contributions and feedbacks are welcome. No warranties of any kind about the current or future features of Cardano are to be expected, implicitly and explicitly.

Getting started

Checkout CONTRIBUTING.md document for possible contributions and communication channels

More documentation about Leios can be found in the web site.

Content

Current

• Logbook contains a detailed account of problems,successes, failures, ideas, references and is intended as a tool to help the team members stay in sync. It's updated frequently with notes about the day-to-day work, meetings, ideas, etc.
• simulation contains experimental Haskell code to simulate the Leios protocol
• sim-rs contains experimental Rust code to simulate the Leios protocol
• site contains the sources of the aforementioned web site

Specification

Build the Agda specification for Leios using either

$ nix build --no-link --accept-flake-config .#leiosSpec

or

$ nix develop

$ cd formal-spec

$ agda Leios/SimpleSpec.agda

Archive

The Leios CIP initially proposed in November 2022, yielded the following content. While the material there is still relevant and useful, it won't be updated in the future.

• report: the LaTeX source for the design report
• CIP: the initial version of the Leios CIP
• simulation: simulation and visualisation code for investigating Leios-like network traffic patterns.