Sufficiently complex operating systems will never be trustworthy not because of maliciousness, but because of bugs.
Pick any old version of Linux and browse the local privilege escalation attacks. It seems likely that recent versions of linux have as-yet undiscovered attacks. The existence of even one means that the OS is not trustworthy in the presence of non-trustworthy applications.
As long as Ginseng is more amenable to verification than the Linux kernel, this isn't just pushing the issue around, but rather reducing the work needed.