[nextos]

Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together.

Nevertheless, Lean 4 has closed the gap and it's closer to those than Coq at this stage.