Caution
Important Disclaimer & Acceptance of Risk
This is a proof-of-concept implementation in its very early stage and is mostly experimental and exploratory. This code is provided "as is" for research and educational purposes only. All contributions and feedbacks are welcome. By using this code, you acknowledge and accept all associated risks, and our company disclaims any liability for damages or losses.
This repository is to define a formal specification of the Ouroboros Leios protocol.
Build the Agda specification for Leios using either
$ nix build --no-link --accept-flake-config .#leiosSpecor
$ nix develop
$ cd formal-spec
$ agda Everything.agda