Posts  / #POST-220149
REDDIT

Coq vs F* vs Lean

A
Feb 19, 2026 · 14:58

i want to create formal verification for my rust project.

i see that signal uses hax to extract rust code into F\*

when searching online it looks like Coq seems popular, but i dont know enough to understand why signal would use F\*. both seem pretty capable, so id like to know how to compare them for use in my project.

i am testing with F\* in my project and i seem to have some memory leak issues. so id like to know more if that something i should study more and fix or if i should switch to Coq or Lean?

id like to commit to one for my project.