[[F-star]] is a dependently typed functional programming language and proof assistant developed at Microsoft Research. It is designed to support formal verification of software systems, allowing programmers to write code and proofs in the same language. [[F-star]] combines features from ML-like languages, dependent types, and automated theorem provers. One of the main features of [[F-star]] is its support for dependent types. Dependent types allow types to depend on values, enabling more precise specifications and stronger static guarantees. This makes it possible to express complex properties about programs and reason about them formally. [[F-star]] provides a rich type system that includes various constructs like algebraic data types, higher-order functions, refinement types, effects, and monadic programming. These features facilitate the development of expressive and modular specifications. The proof aspects of [[F-star]] are based on an [[SMT]] ([[Satisfiability Modulo Theories]]) solver called Z3. [[F-star]] leverages Z3's capabilities to automatically verify certain properties of programs specified in the language. This allows developers to write proofs using tactics or declarative proof scripts. [[F-star]] also supports interactive theorem proving using an interface called FStar.Reflection. This enables users to prove properties interactively by writing proof scripts that manipulate terms symbolically. In addition to program verification, [[F-star]] can be used for program extraction. Once a program has been verified in [[F-star]], it can be extracted into efficient OCaml or F# code. [[F-star]] has been used successfully in various projects, including verifying security protocols, compilers, operating systems components, cryptographic libraries, web servers, and more. Its powerful type system and automatic theorem proving capabilities make it a popular choice for developing safe and secure software systems. Overall, [[F-star]] provides a powerful combination of programming language features and formal verification capabilities for building [[correct-by-construction]] software systems. It offers a balance between automation and user-guided proof development, making it suitable for both beginners and experienced formal verification practitioners.