The problem with many of these formats is they're Turing-Complete languages with input driving what they do. The input is also malicious. So, the solution so far is to isolate and mediate such things with verification going into the mechanisms for that.

An example of one for exactly your types of programs is Microsoft's Xax:

https://www.microsoft.com/en-us/research/wp-content/uploads/...

My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle:

https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...

Aren't microprocessors Turing-Complete machines that undergo formal verification?

The kind of verification they undergo varies considerably. The amount of errata in modern CPU's shows both they're not fully verified for correctness and that the verification they get works wonders given number of components & interactions. Even if fully verified, the verification would be that the Turing-Complete hardware properly implemented a model of the Turing-Complete hardware.

That kind of buys us nothing in terms of whether we'll know if programs are malicious or contain them, eh? And look at the giant, losing game that followed between the mice and the well-fed cats. It's why safety-critical systems often used deterministic, state-machines running on simple MCU's or PLC's. :)

In the examples you mention (document readers) the bugs become security problems because programs have too much privileges. Easiest way to remove security problems is not to remove bugs, but remove privileges. Privilege revocation, privilege separation, W^X work wonders.

Protocols like https, ssl and cryptography and operating systems would be my first choices.