I’m excited to announce the emergence from stealth of &Truth, PBC, the company I’ve been building for the past few months with my co-founders Chris Hsu and @ilyasergey.  Come see what we are up to: andtruth.com.

I'm thrilled to bring &Truth out of stealth as its co-founder and Chief Science Officer. With a team I'm proud to be part of, we're setting out to specify and prove all the world's software correct and secure.

If you geek out over code people can understand and trust, join us!

We are out of stealth! As AI writes more code, we're building tools to prove programs meet precise requirements, with Lean proofs anyone can independently check. Let's make verified software the norm in every language and application.

Come take a look: andtruth.com

🤔 Can VLA models teach themselves the best way to reason?

We introduce R&B-EnCoRe which is a self-improving pretraining cycle for reasoning VLAs to propose and self-discover what embodiment-specific reasoning looks like.
🔗 milanganai.github.io/rnb-encore
📃 arxiv.org/pdf/2602.08167

test-time compute [ttc] in robotics isn't free & isn't always worth it. smart allocation of ttc recovers frontier-level planning at a fraction of the cost!

coauthor @milanganai
w/ Yasmina @ajaysridhar0 Mozghan @katielulula Clark Barrett @jiajunwu_cs @chelseabfinn @drmapavone 🧵

What if we could mathematically prove that code does what it's supposed to do, not just test it and hope?

The Caltech AI Alignment Group hosted @ClarkBarrett7 from @Stanford for a talk on CSLib, a platform for AI-assisted formal verification in Lean, and why proving code correct most urgent problems in AI safety.

1/7

Congratulations to the entire CVC4/cvc5 team for winning the Rance Cleaveland Test-of-Time Tool Award at ETAPS this week!
etaps.org/awards/test-of…

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 omputer 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/csl…

#LeanLang #LeanProver #CSLib #OpenSource #FormalVerification

🥁And the #cav24 Award goes to...🥁
Clark Barrett @Stanford, David Dill @Stanford, Kyle Julian @Wing, Guy Katz @CseHuji and Mykel Kochenderfer @aiprof_mykel @Stanford for their #cav17 paper “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”
Congratulations! 👏

How can we train a language model to communicate with other agents? We propose informativeness as a training objective, where a sender's message is informative insofar as it increases the receiver's log probabilities over future observations conditional on the message. (1/8)

Are you ready for @eulerfinance's ✨$1.25M✨ audit competition on @cantinaxyz?

We're thrilled to announce that $100k of the total pot is being allocated to formal verification managed by @certora 🔥

Check out our new blog post by Alex Ozdemir on adding a new theory solver: cvc5.github.io/2024/01/26/add…

We're looking to get to know the users of SMT solvers! Please DM us if you use any SMT solver, and especially if you use cvc5. Reposts for visibility are also appreciated!

Generating and Exploiting Automated Reasoning Proof Certificates | Communications of the ACM dl.acm.org/doi/10.1145/35…

Just participated in a fun podcast hosted by @joe__scott__ in which we discuss automated reasoning and my research. Check it out: youtu.be/RVjQkUI0kcw

Congratulations to the cvc5 team. 1.0 release yesterday, and best tool paper award at ETAPS today.

Coming soon...cvc5
facebook.com/cvc4smtsolver/…