This looks nice. I wasn't aware of Acorn--how much adoption does it have in the mathematics community (or formal methods / robotics / other communities)? I feel like most are rallying around Lean.
It's a much newer project than Lean, and Lean has more adoption. But the vast majority of mathematicians aren't using formal methods at all, so perhaps the space is still oepn.