Adding to your list, Z3, Lean, F\*, Koka are all non-trivial I think.

nequo 4 months ago | parent | context | favorite | on: What would it take to recreate Bell Labs?

Adding to your list, Z3, Lean, F*, Koka are all non-trivial I think.