Formal proofs can probably show that spectre and meltdown aren't exploited by enforcing type-safety for all speculative memory accesses, but that requires at le

Formal proofs can probably show that spectre and meltdown aren't exploited by enforcing type-safety for all speculative memory accesses, but that requires at least some knowledge of the target processor and may still be slower at processing untrusted input. There's very little that can be done about rowhammer with formal methods because it breaks the assumptions of any formal model of computation (that values stored to RAM are the same values that will be eventually read from RAM).