[nickpsecurity]

Sure you can. I've proposed how to do it here several times. You can start like Niklaus Wirth with a simple interpreter (eg P-code) + basic, routines for hardware. You write compiler as series of small passes (no optimization) in that interpreter. Compile it with itself. Add optimizations and recompile.

For hardware, you start with simplified CPU like a Forth or ZPU processor. One you can check by hand and eye on an older process node. Reverify it with itself. Then run above step for software on it. Optionally better EDA tools, too.

The diversity method ports the simple interpreter or compiler to a number of CPU architectures or dev tools. Pick whichever you want. If you aim for same binary, you'll need compiler designed to do that or reproducible builds like Wheeler links to up thread.

[noobermin]

"There exists" is not the same as it is practical. My sentiment doesn't regard possibility, but feasibility for the average user.

[nickpsecurity]

It's quite feasible. You just pay a programmer or smart student to do it for you using the published literature. Done. Even stronger if you trust them. Use multiple, distrusting pros on same project if more trustworthiness is needed. What you cant afford you crowd fund or ask for grants.

It's a question of priorities rather than feasibility. Most users or customers dont care enough to invest time or effort needed. End of story. Same one as usual for strong INFOSEC.

I'll also add that there already exists certifying compilers for C and Standard ML that both extract to ML. The ML extracted is simple enough to hand-compile to ASM following one of two guides. So, not only can oma human verify no subversion, there's already a production one with machine-checked proof that's also be checked by humans [again].