AI is now writing tons of the code that gets pushed to production. As code generation gets cheaper, verification becomes the bottleneck. We believe in a future where every piece of software comes with a mathematical proof that it does what its author intended - in doing so, eliminating many classes of exploits. Talos is part of the foundation for that.
Talos provides a Wasm interpreter optimized for reasoning at the binary level, together with a weakest-precondition calculus layer for proving properties about programs. Because we reason directly about WebAssembly, any language with a Wasm backend is in scope: Rust, C++, Go, C, Swift, Kotlin, Zig, C#, and many more.
To make this possible, we use Lean: a programming language and theorem prover that lets you both write software and mathematically prove that it's correct - all in one system. That's what lets Talos double as both an executable interpreter and the formal object Lean reasons about. Lean also integrates with modern AI proving tools, discharging goals automatically via both proof search and direct evaluation.
To see Talos in action check out a proof for Stein's GCD algorithm, implemented in the popular Rust crate num-integer: https://github.com/cajal-technologies/talos/blob/main/progra....
Our roadmap:
- Full Wasm coverage by first passing the official W3C testsuite, then later verifying against SpecTec (formal Wasm spec) - Arbitrary crate verification - any Rust crate that compiles to Wasm should be in scope - Building our proof library codelib, to make verifying increasingly complex programs tractable
We would love to hear the community’s feedback on Talos and comments on the state of formal verification right now. Contributions are also welcome!
It supports Markdown and HTML, stable URLs, renaming, republishing to the same URL, and watch mode for continuous updates to same file. It is MIT licensed.
The main design choice is that there is no hosted Pagecast account. It uses your Cloudflare account and deploys there directly and has claude code and codex integrations as skill/hooks.
Basically it can be used as a replacement for codex sites or claude artifacts
Until now Skills have basically been locked to closed models, and with the ability to have private, local intelligence becoming increasingly important, but this feature allows you to do XYZ with local models.
It's fully compatible with OpenAI's /v1/skills API, so you can drop mistral.rs into your existing code with minimal difficulty.
We support the accompanying tools too: /v1/files or input_file for attaching files to your prompts, and mistral.rs also allows models to send generated files back using the OpenAI-compatible method.
It's also easier than ever to try mistral.rs: we are including prebuilt binaries for NVIDIA CUDA, Apple Silicon, and CPU! # Linux/Mac > curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/EricLBuehler/mistral.rs/ma... | sh # Windows > irm https://raw.githubusercontent.com/EricLBuehler/mistral.rs/ma... | iex
Then: mistralrs serve --agent --isq 4 -m google/gemma-4-E4B-it
Super excited for you to try this out and any feedback! Do you have any suggestions for what you would like to see in the next releases?
Check out the GitHub: https://github.com/EricLBuehler/mistral.rs Docs & Quickstart: https://ericlbuehler.github.io/mistral.rs/
crawlie fixes that! It's 100% free, it's local-first, it's agent-native (MCP baked in!), and every issue it finds comes with why it matters and how to fix it.
The idea came from an emerging family dynamic I kept noticing. My daughters (A, 9 and J, 8) are becoming increasingly independent, but as parents, we hold an enormous amount of invisible state in our heads and phones: what day a project is due, who needs cleats, what's for lunch, which kid has library day, what chores need to happen before screens, how many days until the camping trip, what Grandma wanted them to know, what changed after school, etc.
Kids live downstream of that system, and their experience of it is repetitive nagging:
"Brush your teeth." "Pack your folder." "Don't forget your cleats." "Don’t forget your water bottle." "Did you pack your cleats?" "Please pack your cleats."
Even if the tone is kind, the repetition makes it feel like a nag. And all of the information is trapped behind screens, which isn't great if you're trying to limit your kids' screen time, all while trying to give them more ownership in the process.
Attagram tries solve for that. It turns that invisible family state into a small daily artifact a kid can own.
Every morning, the printer wakes up and prints a parent-curated morning edition newspaper. It has sections like: today’s plan, a todo list, a countdown to an event, a joke, a riddle, a note from a grandparent, and lots more. It's something kids can tear off, pin to their bulletin board, shove in their pocket, or punch through a spike.
All of this is managed through, yes, an app. BUT! The app is for the parents. Its job is to be the best in the world at turning family logistics, rituals, and affection into a screen-free paper experience. The paper remains the hero, and how a kid experiences Attagram.
Technically, Attagram is pretty simple. It uses off-the-shelf parts to connect to a cloud service so daily digests can be generated and printed at scheduled times. It also allows trusted family members to send one-off notes as needed. The magic is in the experience overall and how it feels to hold the paper in your hands.
This is my first hardware project, and as a software person, I have really appreciated (and respected) how much there is to learn. It's a lot of work to make sure this product is perfect on day one, because there's no easy way to update hardware. Software is so forgiving!
We have a nationwide private beta program in homes now, and the feedback has been really positive. More than one family has told me that their kids park themselves in front of the printer each morning, waiting for it to print at the scheduled time. I'm planning to ship a few more units for free to really ensure we're getting all the input we can before going into more scaled production. If you think you'd be interested in one, drop me a line at [email protected].
Our modest plan is to reach 100 paid reservations before scaling manufacturing, partly to test whether strangers actually want this enough to pay rather than just say "cute idea." https://www.attagram.com/order
I’d value HN's experience on:
1. Industrial design: what stands out as being "bad design" in the current iteration? Also, if this is something you'd want to work on, I'd love to chat!
2. Mechanical engineering: what are the best ways to "harden" a device like this so it's reliable, but easy to manufacture. Also, if this is something you'd want to work on, I'd love to chat!
3. Manufacturing: when do you engage with a contract manufacturer in China? What do you try to avoid? Also, if this is something you'd want to work on, I'd love to chat!
4. HN Parents: is this something you could see yourself buying, or it just cute? If the former, but you wouldn't pre-order, why not?
Glassboard let's you draw over anything on your Mac, across every app and every screen, Khan-academy style!
Hold a keybind and draw. Release and it fades away. That's all! (well, except colors, shapes, a radial menu switcher and keybinds galore). But the basic concept is simple hold, draw, release, continue presenting without losing flow.
Made for frequent screensharers and content creators.
No more wiggling my mouse pointer at what I want to highlight while screensharing.
Try it at https://stem.ps/glassboard. It's completely free and will stay that.
I'd like to share our DOCX plugin for Cowork and Codex.
It uses 2-5x fewer tokens compared to the traditional docx skill because it doesn't write any code nor execute python/node script. It is also much more reliable.
Our DOCX plugin converts docx<->html bidirectionally. This means AI only operates on HTML. AI is excellent and very efficient when it comes to HTML.
Most libraries (if not all) support docx->html, but none supports html->docx. This is what is novel about our approach.
Here's the demo: https://drive.google.com/file/d/1UNlUJYwkNX3NiANDkLLb3UoRSms...
We've been using it in-house for redlining legal documents, and we love it. If you redline docx files, please give it a try: https://github.com/LegalRabbit-AI/legalrabbit-docx-claude-pl...
v2 is a new version that improves the calculations accuracy by 5x for the Sun and by 20x for the Moon, verified by an extensive test harness vs ground truth from US Naval Observatory, in addition to fixing a ton of issues and modernizing the distribution with ESM. Hope you enjoy it.
As in, the puzzle does not have a unique solution using sudoku logic alone. You must use one of two forms of hidden word logic to finish the puzzle. 1) Deduce where a word must be placed and add letters, or 2) deduce where a word may not be placed and restrict letters. To keep it more sudoku like and aid in solving, every row, column, and box has at least one letter of a found word.
In playtesting I thought it was fun, although at times very difficult for me (I'm not an expert sudoku player), so I thought I'd build it out to share.
The puzzles are generated by creating racks of 9 unique letters, finding all words that can be made with those letters, generating sample grids, finding the words in them, throwing out candidates that don't fit the word placement criteria, then carving the board by removing letters until two constraints hold: we have >=2 solutions by sudoku logic and exactly 1 solution when the word search logic is added. Overall about 60000 puzzles are generated and thrown out for every sound one.
I used Claude pretty extensively for the code, which includes:
- Puzzle generator - Puzzle solver - Puzzle explainer - Static website (Cloudflare) - Online puzzle player (local storage) - Online static puzzle walkthrough - Print book layouts - PDF layouts
Overall, it's been a lot of fun to focus on for a few weeks.
This is a tool for profiling eBPF programs themselves, probe->kernel activity, interactions with shared hash maps, etc.
Since eBPF programs are pieces of machine code residing in (kernel) address space, you could profile them with standard perf just like any other kernel function. However, perf alone won't show you other useful metrics like number of executions and average eBPF program runtime, like bpftop does. Also, I want an easy way to map CPU samples to original source code lines, where possible.
I wanted to unify both approaches, display the bpftop-style call count & probe latency, with the ability to drill down inside where the eBPF program spends most of it's time.