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 BibTex installed on your platform then run

pdflatex -halt-on-error highway && \
  bibtex highway && \
  pdflatex -halt-on-error highway && \
  pdflatex -halt-on-error highway

The 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