I feel like this is the same black hole as small local models.

Things people want to be awesome and true, and things that are actually awesome and true don't intersect the way people want them to.

…so if there was an easy way to do provably correct AI code, it would be nice.

…but I’d also like a frontier that runs on my raspberry pi and a cheap fully autonomous self driving car that just uses a single cell phone camera.

Unfortunately wanting those doesn't make them exist; and people telling you they do exist usually are either a) uninformed, or b) selling something.