Functional programming language with effects
Semiautomated verification system using SMT
Interactive proof assistant based on dependent types
Microsoft Research, Inria Paris, MIT, Rosario, …


Variant of dependent type theory
Recursion and semantic termination check
Refinements
x:t{p}
Pure t pre post
Subtyping and subeffecting, Extensional equality
type st (mem:Type) (a:Type) = mem > Tot (a * mem)
total reifiable new_effect {
STATE_m (mem:Type) : a:Type > Effect
with repr = st mem;
return = fun (a:Type) (x:a) (m:mem) > x, m;
bind = fun (a b:Type) (f:st mem a) (g:a > st mem b) (m:mem) >
let z, m' = f m in g z m';
get = fun () (m:mem) > m, m;
put = fun (m:mem) _ > (), m }
total reifiable new_effect STATE = STATE_m heap
Hoare logic style pre and postconditions
let incr () : ST unit (requires (fun n0 > True))
(ensures (fun n0 _ n1 > n1 = n0 + 1))
= let n = STATE.get() in STATE.put (n + 1)
Pre and post conditions are just syntactic sugar for WPs
WPs computed generically for all effects
relies on a monad on predicate transformers (Dijkstra monad)
we now obtain this for free by selective CPSing effect definition
STATE.repr t = mem > t * mem
STATE.wp t ~= mem > (t * mem > Type0) > Type0
Monadic reification
STATE.reify : (St a) > Ghost (nat > Tot (a * nat))
Allows us to give weak specification to an effectful function
let incr () : St unit = let n = STATE.get() in STATE.put (n + 1)
and prove lemmas about reification of effectful computation
let incr_works (n:nat) : Lemma (snd (STATE.reify (incr()) n) = n + 1) = ()
Reduces “relational” effectful verification to pure verification
F* tactics written as effectful F* code (inspired by Lean, Idris)
have access to F*'s proof state (and can efficiently roll it back)
can introspect on F* terms (deep embedding, simply typed)
can be interpreted by F*'s normalizer or compiled to OCaml
userdefined, nonprimitive effect: proof state + exceptions monad
noeq type __result a =
 Success of a * proofstate
 Failed of string //error message
* proofstate //the proofstate at time of failure
let __tac (a:Type) = proofstate > Tot (__result a)
reifiable reflectable new_effect {
TAC : a:Type > Effect
with repr = __tac ... }
let tactic (a:Type) = unit > Tac a
Arithmetic expression canonizer (Guido)
Bitvectors in Vale (Nick G, Nik S, and Chris H)
Separation logic (Monal and Aseem, ongoing)
Pattern matcher (Clément, ongoing)
upcoming case studies will probably include:
Improve tactics, balance automation and control
Better treatment of effects: Dijkstra monads for free v2
Studying more effects: probabilities, concurrency, …
Effect masking: hiding exceptions, state, divergence(!?), …
Verified interoperability: F* (OCaml) + Low* (C) + Vale (ASM)
Further work out metatheory and selfcertify core typechecker
Join the team at Inria Paris and Microsoft Research