Aleo
An ACL2 library about the Aleo blockchain and ecosystem.
Aleo supports private applications via zero-knowledge proofs.
This ACL2 library contains a growing collection of
formalizations, proofs, and tools
for the Aleo blockchain and ecosystem.
This ACL2 library is being developed by Provable.
Currently this library contains three sub-libraries:
- A sub-library about AleoBFT,
the consensus protocol of the Aleo blockchain.
- A sublibrary about AleoVM,
the virtual machine of the Aleo blockchain.
- A sub-library about Leo,
a programming language for zero-knowledge applications
to be deployed on the Aleo blockchain.
Subtopics
- Aleobft
- Formal model and correctness proofs of AleoBFT.
- Aleovm
- An ACL2 library for the AleoVM.
- Leo
- An ACL2 library for the Leo language.
