> For the complete documentation index, see [llms.txt](https://docs.ackinacki.com/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.ackinacki.com/for-node-owners/protocol-participation/block-keeper/formal-verification.md).

# Formal Verification

The formal verification of Block Keeper smart contracts was performed by the [Pruvendo Team](https://pruvendo.com/).

[Learn what formal verification is and  find out about  Pruvendo's formal verification approach.](https://drive.google.com/file/d/1xcZ5-1uLzTSMFbfHiq-4onhfwSoUWNZ2/view?usp=sharing)<br>

On the following pages, you will find:

* BLS - [Business Level Specification](https://docs.ackinacki.com/protocol-participation/block-keeper/formal-verification/block-keeper-contracts-business-level-specification),&#x20;
* HLS - [High Level Specification](https://docs.ackinacki.com/protocol-participation/block-keeper/formal-verification/block-keeper-contracts-high-level-specification),&#x20;
* LLS - Low Level Specification of Block Keeper contracts.