‫اف استار، زبان جدیدی از مرکز تحقیقات مایکروسافت

F*: A Higher-Order Effectful Language Designed for Program Verification 

F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types.