Project Everest produced provably correct and secure software in F*, now running in systems like the Windows kernel, Hyper-V, Linux, Firefox, Python, and several others

A new paper describes our experiences, some lessons learned, and possible paths ahead: project-everest.github.io/assets/evere...

PulseParse & EverCBOR

Uses F* and Pulse to formalize several new standards for secure data formats and attestations, including CBOR, CDDL, and COSE, producing verified libraries and compilers.

arxiv.org/abs/2505.17335

#fstarlang #pulse #everparse #rust #cbor #cddl #cose #dice #dpe

PulseCore @ PLDI 2025: A concurrent separation logic in F*, with impredicative invariants, higher-order ghost state, and later credits like Iris, but with a semantics in dependent types based on Indirection Theory, rather than through a categorical semantics.
fstar-lang.org/papers/pulse...

On a flight to ICSE a few weeks ago, I coded up Wouter Swierstra's extremely cool and classic Data Types a la Carte in F*, adding proofs of termination and correctness.

I wrote up a chapter in the Proof-oriented Programming in F* book describing it today:

fstar-lang.org/tutorial/boo...

On Tuesday, I'm giving a talk and demo of Pulse, a separation logic DSL in F*.

Talk abstract with zoom link etc:
fmindia.cmi.ac.in/vss/

Towards Neural Synthesis for SMT-assisted Proof-oriented Programming

wins an ACM SIGSOFT Distinguished Paper Award at ICSE '25

arxiv.org/abs/2405.01787

Excited for all the progress up ahead in AI-assisted program proof!

Massive parenting win today, working with my 10-year old to derive Newton's equations of motion (uniform acceleration, straight line). Then using it to time some dropped stones and estimating that the height of the Ravenna foot bridge from the handrail to the creek below is about 29m.

I often hear from my musician friends: "Don't trust an algorithm".

Makes me sad to realize how much the word "algorithm" has come to just mean an "automated recommendation system".

We need to take it back!