Lasm's 294 theorems stayed green when we broke unfollow. So did the API suite

Lasm compiles Lean 4 to WebAssembly so you can write a web app in Lean and prove things about it. Its Show HN went up last week, and its flagship example is Conduit, the RealWorld Medium clone, with 294 proved theorems. The author's stated goal is "to be able to delete much of my test suites and replace them with Lean theorems" (lastmjs). Our view: the proofs are real and the README is the most honest one we have read on this kind of project, but the layer it lists as trusted is exactly where a one-line bug gets through both the theorems and the test suite. Keep the tests there, and make them sharper.

What Lasm proves, in its own words

PROOFS.md is precise. The endpoint code is written against a store interface, and the proofs run it against a model: "the tables as Lean lists (DB), and for each SQL statement a named function that does to the lists what the statement does to the tables."

One of the 50 propositions is others_untouched: "after any request from me (or from nobody), other users' rows, articles, follows and favorites ... are still there unchanged". That is a strong, useful property for a social app.

The same file has a section titled "What is trusted, not proved". First on the list: "The SQL. Each statement in Server/Sql.lean is assumed to do what its model in Proofs/Model.lean does." It adds that "the official API suite exercises them". So the claim on the SQL rests on that suite.

The run

We cloned Lasm at commit 464d4c9 (1 November), installed Node 24.22.2 and built Conduit with @lasm/cli 0.3.6. On the unmodified code, both checks pass:

npm run proofs
npm test

50 propositions and 294 theorems checked; PROOFS.md, SPEC.md and the stated counts agree (30 s).
RealWorld API tests (node): 13/13 files, 154 requests, all passed

Then we made one-line changes to Server/Sql.lean, one at a time, rebuilt the server, and ran both again. The first drops half of a WHERE clause in unfollow:

   unfollow a b := do
-    discard <| db.run "DELETE FROM follows WHERE follower = ? AND followed = ?" #[toJS a, toJS b]
+    discard <| db.run "DELETE FROM follows WHERE followed = ?" #[toJS b]

Now when one user unfollows someone, every follower of that person is removed. That breaks others_untouched in the running app. The second change does the same to unfavorite. The third swaps follower and followed in the feed query.

To confirm the first row is a real bug and not a quirk of the suite, we drove it by hand: three users, two of them follow the third, and one unfollows.

== original build
before: ben follows celeb = True
ana DELETE /follow -> 200
after:  ben follows celeb = True
== M1 build
before: ben follows celeb = True
ana DELETE /follow -> 200
after:  ben follows celeb = False

Ana's unfollow returned 200 and silently removed Ben's follow.

Why the proofs could not see it

They are not meant to. The lakefile puts the SQL in a separate Server library, and npm run proofs builds Conduit and Proofs. Its log after our change says "Build completed successfully (34 jobs)" without compiling the file we edited. The theorem about other users' follows is true of the model's removeFollow, which filters out exactly one pair. The statement that runs was no longer that model.

That is the boundary the README describes, so this is not a hidden flaw. The surprise is the other half: the API suite "exercises" the SQL, and exercising is not the same as checking it. In the RealWorld suite, no second user ever follows or favorites the same target. A DELETE that removes too much therefore looks identical to one that removes the right row.

What it verifies, and what it misses

• Verifies: endpoint logic against the model. That covers authorization, idempotence, pagination, slug uniqueness and JSON round trips, for every input rather than sampled ones. That is more than most web apps can say.
• Verifies, by testing: each SQL statement's single-user happy path, through the official suite.
• Misses: whether each SQL statement matches its model when more than one user's rows are in the table. In our run, that let two of three one-line changes through.

The cheap fix uses what Lasm already has. Run the model and the real SQLite store side by side on the same random sequences of requests, with several users, and compare the tables after each step. The model is executable Lean, so it can serve as the test oracle for the code it was written to describe.

Caveats. Three mutations of our choosing on one example app, not a survey. We did not run the Playwright suite, the other platform bindings or proofs:paranoid. The project states that the SQL is trusted, and we are reporting the size of that trust, not a defect in the proofs.