A proof-oriented language & verification framework

Prove code
correct.

F* combines functional programming, precise specifications, and machine-checked proofs. State what your code should do, then prove it.

Try F* Learn F* Get F*

Dependent types. Refinements. Automated proofs.

list_append

F* source

let rec list_append (x y:list 'a)
  : z:list 'a { length x + length y == length z }
  = match x with
    | [] -> y
    | hd :: tl -> hd :: list_append tl y

The result's length is part of its type. F* proves the property for every input.

Full file ↓

OCaml

let rec listAppend_list_append (x : ('u___a) list) (y : ('u___a) list) : ('u___a) list =
  (match x with
    | [] -> y
    | (hd :: tl) -> (hd :: (listAppend_list_append tl y))
  )

The extracted OCaml function. Types and proofs erase to an ordinary list append.

Full file ↓

F#

let rec listAppend_list_append (x : list<'u___a>) (y : list<'u___a>) : list<'u___a> =
  (match x with
   | [] -> y
   | (hd :: tl) -> (hd :: (listAppend_list_append tl y)))

The extracted F# function, ready to use with .NET.

Full file ↓

C

static Prims_list__uint32 ListAppend_list_append__t(Prims_list__uint32 x, Prims_list__uint32 y) {
  (void)y;
  Prims_list__uint32 custard_result = NULL;
  Prims_list__uint32 *custard_dst = &custard_result;
custard_tail:;
  if (cherry_tag(x) == PRIMS_NIL__UINT32) {
    cherry_inc(y);
    *custard_dst = y;
    return custard_result;
  }
  else {
    CHERRY_ASSUME(cherry_tag(x) == PRIMS_CONS__UINT32, "incomplete match in ListAppend.list_append@t");
    uint32_t hd = ((struct Prims_list__uint32_Cons_s *)x)->hd;
    Prims_list__uint32 tl = ((struct Prims_list__uint32_Cons_s *)x)->tl;
    Prims_list__uint32 cherry_tmp2;
    if (cherry_is_unique(x)) {
      cherry_tmp2 = x;
    } else {
      cherry_inc(((struct Prims_list__uint32_Cons_s *)x)->tl);
      cherry_dec_Prims_list__uint32(x);
      cherry_tmp2 = NULL;
    }
    Prims_list__uint32 custard_trmc_v = cherry_reuse_Prims_list__uint32_Cons(cherry_tmp2, sizeof(struct Prims_list__uint32_Cons_s), hd, NULL);
    *custard_dst = custard_trmc_v;
    custard_dst = &((struct Prims_list__uint32_Cons_s *)custard_trmc_v)->tl;
    {
      Prims_list__uint32 _ctail1 = tl;
      x = _ctail1;
      goto custard_tail;
    }
  }
}

Prims_list__uint32 ListAppend_append_u32(Prims_list__uint32 x, Prims_list__uint32 y) {
  CHERRY_MUSTTAIL return ListAppend_list_append__t(x, y);
}

Reference-counted C, specialized to UInt32. Tail recursion becomes a loop, and uniquely owned cells can be reused.

Full file ↓

Proof-oriented programming / F* Proof Copilot

Get started
with an agent.

From a first proof to a whole system. Equip your agent with F* and Pulse skills, then iterate with feedback from F*.

Install. Ask. Verify.

Install Proof Copilot in Copilot CLI or Claude Code. Its F*/Pulse coding agent helps write specifications, implement programs, and repair proof failures.

You choose the goal and review the specification. The agent proposes code and proofs; F* checks them.

Explore Proof Copilot Agent guide

proof-copilot

Copilot CLI

copilot plugin install FStarLang/proof-copilot

Run in your terminal. The F* toolchain is installed separately.

Claude Code

/plugin marketplace add FStarLang/proof-copilot
/plugin install proof-copilot@proof-copilot

Run inside Claude Code. The F* toolchain is installed separately.

Choose your starting point.

Start small.

Use the fstar-coder agent to implement list append and prove that the result's length is the sum of the input lengths. Run F* to check the proof.
Model existing code.

Model this component in F*. Make its assumptions and design invariants explicit. Prove the invariants, or identify where they fail, and explain how the model corresponds to the original implementation.

A proof about the model does not automatically verify the original implementation.
Build your system.

Build this system directly in F*. Define its behavior and design invariants, implement it, and verify that the implementation satisfies the specification. Make assumptions and anything left unverified explicit.

Review the specification
Implement
Verify
Repair
Extract

Review the specification, not just the green check. F* proves the stated contract; intent and assumptions still need human review.

Explore the framework

Go deeper.

Imperative & concurrent / Pulse

Mutable memory.
Precise guarantees.

Own a reference. Borrow another. Multiply by repeated addition, with a proof of the result, freedom from overflow, and termination.

Pulse extracts to raw, standalone C with no reference counting. Concurrent separation logic provides a foundation for manual memory management, safe sharing, and concurrent programs.

Program with Pulse

multiply

Pulse source

fn multiply (x y: ref U32.t)
  preserves live x
  preserves y |-> Frac 'p 'y
  requires pure (U32.fits (U32.v !x * U32.v 'y))
  ensures pure (U32.v !x == U32.v (old !x) * U32.v 'y)
{
  let n = !x;
  let m = !y;
  x := 0ul;
  let mut ctr = 0ul;
  while (!ctr < m)
    invariant live ctr ** live x
    invariant pure (U32.v !ctr <= U32.v m /\
                    U32.v !x == U32.v n * U32.v !ctr)
    decreases (U32.v m - U32.v !ctr)
  {
    x := !x + n;
    ctr := !ctr + 1ul;
  }
}

The fractional permission allows reading y, not writing it. The loop invariant tracks the product.

Full file ↓

OCaml

let multiply_multiply (x : (FStar_UInt32.t ref)) (y : (FStar_UInt32.t ref)) : unit =
  (let n = (!(x)) in
  let m = (!(y)) in
  ((x) := (FStar_UInt32.uint_to_t Prims.int_zero));
  let ctr = (ref (FStar_UInt32.uint_to_t Prims.int_zero)) in
  (while (let u___anf0 = (!(ctr)) in
  (FStar_UInt32.lt u___anf0 m)) do (let u___anf0 = (!(x)) in
  ((x) := (FStar_UInt32.add u___anf0 n));
  let u___anf01 = (!(ctr)) in
  ((ctr) := (FStar_UInt32.add u___anf01 (FStar_UInt32.uint_to_t Prims.int_one)))) done);
  ())

The same verified program, extracted to OCaml.

Full file ↓

F#

let multiply_multiply (x : (uint32 ref)) (y : (uint32 ref)) : unit =
  (let n = ((x).Value) in
   let m = ((y).Value) in
   ((x).Value <- (0u));
   let ctr = (ref (0u)) in
   (while (let u___anf0 = ((ctr).Value) in
           (u___anf0 < m)) do
      (let u___anf0 = ((x).Value) in
       ((x).Value <- (u___anf0 + n));
       let u___anf01 = ((ctr).Value) in
       ((ctr).Value <- (u___anf01 + (1u)))));
   ())

The same verified program, extracted to F# for .NET.

Full file ↓

C

void Multiply_multiply(uint32_t *x, uint32_t *y) {
  uint32_t n = x[0];
  uint32_t m = y[0];
  x[0] = 0;
  uint32_t ctr = 0;
  while (ctr < m) {
    uint32_t __anf0 = x[0];
    x[0] = (__anf0 + n);
    uint32_t __anf01 = ctr;
    ctr = (__anf01 + 1);
  }
}

Raw, standalone C with no reference counting. Contracts and proof steps leave no runtime code.

Full file ↓

Parallel GPU programming / Kuiper

GPU kernels.
With guarantees.

Add two vectors in parallel. The contract specifies every output and leaves both inputs unchanged.

Kuiper builds on Pulse to reason about GPU memory and parallel execution, then extracts to CUDA. Its parallel map assigns each output element to one thread, with disjoint writes.

Explore Kuiper

vector_add

Kuiper source

fn vector_add
  (n : szp { n <= max_blocks * max_threads })
  (a : array1 f32 (l1_forward n) { is_global a })
  (b : array1 f32 (l1_forward n) { is_global b })
  (out : array1 f32 (l1_forward n) { is_global out })
  preserves cpu **
    on gpu_loc (a |-> 'a) ** on gpu_loc (b |-> 'b)
  requires on gpu_loc (out |-> 'old)
  ensures on gpu_loc
    (out |-> mk1 (fun i -> add (acc1 'a i) (acc1 'b i)))
{
  Map.map_gpu2_to add n a b out;
}

Ghost snapshots describe the input values. The proof and snapshots disappear from CUDA.

Full file ↓

CUDA

__global__ __launch_bounds__(1024)
/**
  hoisted when extracting vector_add
*/
static void
__hoisted_vector_add_0(uint32_t n, float *a, float *b, float *out)
{
    if (1024U * blockIdx.x + threadIdx.x < n)
        out[1024U * blockIdx.x + threadIdx.x] =
            a[1024U * blockIdx.x + threadIdx.x] +
            b[1024U * blockIdx.x + threadIdx.x];
}

The extracted kernel: one thread per output, with a bounds check for the final block. The full file includes the host launcher.

Full file ↓

Your language / C with PAL

Verify C code
in place.

Keep your C code and your compiler. Add a contract and a loop invariant; PAL translates the program to Pulse for verification.

Here, repeated addition computes the product without overflow. The annotations disappear in a normal C build.

Explore PAL

multiply.c

C source

uint32_t multiply_by_repeated_addition(uint32_t x, uint32_t y)
  _requires((_specint) x * y <= UINT32_MAX)
  _ensures((_specint) return == (_specint) x * y)
{
  uint32_t ctr = 0;
  uint32_t acc = 0;
  while (ctr < y)
    _invariant(_live(ctr) && _live(acc))
    _invariant(ctr <= y && (_specint) acc == (_specint) x * ctr)
  {
    acc = acc + x;
    ctr = ctr + 1;
  }
  return acc;
}

A mathematical product specification. The precondition rules out overflow; the loop invariant tracks the result.

Full file ↓

Pulse

divergent fn func_multiply_by_repeated_addition
    (var_x: Typedef_uint32_t.ty_uint32_t)
    (var_y: Typedef_uint32_t.ty_uint32_t)
  requires ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
  requires ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
  requires
    (with_pure
      (((id #int (UInt32.v var_x)) * (id #int (UInt32.v var_y))) <=
        (id #int (UInt32.v 4294967295ul))))
  returns return_1 : Typedef_uint32_t.ty_uint32_t
  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
  ensures
    (with_pure
      ((id #int (UInt32.v return_1)) = ((id #int (UInt32.v var_x)) * (id #int (UInt32.v var_y)))))
{
  let mut var_x = var_x;
  let mut var_y = var_y;
  let mut var_ctr : Typedef_uint32_t.ty_uint32_t;
  var_ctr := 0ul;
  let mut var_acc : Typedef_uint32_t.ty_uint32_t;
  var_acc := 0ul;
  while (((!var_ctr) `UInt32.lt` (!var_y)))
    invariant ((live var_ctr) ** (live var_acc))
    invariant (with_pure
        (((!var_ctr) `UInt32.lte` (!var_y)) &&
          ((id #int (UInt32.v (!var_acc))) =
            ((id #int (UInt32.v (!var_x))) * (id #int (UInt32.v (!var_ctr)))))))
  {
    var_acc := ((!var_acc) `Pulse.Lib.C.UInt32.add_wrap` (!var_x));
    var_ctr := ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
  };
  return (!var_acc);
}

The generated Pulse function. Product correctness and overflow freedom are verified; termination is not claimed.

Full file ↓

Your language / C# with PAL-CS

Verify C# code
in place.

Insertion sort, with two guarantees: the result is sorted, and it is a permutation of the input.

Write the contracts in C#. PAL-CS checks them through Pulse. Your annotated program still compiles and runs as ordinary C#.

Explore PAL-CS

InsertionSort.cs

C# source

public static class SortingBySortedness
{
    [Ensures("Contents(a).Length == Old(Contents(a)).Length")]
    [Ensures("SortedSpec.Sorted(Contents(a), 0, Contents(a).Length)")]
    [Ensures("IsPermutation(Contents(a), Old(Contents(a)))")]
    public static void InsertionSort(int[] a)
    {
        for (int i = 1; i < a.Length; i++)
        {
            Pal.Invariant(1 <= i);
            Pal.Invariant(Pal.Contents(a).Length == Pal.Old(Pal.Contents(a)).Length);
            Pal.Invariant(SortedSpec.Sorted(Pal.Contents(a), 0, i));
            Pal.Invariant(Pal.IsPermutation(Pal.Contents(a), Pal.Old(Pal.Contents(a))));

            int key = a[i];
            int j = i - 1;
            while (j >= 0 && a[j] > key)
            {
                Pal.Invariant(-1 <= j && j < i);
                Pal.Invariant(i < Pal.Contents(a).Length);
                Pal.Invariant(Pal.Contents(a).Length == Pal.Old(Pal.Contents(a)).Length);
                // The run below the hole is sorted, ...
                Pal.Invariant(SortedSpec.Sorted(Pal.Contents(a), 0, j + 1));
                // ... the run above it is sorted, ...
                Pal.Invariant(SortedSpec.Sorted(Pal.Contents(a), j + 2, i + 1));
                // ... everything above the hole exceeds the value being placed, ...
                Pal.Invariant(SortedSpec.AllAbove(Pal.Contents(a), j + 2, i + 1, key));
                // ... and the two runs are correctly ordered with respect to each other.
                Pal.Invariant(SortedSpec.Dominated(Pal.Contents(a), 0, j + 1, j + 2, i + 1));
                Pal.Invariant(Pal.IsPermutation(
                    Pal.SetAt(Pal.Contents(a), j + 1, key),
                    Pal.Old(Pal.Contents(a))));
                Pal.Decreases(j + 1);

                SeqLemmas.UpdShiftIsPermutation(a, j, key);

                a[j + 1] = a[j];

                // The four parts of the invariant, re-established one at a time for
                // the narrowed hole. Stating them here rather than leaving them to the
                // solver is the whole job of a proof annotation language.
                Pal.Assert(SortedSpec.Sorted(Pal.Contents(a), 0, j));
                Pal.Assert(SortedSpec.Sorted(Pal.Contents(a), j + 1, i + 1));
                Pal.Assert(SortedSpec.AllAbove(Pal.Contents(a), j + 1, i + 1, key));
                Pal.Assert(SortedSpec.Dominated(Pal.Contents(a), 0, j, j + 1, i + 1));

                j--;
            }
            a[j + 1] = key;
        }
    }
}

Insertion sort with its proof annotations. The full source includes the predicates and sequence lemma.

Full file ↓

Pulse

fn func_SortingBySortedness_InsertionSort (var_a: array I32.t) (#pre_a: erased (Seq.seq I32.t))
  requires A.pts_to var_a pre_a
  ensures  exists* post_a.
           A.pts_to var_a post_a **
           pure (((Seq.length post_a) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted post_a 0 (Seq.length post_a)) /\
           (CS.is_permutation post_a (reveal pre_a)))
{
  let mut var_i = 1l;
  while (
  let t0 = !var_i;
  let t1 = length_i32 var_a;
    (I32.lt t0 t1)
  )
  invariant exists* va_0 vi_1.
           A.pts_to var_a va_0 **
           R.pts_to var_i vi_1 **
           pure ((1 <= (I32.v vi_1)) /\
           ((Seq.length va_0) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted va_0 0 (I32.v vi_1)) /\
           (CS.is_permutation va_0 (reveal pre_a)))
  decreases ((pow2 31 - (I32.v !var_i)))
  {
    let t2 = !var_i;
    let t3 = read var_a t2;
    let mut var_key = t3;
    let t4 = !var_i;
    let mut var_j = (I32.sub t4 1l);
    with vi_3 vkey_5. assert (R.pts_to var_i vi_3 ** R.pts_to var_key vkey_5);
    while (
    let t5 = !var_j;
    let t10 = if ((I32.gte t5 0l)) {
    let t6 = !var_j;
    let t7 = read var_a t6;
    let t8 = !var_key;
      (I32.gt t7 t8)
    } else {
    let t9 = false;
      t9
    };
      t10
    )
    invariant exists* va_2 vj_4.
           A.pts_to var_a va_2 **
           R.pts_to var_i vi_3 **
           R.pts_to var_j vj_4 **
           R.pts_to var_key vkey_5 **
           pure ((((0 - 1) <= (I32.v vj_4)) /\ ((I32.v vj_4) < (I32.v vi_3))) /\
           ((I32.v vi_3) < (Seq.length va_2)) /\
           ((Seq.length va_2) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted va_2 0 ((I32.v vj_4) + 1)) /\
           (spec_SortedSpec_Sorted va_2 ((I32.v vj_4) + 2) ((I32.v vi_3) + 1)) /\
           (spec_SortedSpec_AllAbove va_2 ((I32.v vj_4) + 2) ((I32.v vi_3) + 1) (I32.v vkey_5)) /\
           (spec_SortedSpec_Dominated va_2 0 ((I32.v vj_4) + 1) ((I32.v vj_4) + 2) ((I32.v vi_3) + 1)) /\
           (CS.is_permutation (Seq.upd va_2 ((I32.v vj_4) + 1) vkey_5) (reveal pre_a)))
    decreases (((I32.v !var_j) + 1))
    {
      with va_6 vi_7 vkey_8 vj_9. assert (A.pts_to var_a va_6 ** R.pts_to var_i vi_7 ** R.pts_to var_key vkey_8 ** R.pts_to var_j vj_9);
      Let_SeqLemmas_UpdShiftIsPermutation.lemma_SeqLemmas_UpdShiftIsPermutation va_6 vj_9 vkey_8;
      let t11 = !var_j;
      let t12 = !var_j;
      let t13 = read var_a t12;
      write var_a (I32.add t11 1l) t13;
      with va_10 vi_11 vkey_12 vj_13. assert (A.pts_to var_a va_10 ** R.pts_to var_i vi_11 ** R.pts_to var_key vkey_12 ** R.pts_to var_j vj_13);
      assert (pure ((spec_SortedSpec_Sorted va_10 0 (I32.v vj_13))));
      with va_14 vi_15 vkey_16 vj_17. assert (A.pts_to var_a va_14 ** R.pts_to var_i vi_15 ** R.pts_to var_key vkey_16 ** R.pts_to var_j vj_17);
      assert (pure ((spec_SortedSpec_Sorted va_14 ((I32.v vj_17) + 1) ((I32.v vi_15) + 1))));
      with va_18 vi_19 vkey_20 vj_21. assert (A.pts_to var_a va_18 ** R.pts_to var_i vi_19 ** R.pts_to var_key vkey_20 ** R.pts_to var_j vj_21);
      assert (pure ((spec_SortedSpec_AllAbove va_18 ((I32.v vj_21) + 1) ((I32.v vi_19) + 1) (I32.v vkey_20))));
      with va_22 vi_23 vkey_24 vj_25. assert (A.pts_to var_a va_22 ** R.pts_to var_i vi_23 ** R.pts_to var_key vkey_24 ** R.pts_to var_j vj_25);
      assert (pure ((spec_SortedSpec_Dominated va_22 0 (I32.v vj_25) ((I32.v vj_25) + 1) ((I32.v vi_23) + 1))));
      let t14 = !var_j;
      var_j := (I32.sub t14 1l);
      ()
    };
    let t15 = !var_j;
    let t16 = !var_key;
    write var_a (I32.add t15 1l) t16;
    let t17 = !var_i;
    var_i := (I32.add t17 1l);
    ()
  };
  ()
}

The generated Pulse function, checked against sortedness and permutation specifications.

Full file ↓

Agent-written. Proof-checked.

Built with agents.
Checked with F*.

Human-guided agents build real systems, with F* checking the code against its specifications.

Verified code. Real applications.

F* in Production

Explore Project Everest

In Windows & Azure: EverParse-generated parsers validate messages in the Hyper-V virtual networking stack.
In Firefox: HACL* supplies verified cryptography for Firefox's NSS security engine. · NSS code
In Python: HACL* supplies verified hash fallbacks for hashlib in Python 3.12 and later.
In Linux: HACL* supplies Curve25519 code used by WireGuard in the Linux kernel.
In eBPF for Windows: EverParse-generated validators check IOCTL messages and ELF inputs .
In ElectionGuard: ElectionGuard's C++ SDK uses HACL*'s verified big-integer arithmetic.
In Tezos: HACL* and EverCrypt provide cryptographic primitives for the Octez blockchain implementation.
In Mbed TLS: Mbed TLS integrates HACL*'s verified Curve25519 implementation.

Prove code
correct.

F* source

OCaml

F#

C

Get started
with an agent.

Install. Ask. Verify.

Copilot CLI

Claude Code

Choose your starting point.

Start small.

Model existing code.

Build your system.

Go deeper.

Mutable memory.
Precise guarantees.

Pulse source

OCaml

F#

C

GPU kernels.
With guarantees.

Kuiper source

CUDA

Verify C code
in place.

C source

Pulse

Verify C# code
in place.

C# source

Pulse

Built with agents.
Checked with F*.

Atlas

HACL-Pulse

Pulse Verified GC

AlgoStar

KuiperBench

F* in Production

Prove codecorrect.

F* source

OCaml

F#

C

Get startedwith an agent.

Install. Ask. Verify.

Copilot CLI

Claude Code

Choose your starting point.

Start small.

Model existing code.

Build your system.

Go deeper.

Mutable memory.Precise guarantees.

Pulse source

OCaml

F#

C

GPU kernels.With guarantees.

Kuiper source

CUDA

Verify C codein place.

C source

Pulse

Verify C# codein place.

C# source

Pulse

Built with agents.Checked with F*.

Atlas

HACL-Pulse

Pulse Verified GC

AlgoStar

KuiperBench

F* in Production

Prove code
correct.

Get started
with an agent.

Mutable memory.
Precise guarantees.

GPU kernels.
With guarantees.

Verify C code
in place.

Verify C# code
in place.

Built with agents.
Checked with F*.