Agreed that conceptual simplicity is always best, and the current Casper FFG + LMD-GHOST doesn't have provable guarantees yet (though seems to be working in practice). I'm excited to see slight modifications to the consensus/forkchoice algo that do have provable guarantees, like [Goldfish](https://www.paradigm.xyz/2022/09/goldfish) from Paradigm Research.