This is the compiler for the Horus formal verification tool. See the main repository for full documentation.
Kindly note, Horus is a tool consisting of two separate components: Horus-Check, released under the AGPLv3 license, and Horus-Compile, released under the Cairo Toolkit License. When "Horus" is referenced, the reference is to the two components jointly.
Horus is currently in the alpha stage and no guarantee is being given as to the accuracy and/or completeness of any of the outputs the tool may generate. The tool is provided on an 'as is' basis, without warranties or conditions of any kind, either express or implied, including without limitation as to the outputs of the verification process and the security of any system verified using Horus. As per the relevant licenses, to the fullest extent permitted by the law, Nethermind disclaims any liability in connection with your use of Horus and/or any of its outputs.
Please also note that the terminology used by Horus, including but not limited to words such as 'guarantee', should be interpreted strictly within the remit of formal verification terminology. These words are not intended to, and shall not be construed as having legal significance of any kind.
For the avoidance of doubt, the outputs generated by Horus and/or your usage thereof shall not be considered or relied upon as any form of financial, investment, tax, legal, regulatory, or other advice.
Horus-Check is licensed under AGPLv3 (Copyright (C) 2023 Nethermind). For more information on the dependencies, please see here.
Horus-Compile is licensed under the Cairo Toolkit License (Copyright (C) 2023 Nethermind), pursuant to an exception granted to Nethermind by Starkware Industries Ltd. For more information on the dependencies please see here.