Post

Zicklag
@zicklag.dev

Here it is! The blog post about @quint-lang.org that I've been trying to get out since Friday. 😄 It gives an overview of the kinds of formal methods I know of, as well as my recent experiences using Quint to design the arbiter service we've been working on.

zicklag.leaflet.pubModeling Software With QuintI believe having good abstractions is key to writing good code. But as a coder, I often write code in an effort to find those abstractions…

5 reposts26 likes

Sam Hart
@hxrts.bsky.social

Nice post! I’ve also been playing with both Quint and Lean a bunch recently. Feels like the biggest gap is going from correct model -> correct production code. I’ve spent more time closing this gap than on verification. Curious if you’re in a similar boat.

Zicklag
@zicklag.dev

I haven't gotten to that step yet, other than giving model-based testing a try real quick. I'll most-likely have a follow-up post once I get further into things.

Erlend Sogge Heggen
@erlend.sh

We agree with this prognostication by @martin.kleppmann.com Instead of forcing too much of our code into plain-English and risk eroding our more deeply systemic understandings, we adopt a practice of ongoing architectural formalization, a meet-halfway language for the human and computer.

Martin Kleppmann@martin.kleppmann.com

New blog post! ✨ I argue that AI will make formal verification go mainstream. martin.kleppmann.com/2025/12/08/a... Three reasons for this: 1. LLMs are getting increasingly good at writing proofs using proof assistants. This will make formal verification vastly cheaper than it's been to date.

martin.kleppmann.comPrediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog