Nowadays, deep learning applications are utilized across various critical domains such as healthcare systems, industrial control, and automated driving. The incorporation of deep learning applications into such critical contexts has sparked interest in their formal verification, necessitated by the high level of rigor demanded by these applications. This paper introduces a formal verification approach at the source code level for matrix operations, which are extensively employed by deep learning applications using the Frama-C platform. These operations are derived from the BLAS (Basic Linear Algebra Subroutines) scientific library. The formal verification process begins with the specification of the program using an annotation language in the style of Hoare logic, facilitated by the platform. A set of verification conditions is then generated based on the specified program. These verification conditions are subsequently discharged using the Coq proof assistant. The primary objective of this article is to bolster confidence in deep learning operations by demonstrating the verification of properties through logical models of memory, data structures, and operations.