Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language of commands for controlling/guiding the proof assistant, and LTAC is the "type-level programming language on steroids" for writing type-level proofs. ("Type-level" is the important word here - the Curry-Howard correspondence allows us to encode propositions as types, and proofs are inhabitants of those types).
When I was getting into certified programming, I found it helpful to try different proof systems until I could understand the common features. I found Microsoft's Lean Theorem Prover [2] to be quite user friendly and well documented, and I liked the syntax and feel. Also, trying out something bare-bones like Twelf [3] can help too, because there is not a lot of extra stuff tacked on and it is closer to an assembly language for machine-assisted proofs.
For doing real-world things with Coq such as writing a simple web server, check out Guillaume Claret's blog [4].
Agda is comparable to Coq in terms of what they can do (I have heard). Idris is a "PacMan-complete" language that you might find useful for writing real-world programs, but I am not familiar with its suitability for programs relying on really complex proofs. Edwin Brady is writing a book on Idris [5], and you can get pre-release drafts through the Manning Early Access Program.
[1] http://plv.csail.mit.edu/bedrock/
[2] https://leanprover.github.io/
[3] http://twelf.org/wiki/Main_Page
[4] http://coq-blog.clarus.me/
[5] https://www.manning.com/books/type-driven-development-with-i...
https://www.cl.cam.ac.uk/~mjcg/cambridge-wilding-sept08.pdf
Specifics on how they do EAL7 CPU and crypto here:
http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf
Eschersoft's tools below. They also have C analyzer.
http://www.eschertech.com/products/pd_and_spark.php
Specware from Kesterel Institute, like lots of their stuff, is pretty cool but I think efficiency dictates manual derivation of code. Gets you close to it, though.
ftp://ftp.kestrel.edu/pub/papers/specware/specware-jm.pdf
Esterel's SCADE w/ SPARK Ada below. Has huge list of application areas. I clearly forgot automotive in applicatino areas.
http://www.sigada.org/conf/sigada2003/SIGAda2003-CDROM/SIGAd...
Note: There's also been hardware synthesis from PVS and HOL specs. Most cool stuff like that is hard to get legally due to ACM/IEEE/Spring BS. I mention it so you know it's been done. I even saw one manual, formal verification of standard cells themselves. Getting close to the bottom. If my brain was whole, I'd be pulling out solid-state, physics books & doing HOL models of process nodes' molecules to get a jump on their asses lol.