The recent (and well-deserved) TLA+ attention motivated me enough to refresh my 20-year-old Haskell code that parses, pretty-prints, and evaluates TLA+ specs and expressions. Enjoy, copy, transcribe to other languages, etc. Maybe you too find it useful: github.com/ret/specifica
reto retweeted
I'm happy to announce Thales, a TypeScript compiler and JS engine in Lean. Thales compiles a subset of TypeScript to Lean via a shallow embedding. I'm building a bridge for TS programmers into Lean's program verification toolset. Check out github.com/jessealama/thales to get started.
reto retweeted
Our AI theorem prover has just got a lot more powerful. Please give it a spin!
This quoted post is unavailable.
reto retweeted
AI is writing a growing share of the world's software. No one is formally verifying any of it.
New essay: "When AI Writes the World's Software, Who Verifies It?"
leodemoura.github.io/blog/20…
reto retweeted
The CSLib steering committee recently announced the official launch of CSLib — an open-source effort to formalize computer science in Lean, inspired by the impact of Mathlib in mathematics.
CS researchers, practitioners, and enthusiasts are invited to get involved to support formalizing essential computer science concepts, and building infrastructure for reasoning about real-world code with Lean.
Learn more at:
🌐 cslib.io
📄 White paper: arxiv.org/abs/2602.04846
🤝 Contribute: github.com/leanprover/cslib/…
#LeanLang #LeanProver #CSLib #OpenSource #FormalVerification
reto retweeted
I wrote an essay on proof assistants in the age of AI.
leodemoura.github.io/blog/20…
Arrived just in time for the weekend 👓… Thanks for putting the work into this @bml_khubbard!
reto retweeted
I created a short video about how Arch (the intelligent proxy for agents built on Envoy) can help with intent routing for smarter retrieval, guardrails for safety, and function calling for agent personalization via simple @FastAPIs. Of course, @Gradio is our natively integrated chat interface, and you can select from @MistralAI and @OpenAI LLMs for summarization (more coming soon)
reto retweeted
1. Richard Bird, code as poetry.
2. Mike Burrows, absolute mastery of low level code.
3. Jeff Dean, planet-scale coding.
4. Niklas Wirth, frugality and precision in language design.
5. Lennart Augustsson, utter genius at coding anything.
reto retweeted
Rust Foundation Collaborates With AWS Initiative to Verify Rust Standard Libraries
foundation.rust-lang.org/new…
