Can you say more about how your work compares to existing VMs, such as the JVM?
Most commercially used VMs are not designed to the level of security required to protect humanity from an UFAI. VM escape bugs are routinely found in various JVM implementations and the complexity and structure of the VM itself precludes existing or theorized analysis tools from being able to verify the implementation to a level of detail sufficient for high-assurance systems.
To be useful in this context, a VM needs to be designed with simplicity and security as the two driving requirements. One would expect, for example, an interpreter for such a VM to occupy no more than 1,000 lines of MISRA C, which could have its security assertions proven with existing tools like Coq. The goal is to get in the core VM the simplest set of opcodes and state transitions which still allow a nearly Turing-complete (total functional, to be specific) program description language, and one which is still capable of concisely representing useful programs.
The other way in which it differs from many VM layers is that is has a non-optional strong typing system (in the spirit of Haskell, not C++).
and what sorts of things you want to prove about executions?
Type checking, mostly. Actually that aspect of the system has less to do with boxing than the design of the artificial intelligence itself. You can imagine, for example, a core evolutionary search algorithm which operated over program space by performing type-safe mutation of program elements, or achieved creative combination by substituting type-equal expressions.
It is also important to prove some properties, e.g. bounds on running time. Particularly when interacting with other untrusted agents ("sharing minds" -- machine-to-machine communication is likely to be literally uploading memories from one mind-space to another).
Type checking, mostly.
You're building a box to contain a strong AI out of type checking? I suggest that unless your types include "strings that can be displayed to a human without causing him to let the AI out of the box", this is unlikely to succeed.
bounds on running time
Won't you run into Halting Problem issues? Although perhaps that's why it's only nearly Turing-complete. Incidentally, can you quantify this and say how your machine is less powerful than a Turing-complete one but more powerful than regexes?
How are you saving the world? Please, let us know!
Whether it is solving the problem of death or teaching rationality, one of the correlated phenomena of being less wrong is making things better. Given the value many of us place on altruism, this extends beyond just ourselves and into that question of, “How can I make The Rest better?” The rest of my community. The rest of my country. The rest of my species. The rest of my world. To word it in a less other-optimizing way: How can I save the world?
So, tell us how you are saving the world. Not how you want to save the world. Not how you plan to. How you are, actively, saving the world. It doesn’t have to be “I invented a friendly AI,” or “I reformed a nation’s gender politics” or “I perfected a cryonics reviving process.” It can be a simple goal (“I taught a child how to recognize when they use ad hominen” or "I stopped using as much water to shower") or a simple action as part of a larger plan (such as “I helped with a breakthrough on reducing gas emissions in cars by five percent”).
If we accept this challenge of saving the world, then let us be open and honest with our progress. Let us put our successes on display and our shortcomings as well, so that both can be recognized, recommended, and, if need be, repaired.
If you are not doing anything to save the world, even something as simple as “learning about global risks” or “encouraging others to research a topic before deciding on it”? Then find something. Find a goal and work for it. Find an act that needs doing and do it.
Then tell us about it.