I've been interested in any smart contract languages/VMs that are somehow more capable of being provably correct/secure. The only one I've come across is Kadena, which internally uses the Z3 prover, but I haven't looked into the source code in depth or if it's able to be applied to custom smart contracts (dApp) as well.

Are there other blockchains that are similar? Is there a strict subset and prover for Solidity or other languages? Or things like proven smart contract kernels that can be built on top of? Eg, OpenZeppelin Contracts, but with provers rather than only audits.