Unfortuately there is none. QEMU is a large project and doesn't have much formal design or API documentation. On the other hand it's not big enough (compared for instance to the Linux kernel) to have a wider community interested in trying to provide internals documentation for newcomers.
Our general advice is "look at the existing code for the bit you're interested in to see how it works". You can sometimes find descriptions of the overall architecture online in third party blog posts and the like, but if they're more than a few years old then be wary that they might be out of date -- they're likely to be right in general principles and wrong in details, because things change.
For adding new instructions to an existing ISA: the first couple of sections of https://www.qemu.org/docs/master/devel/index-tcg.html are relevant here. Depending on the target it might or might not use decodetree (decodetree is much easier to add a new insn to, but some older targets still do by-hand switch-statement based decoding.) Look at how an existing insn that is similar to what you want to do works.
Implementing CHERI in particular is going to be pretty awful, because the things it does (like 128-bit pointers) break various assumptions QEMU makes. The University of Cambridge forked QEMU to add CHERI support for MIPS and RISC-V and I think also AArch64: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri... -- but the changes are pretty invasive and also not likely to be very fast. (The fork looks like it's based on 6.0, so three years old now.)
(If anybody is interested in trying to write up some documentation for QEMU's internals (either a general overview/roadmap or something on a particular subsystem), I'd be happy to code-review patches that add something to the "Developer Information" subsection of our manual.)
Well, they have reasonable documentation for certain external APIs (syscalls, boot parameters, sysfs files, etc). But not internal API documentation or "formal design".
Certain things are sketched and outlined, and certain things have detailed documentation, but as a whole there is no "formal design" of the system.
It's not really bonkers though because it turns out that formal designs doesn't necessarily make better software. Or rather, the formal designs that academia might have taught. There is a formal design, it's the code.
20 or 30 years ago, there was this big push that formal designs should be the key piece of work and you should be able to press a button and generate the application from the design automatically. Turns out they were so wrong they basically went 360 back to right again and that's what we do. It's just that the design doesn't look like some crazy incomprehensible executable-UML, but programming languages. Which are quite legible, precise, and unambiguous (at least compared to English), and make very good languages to write designs in.
(The place where they are still wrong of is that you don't need to know or care about any of the fine detail in order to make a good design. Once you accept that, then specifying the design with code is pretty reasonable.)
Indeed, I was going to point out the lack for KVM as well. The same is also very true when it comes to Linux networking stuff. One of the most difficult things I've ever had to do was complicated networking stuff with KVM/qemu VMs when I had nobody to ask or talk to about it. There are enormous swaths of undocumented surface (or lightly documented by a blog post that may or may not be accurate anymore, and is nowhere near comprehensive). One of my biggest hope for LLMs like GPT-4 is the ability to improve on this, though as of right now it hallucinates like mad. The more niche the case, the worse it gets too.
Well, every time this line of thinking comes up, I don't believe there is a gofundme, indiegogo, patreon, etc to which I could donate. Because I for sure think that would be a good investment for future generations, but you are correct that I almost certainly couldn't convince my employer to spend the money. I'd guess that's partially because they don't directly benefit from qemu, setting aside the daily use of buildkit which for sure does. Come to think of it, I'd guess Docker(Mirantis?) is BY FAR the most "you really, really should be a corporate sponsor" of qemu
Well, you can donate to the project (there's a paypal link at the bottom of https://www.qemu.org/sponsors/ which donates to the Software Freedom Conservancy earmarking it as being for QEMU), *but* doing that won't cause somebody to be paid to work on the project (it can cover random project expenses like CI usage, I think). Mostly our sponsorship is either "in-kind" (access to compute hosts, hosting downloads, cloud compute credits etc) or else is sponsorship to help pay for the annual KVM Forum conference.
In general there is no mechanism for "pay money to have work happen" because pretty much all non-hobbyist QEMU developers are doing it because they're paid by some company (RedHat, Linaro, etc etc etc) to do that work as their full time job. So they're not in the market for random small side jobs.
The primary nexus for QEMU developers is the qemu-devel mailing list. (Very high traffic because it's also used for patchmails.) The irc channel is a bit more variable and tends in particular to be quiet outside UK/Europe working hours, just because most QEMU devs happen to be Europe based.
I discourage private emails sent direct to me on QEMU topics (because they should generally be to public lists so other community members can answer them or benefit from the answer), but you can find me on the mailing lists and irc.
Our general advice is "look at the existing code for the bit you're interested in to see how it works". You can sometimes find descriptions of the overall architecture online in third party blog posts and the like, but if they're more than a few years old then be wary that they might be out of date -- they're likely to be right in general principles and wrong in details, because things change.
For adding new instructions to an existing ISA: the first couple of sections of https://www.qemu.org/docs/master/devel/index-tcg.html are relevant here. Depending on the target it might or might not use decodetree (decodetree is much easier to add a new insn to, but some older targets still do by-hand switch-statement based decoding.) Look at how an existing insn that is similar to what you want to do works.
Implementing CHERI in particular is going to be pretty awful, because the things it does (like 128-bit pointers) break various assumptions QEMU makes. The University of Cambridge forked QEMU to add CHERI support for MIPS and RISC-V and I think also AArch64: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri... -- but the changes are pretty invasive and also not likely to be very fast. (The fork looks like it's based on 6.0, so three years old now.)
(If anybody is interested in trying to write up some documentation for QEMU's internals (either a general overview/roadmap or something on a particular subsystem), I'd be happy to code-review patches that add something to the "Developer Information" subsection of our manual.)