Highway is a correct-by-construction (CBC) Casper-based consensus protocol. This paper contains the mathematical description of the protocol, including its safety and liveness proofs.
A pre-generated version of the PDF can be found on the GitHub releases page. To generate the PDf yourself you must have LaTeX and Biber installed on your platform then run
pdflatex -halt-on-error highway && \
biber highway && \
pdflatex -halt-on-error highway && \
pdflatex -halt-on-error highwayThe output will be highway.pdf.
If you see
! LaTeX Error: File `stix.sty' not found.
You may need to install additional parts of your LaTeX distribution (beyond the
base / recommended). E.g. if you are using texlive on Linux then you can try
sudo apt install texlive-fonts-extra