I have no idea what the CIA uses. Never met anyone from the CIA in their IT department(s).

The folks I know who have worked at the NSA (and people still in their employ) have mentioned several projects. One of their projects has been a hardened Linux implementation:

https://github.com/SELinuxProject

The NSA also releases several tools and packages of recommendations on how to tighten common operating systems and tools. They have written (I'm told) their own embedded OS (or more than one) for some of their widgets and gadgets over the years. I haven't seen this, because they've never released it outside their agency.

As for using Ada: One of the interesting things that one can do with a strongly typed, very tightly/highly defined language like Ada is that you can run a tool over your code to prove that you don't have any static errors. There's a language subset and a tool available in the GNU Ada package called "SPARK" that will do this to Ada code: allow you to perform formal, static validation of the correctness of a program. That's a very large advance.

One of the biggest beefs I hear about Ada is how "it seems like you never get anything done!" Software people who are used to C moan about how many times the Ada compiler spits out their source code, saying in effect "No, that won't work, you're wrong here, here and here." This was a frustration of mine the first time I played with Ada as well. 

Well, if one persists and fixes the errors, eventually the Ada source compiles. Then you link the program with the libraries... then you run it. And often... you find that it just works. There are no run-time errors. You find where you need to add functionality, or add additional provisions, but what most people new to Ada find amazing is that once they fight their code past the compiler's anal-retentive type/range/etc checking, it just works. Lots of people who grew up hacking C/C++ act like abused spouses, flinching and expecting their Ada programs to spit up blood at run time. They can't believe that "it just works." Well, that's what happens when you use a tool that has much, much more information encoded about your variables, what they are, how you're going to use/access them, from where, etc. 

Ada has several other advantages over C/C++, including a better exception handling mechanism, better run-time type checking, better package handling. There's a flip side to C++ vs. Ada: C++ started as a pre-processor to C that was basically "C with classes." Then the effort that became C++ started rolling, and while it started as "C with classes, inheritance and OOP" by the mid-late 90's, C++ blew up into this hugely complicated language that had two full paradigms contained in the language: OOP, and generics implemented with template replication of code, which could blow up the size of generated code rather rapidly.

It got so bad so quickly that one of the efforts I was involved with was to travel to Japan and meet with Japanese embedded device companies, Northern Telecom from Canada, a couple other companies from the US, and the toolchain company Cygnus. We tried to hash out a "embedded system subset" of C++. This effort became part of "Embedded C++" aka "EC++" which has had a checkered history in software development. The C++ language gurus took offense to the very idea, thinking their language as 'perfect.'

Well, the idea behind EC++ didn't go away, even if the priests of C++ language development ridiculed the idea. There is another subset called "Misra," and this one has more "juice" behind it. They're both trying to get at the same result: Get a smaller, easier-to-verify/debug subset of C++. These efforts came about because C++ is a hugely complex language, with lots of obscurant details that are difficult to remember. Example: I haven't really written any FORTRAN (66, 77 or 90) since about 1992, but I can remember FORTRAN better and more reliably than C++, which I used until about 15 years ago. C++ just has so many more obscure, tedious details than most any other language used in industry. Heck, I can remember more details of programming System/370 assembly language on IBM mainframes than I can of certain aspects of C++ - and I haven't done any IBM S/370 work since 1988.

It follows then that writing operating systems in C++ is fraught with problems that are going to be difficult to find. If the language has features that are difficult to remember correctly, then it's a cinch that they're often going to have errors in how they're used, which leads to reliability problems.

At the core of the C++ language's problem is this: Valid C programs are valid C++ programs. You cannot have secure software in a language that accepts such a loosely-defined program as you write in C. 

Linux appears to be moving in the direction of using the language "Rust" for kernel implementation, because Linus (and others) see that C/C++ won't allow Linux to become a highly reliable OS in the future. Matter of fact, Linus raised some hackles recently when he declared C++ to be a "crap language." For the record, I've thought so too for over a decade...

Rust appears to be an OK language, but I think Ada still has the edge, because Ada has years of development behind it, including things like a compiler language verification suite - I can verify that my compiler of choice actually implements Ada correctly, thereby allowing me to have confidence in the toolchain for writing code. 

We have big problems in the world of computing and software systems now, costing big money, big privacy breaches, with big consequences. We need to grow up and make the field of programming and computer engineering professional, and I believe that not only do we need to become much more selective about implementation languages and architectures, we need to have licensing exams (much like a PE exam) for people who are creating and implementing public safety, health, critical control software systems. Part and parcel of this licensing needs to be background checks, and some systems should be restricted as to who can work on them and access the source code - much as we had "US-born citizen" requirements on defense projects in the 1980's.