This document describes the specification and verification of Eigenlayer using the Certora Prover and manual code review findings. The work was undertaken from July 9th 2024 to august 12th 2024. The scope of this audit is the Eigen pod, pod manager, and supporting libraries. The pod manages the various validators under a user, and updates the pod manager with the number of shares to be allocated for each user based on the amount of assets locked up in the pod, or in the stakes that are registered to that pod. The pod manager manages the pods and supplies the interface between each pod and the delegation manager. As of the writing of this document, the slashing and rewarding logic have yet to be implemented and so the main focus of the audit is of sound logic and adherence to the beacon specs.