Stories have been doing the rounds this week of an "unhackable" computer. Of course, these are not strictly true. More credible media reports an "unhackable" kernel - here in New Scientist. The kernel is the complicated bit of software that lets other stuff (so called "userspace") not have to worry about directly fiddling with the hardware, and makes sure all of userspace plays nice together. Here's the page with the FAQ from the folk who built it.
Of course, making an unhackable kernel is an incredible feat - though calling it "unhackable" is a bit more fluff in my view (totally forgivable, given the achievement, mind!). I remember looking at formal proofs in my student days. This stuff is hard. To prove a whole kernel does what it says on the tin. Wow. To do it without needing to trust your compiler? Even better.
Don't think though that this is going put AV vendors out of business any time soon. The overwhelming majority of security break-ins have been due to userspace software - think heartbleed for example - or due to errors at "layer 8" (those foolish bags of meat that drive computers). As such, just having a secure kernel is only going to get you so far - which is why this is useful in things like military drones: you can start to write formally proven drone software, and no-one is going to install adobe flash on a predator drone (please, FFS tell me they aren't!).
What this should do, though is inspire confidence in "the Internet of Things" - well, at least a bit. If my door locks are going to be on the Interwebs, I damn sure want them running a kernel like this that's formally proven and open source. Sadly, we will probably end up with a load of never-updated proprietary hoo-ha that's got more holes than a hedgehog's pillow.