namin

7 ms·

1.
LemmaScript: A Verification Toolchain for TypeScript via Dafny(midspiral.com)
4 points by namin 5mo ago|0 comments
2.
Show HN: LemmaScript, a verification toolchain for TypeScript via Dafny(github.com)
5 points by namin 5mo ago|0 comments
3.
Show HN: Guardians – Verify tool-using agent workflows before execution(github.com)
8 points by namin 5mo ago|0 comments
4.
by namin 6mo ago
Thanks, we will provide case studies. Already today, lemmafit doesn't need familiarity with Dafny. It is used under the hood, so you just use Claude Code normally and lemmafit adds the verification harness. You don't need to inter
5.
by namin 6mo ago
Since around Opus 4.5, systems like Claude Code are very good at Dafny proofs. They don’t get everything right in one shot but can iterate with verifier feedback. Some proofs take over 20 minutes to complete. The system knows to put tempora
6.
by namin 6mo ago
Hey HN! We've been experimenting with Dafny formal verification in web apps. We've been using AI to write verified state machines, proving undo/redo preserves invariants, verifying business logic, and creating apps with this
7.
Show HN: Lemmafit: Make agents prove that their code is correct(github.com)
7 points by namin 6mo ago|5 comments
8.
by namin 7mo ago
Ha. At least you can check the theorem statements and see that the proofs verify :)
9.
A Very Small SAT Solver (From Haskell) Now in Dafny, Proved Correct with LLMs(github.com)
4 points by namin 7mo ago|2 comments
10.
Verifying State and Reconciliation in Collaborative Web Apps(midspiral.com)
3 points by namin 8mo ago|0 comments
11.
Show HN: Henri: a small, hackable agent CLI(github.com)
4 points by namin 8mo ago|0 comments
12.
Show HN: Holey: Staged execution from Python to SMT for synthesis(github.com)
4 points by namin 8mo ago|0 comments
13.
Building a React App with Formally Verified State(midspiral.com)
3 points by namin 9mo ago|0 comments
14.
From Intent to Proof: Dafny Verification for Web Apps(midspiral.com)
5 points by namin 9mo ago|0 comments
15.
by namin 11mo ago
Harvard SEAS | https://metareflection.seas.harvard.edu and https://namin.seas.harvard.edu | Postdoctoral Fellow | Greater Boston Area | ONSITE I am looking for a postdoctoral fellow interested in the intersection of
16.
Show HN: Tiny Hoare logic verifier using SMT(github.com)
12 points by namin 1y ago|1 comments
17.
Show HN: Live software archaeology of FOL (theory of reasoning)(io.livecode.ch)
3 points by namin 1y ago|0 comments
18.
Work with Apps on macOS(help.openai.com)
5 points by namin 2y ago|0 comments
19.
A Scalable Communication Protocol for Networks of Large Language Models(agoraprotocol.org)
3 points by namin 2y ago|0 comments
20.
by namin 2y ago
Harvard SEAS, ONSITE (Boston area, MA, US) I have one opening in a new project around AI for precision medicine. One thrust is about combining biomedical knowledge graphs and large language models into a biomedical-fluent core platform. Ano
21.
Arc Prize Guide(arcprize.org)
7 points by namin 2y ago|1 comments
22.
by namin 2y ago
Awesome, thank you! I'll check it out.
23.
by namin 2y ago
This seems cool! Is there a way to try it locally with an open LLM? If you provide a way to set the OpenAI server URL and other parameters, that would be enough. Is the API_URL server documented, so a mock a local one can be created? Thanks
24.
Show HN: Verified Multi-Step Synthesis Using LLMs and MCTS(arxiv.org)
1 points by namin 3y ago|0 comments
25.
by namin 3y ago
Not dumb! The verifier lets slide an error on the last line, while it's still in progress.
26.
by namin 3y ago
Yes. The verifier check already ensures syntactic correctness, but the search could goes faster if the underlying LLM doesn't generate bad syntax to begin with.
27.
by namin 3y ago
> How does the MCTS distinguish between 'generated a stupid lemma that is true' and 'generated a valid lemma'? It does not, though I would like to add validation as part of the check as future work. > Is there any
28.
by namin 3y ago
Interesting! Is the end goal similar to the outlines library: https://github.com/outlines-dev/outlines ?
29.
by namin 3y ago
Thanks. I adapted this old MCTS library: https://github.com/ImparaAI/monte-carlo-tree-search which is also very short and understandable.
30.
by namin 3y ago
Thanks for taking a look! This is not the main loop. This just generates one completion that succeeds (or gives up) deferring to the Dafny checker to decide. The main loop is the simulate function of the MCTS library. https://git

More ›