You don't write some clean code that things can be proved about... you have the things you want provable about the code, then you develop code along with a proof that those things remain correct. Want to prove something not originally envisioned? Want to change definition of what you're proving? Start over again.

So, you have that data structure which determines credence. What is credence, exactly? The AI should have a bit set here when it's telling a lie? What's a lie? The AI outputs a sequence of characters. It affects your actions after you read it. Whenever it is a lie is as much a fact about you as about the AI.

The black box assumption wasn't the first. It came after many failed attempts to make AI using normal, very direct programming techniques - and after growing understanding that if we make AI, it'll likely be some kind of self developing seed which will do god only knows what after it had read the internet (and which won't be able to talk to you otherwise). Consider this site. A lot of stuff on this site tells how to modify your thought processes. You want the AI not to read and apply any techniques it comes across here. That's some restricted AI for sure. Really stubborn AI.

Furthermore there is enormous data overload even for human level intelligence. Human brain has 100 trillion connections or so.

Underhanded c contest (someone linked it in a comment) is a good example of how proofreading doesn't work. Other issue is that you can't conceivably check like this something with the size of many terabytes yourself.

The apparent understandability is a very misleading thing.

Let me give a taster. Consider a weather simulator. It is proved to simulate weather to specific precision. It is very straightforward, very clearly written. It does precisely what's written on the box - models the behaviour of air in cells, each cell has air properties.

The round off errors, however, implement a Turing-complete cellular automation in the least significant bits of the floating point numbers. That may happen even without any malice what so ever. And the round off error machine can manipulate sim's large scale state via unavoidable butterfly effect inherent in the model.

I'm not exactly sure why this matters.

I mean, OK, suppose you're right that it's possible that the world might turn out to be set up in such a way that we can keep the "upper hand" against a superintelligence. Suppose further that there is a "central dogma" here that contradicts this, and therefore that central dogma is wrong.

OK. Granting all of that, what choices ought I make differently?

One obvious example is chess playing from a significantly better position. No superintelligence has any chance against only a good human player.

Can you prove that the board position is significantly better, even against superintelligences, for anything other than trivial endgames?

And what is the superintelligence allowed to do? Trick you into making a mistake? Manipulate you into making the particular moves it wants you to? Use clever rules-lawyering to expose elements of the game that humans haven't noticed yet?

If it eats its opponent, does that cause a forfeit? Did you think it might try that?