Genode/seL4 Thread

Yes, it also can be hacked. Actually, all systems can be hacked if they are made by human beings!

seL4 is like having just the steering wheel of car. You can't do anything with it, it just a small part of a bigger thing. Of course you can formally verify it, it's like formally verifying that a single nail in a house is made of metal.
Even Genode, which is based on L4, is just a framework for operating systems, a tool for building more complex OSs.

If you say this is unhackable, you need to fucking leave.
Formal verification is a great step forward, but you, OP, are a verified fuckwit. Go away until you realize how stupid your post was. If you are trolling then you did a 7/10 job but fuck off anyway.

Literal NSALinux.

Theo disagrees. And even if he's wrong, there are many attacks that this scheme won't protect against anyway. If, for example, you're using the Tor Browser Bundle and there's some exploit of the browser that exposes your real IP address, this won't protect against that. I don't even think it will protect against things like privilege escalation inside the VM. So unless you're booting a clean VM every time and not saving state between reboots, you just end up with a rooted VM.

And if you are using some amnesiac VM setup, why bother with this over Xen or anything else?

What's the threat model that Sculpt addresses?

Yeah right, like anyone who's ever sold something as 'unhackable' hasn't been completely full of shit

Putting the 'unhackable' bullshit aside, I'm more interested of seL4 as a microkernel. How is it compared to previous attempts at creating microkernels? I heard it's kinda fast, but I don't know if it's fast enough to be a serious alternative to monolithic ones.

I'm a brainlet so explain to me in simplest terms how can an unhackable kernel exist and why other software can't be unhackable like seL4 as well?

and oh could future DRM schemes borrow some ideas from seL4 and how catastrophic would that be?

Well seL4, as its name implies, is a part of the L4 series. This paper provides some insight into the developments of L4 and seL4 in particular.
dl.acm.org/citation.cfm?id=2893177