Hey there,

For the Claude Code Hackathon (which we sort of unexpectedly got into last week), Nada built a nifty little tool that helps narrow the gap between the guarantees we’re claiming to make and the guarantees we intended to make.

Building a verified AI programming workflow requires us to nail down two concepts:

1. The AI has to prove that the code it wrote is correct (we can do this already)
2. The guarantee we get from that proof has to match what we wanted to guarantee in the first place (the intent gap)

We have tackled this second challenge from a few promising angles, and this past weekend, we explored another: a small tool that uses LLMs to informalize lemmas back to English (without seeing the original requirement), then compares the two to flag disputes.

You can read about it here.

claimcheck is open; you can play with it. And please hit reply if you have thoughts — we appreciate the feedback.

Til next time,
~fernanda

PS: We’ll be opening a waitlist for our product, lemmafit, soon. Look out for an email about that.

TL;DR: install → init → Claude writes code correctly — guaranteed.

Github | LinkedIn