Thomas Leonard's blog

RSS

Blog
Archives
About Me

Category: tla

2026

Proving liveness with TLA

Jan 01 2026

posted in tla

2019

Using TLA+ to understand Xen vchan

Jan 01 2019

posted in mirage, ocaml, qubes, tla, xen

Open Source software developer, with interests in distributed systems and security. [ more ]

@talex5@mastodon.social

All articles on this blog are written by hand, without the use of LLMs.

Recent Posts

Linux input devices (with libinput-ocaml)
Proving liveness with TLA
Linux mode setting, from the comfort of OCaml
Vulkan graphics in OCaml vs C
Investigating Linux graphics

Copyright © 2026 Thomas Leonard
NO AI TRAINING: Without in any way limiting the author's exclusive rights under copyright, any use of this publication to "train" generative artificial intelligence (AI) technologies to generate text is expressly prohibited. The author reserves all rights to license uses of this work for generative AI training and development of machine learning language models.