And especially to Chris Brzuska, Aymeric Fromherz, Markulf Kohlweiss, Guido Martinez, Bryan Parno, and @protz.bsky.social: it was fun reflecting on the work and writing this paper together!
With huge thanks to the many contributors to this work, from @msftresearch.bsky.social, Inria, @cmu.edu, and several other institutions.
Project Everest's architecture
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...
This was fantastic! Thanks for sharing
If you're building security-critical components in embedded systems, secure boot loaders, device attestation components, software bill of materials, etc.: Use our formally verified, high-performance code!
* and a verified implementation of DICE Protection Environment, using the CBOR profile
* a verified compiler for CDDL specifications, yielding either verified C or verified safe Rust code, for parsing and serializing CBOR objects according to a CDDL schema
* a verified implementation of COSE_Sign1, again in C or Rust, using verified cryptography from HACL*
Including:
* a formalization of multiple RFCs, with mechanically checked proofs of correctness and security.
* a library in verified C and in verified safe Rust for validating, parsing, and serializing CBOR objects
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
The paper includes a verified implementation of a task pool in the style of OCaml 5
#fstarlang #ocaml
PulseCore is the foundation for Pulse, an embedded language in F* for proof-oriented programming with dependent types & concurrent separation logic.
fstar-lang.org/tutorial/boo...
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...
way too much shit around here
hahahahahaha
ok, ok, fine ... i should let my own grumpiness pass : )
Come on! Beautiful gentle yaanai v colonial demagogue??
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!
A most gratifying recent moment was a sequence of puns related to knitting towards the end of Asterix in Corsica, which I had never picked up on, but kid (who knits) picked up on instantly and explained to me!
We read them all too, and obsessively re-read them, appreciating more of the puns & allusions each time. That too my old, battered versions of the albums from the 80s which my mom found : )
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!
