Personal Blogs

Research Highlight: First Formal Proof of MAA RMO Primitive

Investigator: Jonathan D.A. Jewell
Date: 2025-11-19
Description: This research presents the inaugural machine-checkable formal proof of the Obliterative Wipe (RMO) property within the Mutually Assured Accountability (MAA) Framework, establishing a new benchmark for provably compliant data erasure.

// --- Main Image Here: Corrected RMO Proof Certificate Image ---

// Alt Text: "A laptop screen displaying Coq proof output for 'saga_obliterate_is_RMO' with a gold certificate badge, signifying the 'First Formal Proof of MAA RMO Primitive' by Jonathan D.A. Jewell."

Today I reached a major completion milestone in pioneering formal proof within the MAA (Mutually Assured Accountability) Framework. Utilising the Coq proof assistant, there is now formal proof that the RMO (Obliterative Wipe) primitive can be demonstrated - with mathematical certainty - that deleted data is fully and provably removed from a system's state.

The RMO (remove-obliterative) is a direct response to the critical need for verifiable data deletion, particularly in the context of GDPR Article 17 (Right to Erasure). Existing systems rely on operational trust; this proof introduces a paradigm shift towards generating machine-checkable `.vo` certificates as conclusive evidence of data obliteration.

Key Proven Properties

The formal proof encompasses critical properties including completeness (all instances removed), non-existence (data is truly gone), idempotency (repeated deletions are safe), and preservation (unrelated data remains intact). The methodology offers a rigorous foundation for building highly accountable digital systems.

Impact & Future Research:

This work sets a precedent for provable compliance in cybersecurity and data privacy. It has significant implications for:
* Enhancing the verifiability of GDPR and other data protection regulations.
* Securing data lifecycles in complex, distributed systems.
* Contributing to the broader Valence Shell Initiative for provably secure digital infrastructure.

Researchers interested in formal methods, data privacy, and secure systems are encouraged to engage with this work.

I thought about why this might be, and I've come to no great conclusions over it. But here are some ideas.

The obvious thing is that the content is different, and there's a lot I put in my journal that is personal and I wouldn't want online, let alone on my employer's website, for the World to see. On the other hand, there's a lot of stuff that I put in my personal journal that is perfectly fit for wider consumption (although I'd look crazy), because it's about reflections on events and how I think about them. True there are emotional elements to it, but nothing more than I have written in nursing assignments or talked about with people in the course of my teaching.

There's also the nature of the more formal content, in that I enjoy writing about early ideas that I have, that I'd rather not have shot down in their genesis before I have a chance to refine them. It's potentially the case that I might want to hold onto them so that no-one takes them, but actually, I'm more worried about them not being good enough than I am about them being so good they're worthy of stealing.

Then I also like to do a lot of sketches and drawings and play around with ideas visually, which sometimes are far better at expressing points which would be long, meandering sentences, not always going anywhere.

Another thing is the complete randomness of the path I take in my writing. I don't think my journal makes any sense at all, and I feel that, in terms of my thoughts and feelings, there's a legitimacy to the fact that it's like that - it's how I actually think. To put it up online probably would only serve a purpose to me looking back at it and no-one else. It could, I suppose, damage what credibility I have, but I think that anyone who knows me probably sees me as being fairly random anyway.

But I actually think the main thing is that, sitting here - in front of the screen - I'm finding it harder to write than something that flows through my pen when I'm writing in my paper journal. I look at it and I think, well, I've got the chance to edit it and change it, so it should be really good. Or at least better than what I write there.

A commitment I made a long time back that no matter how terrible what I've written in my journal, no matter how I've expressed myself, or what I've thought about something (and often someone), I will never retrospectively delete or change it. It's a fixed record. That's not to say I don't later on think, wow, that was a totally inappropriate, stupid, ill-judged thing to say, but I comment on it at at that time and not by erasing how I thought and felt at the time. I find that this is really good, particularly when I'm talking about encounters or arguments or presumptions I've made that later I see a new perspective on. Sometimes that's very different to how it felt at the time or my understanding of context, and when I consider patterns, I sometimes am able to discern biases I had no idea ever existed in me, and gain some insight into the way I see the World.

It's costly, and I have literally thousands of pages in diary after diary of content, much of which I have thought I ought to index or read over in full. But it never happens, and I suppose my life in the past is interesting (to me) but not something I need to relive again and again indiscriminately.

And so, I'm thinking, if I am to establish a blogging habit, as I have a journaling one, what is the value that I can find in this that I can't accomplish through that or could do better here. Blogging for the sake of it isn't something I intend to do - there's too much stuff going on out there that needs to be done, and so much better I could do if I ran out of those. Where is this contribution to come from, or is it a contribution not to be made.

...that no-one is actually viewing this, which is disappointing, albeit what I have to say is unlikely to be crazy exciting!

Still, to give an idea of the kinds of things that associate lecturers do in their spare time.

Today I woke up early. I lay around in bed think about all kinds of things that would make the day productive and, after about 30 minutes of pondering, decided that I would push for today to be mostly focused in three areas:

1) Marking assignments (although these only came in yesterday, I feel that it is time now to start moving things along at a pace).

2) Forum development (including answering fears my students have about their grades and preparing for an online tutorial tomorrow...urg, a Sunday!).

3) Learning to program. Okay, okay, don't worry, I CAN program (so as not to lose all my credibility with my computing students!) What I want to do is learn a new programming language, specifically Erlang (Erikson Language).

Maybe, actually, the big lesson of today is really going to be learning about personal limitations, resource constraints and the importance of prioritisation. All the lessons I should have learned through 19 years of study!