iiinova — where your digital self keeps evolving

Nik Swamy @lambdanik.bsky.social · 09/06/2025

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!

010

Nik Swamy @lambdanik.bsky.social · 09/06/2025

With huge thanks to the many contributors to this work, from @msftresearch.bsky.social, Inria, @cmu.edu, and several other institutions.

120

Nik Swamy @lambdanik.bsky.social · 09/06/2025

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...

181

Nik Swamy @lambdanik.bsky.social · 02/06/2025

This was fantastic! Thanks for sharing

010

Nik Swamy @lambdanik.bsky.social · 29/05/2025

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!

020

Nik Swamy @lambdanik.bsky.social · 29/05/2025

* and a verified implementation of DICE Protection Environment, using the CBOR profile

110

Nik Swamy @lambdanik.bsky.social · 29/05/2025

* 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*

100

Nik Swamy @lambdanik.bsky.social · 29/05/2025

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

100

Nik Swamy @lambdanik.bsky.social · 28/05/2025

The paper includes a verified implementation of a task pool in the style of OCaml 5 #fstarlang #ocaml

030

Nik Swamy @lambdanik.bsky.social · 28/05/2025

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...

fstar-lang.org

Pulse: Proof-oriented Programming in Concurrent Separation Logic — Proof-Oriented Programming in F* documentation

120

Nik Swamy @lambdanik.bsky.social · 28/05/2025

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...

fstar-lang.org

140

Nik Swamy @lambdanik.bsky.social · 24/05/2025

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...

fstar-lang.org

Fun with Typeclasses: Datatypes a la Carte — Proof-Oriented Programming in F* documentation

042

Nik Swamy @lambdanik.bsky.social · 18/04/2025

way too much shit around here

010

Nik Swamy @lambdanik.bsky.social · 18/04/2025

ok, ok, fine ... i should let my own grumpiness pass : )

110

Nik Swamy @lambdanik.bsky.social · 17/04/2025

Come on! Beautiful gentle yaanai v colonial demagogue??

130

Nik Swamy @lambdanik.bsky.social · 06/04/2025

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/

fmindia.cmi.ac.in

Verification Seminar Series

162

Nik Swamy @lambdanik.bsky.social · 20/03/2025

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!

030

Nik Swamy @lambdanik.bsky.social · 08/03/2025

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!

120

Nik Swamy @lambdanik.bsky.social · 08/03/2025

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 : )

110

Nik Swamy @lambdanik.bsky.social · 02/03/2025

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.

010

Nik Swamy @lambdanik.bsky.social · 02/03/2025

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!

1111