[Aurel300]

Welcome to the research field of program refinement. There are a couple of approaches one can take: - Certify: the program isn't actually checked/proven to satisfy the spec, but experts in the field will pore over the code and try to find any disparities or edge cases. - Top-down: given a spec, try to generate an implementation that satisfies it by construction. This depends a lot of the concrete framework, but e.g. Coq supports extraction of executable code from its (verified) source. The results are not very well decoupled from the spec and are often lacking in performance (single-threaded, unoptimised, etc). - Bottom-up: given an actual implementation, prove that it behaves according to the spec. This can allow for optimised programs and concurrency, but both complicate the proofs. (This happens to be my PhD research topic.)

Some work to look at, if you are curious: Event-B, Trillium, IronFleet