Shaw

Rewriting slop.cash with stricter PRD, formal specification with Quint and verification with Lemmascript

Requiring it in AGENTS.md, CONTRIBUTING.md and README

Already found a few state issues and bugs, very promising

I think these are going to be important guardrails for all future projects

Looks like @finnbags is back in the game

X money for creator fees is a good mechanic

Run it fam

That was crazy

TLA+ has been incredibly useful, even on brownfield project, for turning implicit state machines into explicit specs where the entire flow can be tested and verified.

There is a deep relationship between user journey, UX flow and formal specification that has an enormous amount of value to slop code.

I wanted something more programmer-y and Typescript-y, and I came across Quint. It's highly agent friendly and seems to be maximally useful for this new paradigm of programming.

github.com/quint-co/quint

Quint is high level, like TLA+, and doesn't formalize Typescript functionality. So underneath that, lower level, is Lemmascript.

lemmascript.org

This lets you markup your Typescript with contracts.

The combination of these two things makes Typescript feel more like a compile time checked language, more verifiable, stronger guarantees, and it finds different kinds of bugs than AI generated unit tests seem to.

It's not a magic bullet but damn it does seem to improve code quality a lot.

And the agents can rapidly iterate against it.

I think we're gonna see a lot more of this kind of thing popping up, especially in interpreted languages like TS and Python.

I'd recommend using Quint when you're just modeling your application and flows (although I've been installing it into an existing project with good results) and then telling your agent to add Lemmascript in the build phase.

Now the real work begins