>>12 theoretically you could, but you must remember that Rowhammer is not a design issue, it's a physics issue. at a logical level, the process cannot read the memory of other processes. in practice it can because of electromagnetic interference. good fucking luck formalizing electromagnetics with dependent types