UX Engineer @Microsoft | creator of those easing functions | building next-gen motion & graphics tools | formal verification, Lean, Dafny, Bend2
Brooklyn, NY
Joined October 2008
- Tweets26.6K
- Following2.4K
- Followers10.4K
- Likes81.5K
Pinned Tweet
I'm building a motion curve editor beyond your wildest fantasies.
I've been head down solving new easing equations for the last 13 months.
I promise nothing less than a quantum leap in easing technology.
Vulnerability on @telegram seems like their new widgets can have executable payloads
Stay safe, share to raise awareness.
nitter.gq/RouterHubSI/status/212…
Today one of our users reported getting hacked by a single @Telegram message.
No link. No tap. No mini app. They pressed /start on a bot.
We ran the message through our abliterated models. It's zero click code execution in Telegram Desktop. 🧵
207
Robert Penner retweeted
Since it seems that formal verification is going viral again, I might as well drop what I have been working on the side-ish for the past 2.5 weeks over weekends. here is Janus: a Lean 4 framework that formally verifies compiled Go machine code. Not the Go source, the actual arm64 and amd64 bytes the CPU runs.
I already ran on a target successfully: holiman/uint256, the 256-bit math library under go-ethereum. All 146 exported functions are proven correct on both arm64 and amd64: 293 machine-checked theorems covering arithmetic, modular math, Exp, Sqrt, parsing and JSON/SSZ/RLP encoding. Each one says: for every valid input, this machine code returns exactly what the spec says.
How it works:
1. Compile the Go code and pull the function's machine code out of the real binary.
2. Write a short, readable spec in Lean, e.g. "z = x + y mod 2^256".
3. Prove the machine code meets it, instruction by instruction, on a Lean model of the CPU.
4. Lean's kernel checks every step of the proof.
Incredibly enough it found real bugs in the library's latest releast. e.g uint256's Float64() truncates instead of rounding to the nearest value, as its documentation promises. It also turned up several places where the docs/expected behaviour and the ACTUAL behaviour disagreed.
Janus can also prove things about performance: uint256's Add executes exactly 17 instructions on both arm64 and amd64, on every call and that has an upper-bound proof/spec.
Every uint256 spec (plain Lean, one file per function): github.com/Giulio2002/fv-uin…
Full list of findings: gist.github.com/Giulio2002/0…
Code: github.com/Giulio2002/Janus
Proofs: github.com/Giulio2002/fv-uin…
Robert Penner retweeted
I had Opus 5.5 formalize CPython in Lean: 613,318 lines of Lean that copy Python's internals line by line, tested against the real interpreter and checked by Lean.
On the way it found real bugs in Python, including crashes from plain Python code. 🧵
The state machine renaissance
There's a renaissance happening for state machines in software development.
A prompt circulating on X this week tells coding agents to find all the implicit state machines lurking in a codebase. It's like a magic spell that brings submerged structures to the surface.
Suddenly, scattered booleans, conditional branches, and ad hoc state transitions are revealed as parts of state machines.
Once you've identified them, you can model them explicitly, constrain their transitions and eliminate entire classes of bugs.
For JavaScript and web development, XState is an excellent tool for wrangling your state into a disciplined and diagrammable structure.
From code monkeys to lawmakers
"Who am I? Why am I here?"
AI agents have largely conquered the tactics of coding. Now they're climbing the ladder of strategic decision-making. Where does that leave us software engineers?
We're actually being promoted: from code monkeys to lawmakers. Your new mission, if you choose to accept it:
Write the constitution of your codebase.
What must always be true? What must never happen? What are the inviolable laws governing this little universe we've created?
Is your code up to code?
Architects can design extraordinary buildings, but every structure must meet building codes. In agentic software development, code can be generated and rebuilt without detailed blueprints.
With AI-assisted formal verification, we can establish the code for the code: laws every implementation must obey, and proof they did.
Then you can let agents tear down walls, rebuild foundations, and construct entirely new architectures. Give them room to innovate.
Just make sure they build to code.
1
191
Robert Penner retweeted
Now you can really see everything
Paradox: the faster things get, the slower they feel.
Crossing the Atlantic used to take weeks; now an eight-hour flight feels like an eternity.
This is the "hedonic treadmill": as we adapt to improvements, our expectations keep rising.
Patience, young hobbits. 🌲
LLMs are far too slow. It feels like the early days of the internet when you'd wait a full minute to download a megabyte of data.
4
382
Robert Penner retweeted
'The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise' - Edsger Dijkstra
Given Uncle Bob's love for automated testing and now AI, I'm waiting for him to fall in love with formal verification and start raving about it.
In 2019, Bob said "types are math" and "tests are science," declaring formal verification of behavior "intractable."
Certainly, writing formal laws and proofs for application behavior was impractical for most developers in 2019. But NASA had already been using formal verification for decades.
Now formal verification is becoming accessible to ordinary developers, as agents help write laws and proofs. And unlike tests, which check specific inputs, mathematical proofs can establish behavioral laws for all valid inputs.
It's the kind of superpowered testing Uncle Bob would love. I'm curious to see if he'll taste the sweet ambrosia of mathematical certainty.
Correct. Types are formal, tests are empirical. Types are math, tests are science.
Formal verification of structure through types is tractable. Formal verification of behavior is not.
Tests are the only tractable means of verifying behavior.
8
862
Laws and Proofs vs. Unit Tests
A unit test is an example: it checks that your code gives the right output for a specific input.
But how do you prove that your code works for every valid input, like any number or any string? The parameter space could be effectively infinite.
One way to tackle this problem is by spraying the space with thousands of test cases, like thousands of torpedoes in a game of Battleship. ❗🛳️❗
This helps, but it increases your test-run time, and coverage is still incomplete.
Formal verification is a more radical approach: define mathematical laws that describe the required behavior. Then you (well, your agent) can construct rigorous mathematical proofs that your implementation obeys those laws for all valid inputs.
With sufficiently comprehensive laws and sound proofs, you can rule out entire classes of bugs by logical necessity.
The compiler verifies these proofs mathematically, without running your code. No need to fire 1000s of torpedoes when you can prove where the ships are. 🚀
5
617
Robert Penner retweeted
XState v6 is now in beta 🚀
Reduced API surface area (transitions are just functions), much stronger types, durable execution, new tools (CLI, viz, editor), and more to come.
Built for humans *and* agents 🤝
npm i xstate@beta
stately.ai/blog/2026-11-05-x…
