Paulo Matos

Paulo Matos

@ocmatos.com

Compilers at @Igalia.com, binary translation & formal methods. Teaching AI agents to prove their code correct. Dad, Piano, Fortnite. 🇵🇹 in 🇩🇪

228 followers541 following115 posts

Since starting piano lessons I've logged every lesson and practice session. Instrumentive on Android served me well, but I wanted more, so I built my own: rightkey.app It's been my daily driver for a year. If you track your practice, try it and tell me what you think! #piano #musicpractice

Claude really cooked with the latest projects version. Here I am in a café literally talking to Claude to fix some issues while I enjoy a coffee and a bretzel with butter. I don't stop being amazed.

Symphonika is my take on orchestrating coding agents: it picks up GitHub issues, runs agents in separate workspaces and follows each one through a workflow that lives in the repo. Scheduled Routines cover work that has no ticket. #AgenticCoding #SoftwareEngineering p.ocmatos.com/blog/symphon...

p.ocmatos.comSymphonika: building a software factory - Notes & CodeFrom watching agents in Pewpew to giving them work: issue workflows, scheduled routines, and the decisions a software factory must leave to humans.

Six months after JSSE's first release: 47 of 48 JetStream workloads now run (up from 22), 2.9x faster on the ones March could run, and still 100% on test262. This post is about the guardrails that kept it honest. #JavaScript #Rust #AgenticCoding #Claude p.ocmatos.com/blog/faster-...

p.ocmatos.comFaster, With Guardrails - Notes & CodeSix months after JSSE's first release: 47 of 48 JetStream workloads run, up from 22, and 2.92x faster on the ones March could run. test262 is still at 100%. Agents can make an engine faster, as long a...

After Thales, comes Pabst. Great work from Jesse, bringing Formal Verification to the Agentic Coding era.

Jesse Alama@jessealama.net

I'm happy to announce pabst: a tool for Property-Based Testing in JavaScript/TypeScript. Annotate your functions with properties they're supposed to have, run `pabst test` to try to invalidate those claims, and watch the bugs come crawling out. Install via `npm install pabst-checker`,

Paulo Matos reposted

I'm happy to announce pabst: a tool for Property-Based Testing in JavaScript/TypeScript. Annotate your functions with properties they're supposed to have, run `pabst test` to try to invalidate those claims, and watch the bugs come crawling out. Install via `npm install pabst-checker`,

A new category of programming language is forming, aimed at agents rather than humans. Vow is mine: small, self-hosted, with contracts verified by ESBMC. "The language is not for you. Yours is only the product." p.ocmatos.com/blog/whats-i... #agenticcoding #formalverification

p.ocmatos.comWhat's in a vow? A language for the future of agentic coding - Notes & CodeAnnouncing Vow, an agent-first programming language with formal verification built in. Self-hosted, early, and open for you to try.

In March I wrote about JSSE: a JavaScript engine an agent built from scratch. It was fast to build, slow to run. So I asked the agent to optimize it. No bytecode, no JIT, just constant factors. #javascript #engine #jsse #agentic #coding p.ocmatos.com/blog/how-fas...

p.ocmatos.comHow fast do you want it? - Notes & CodeSeven weeks of agentic optimization on JSSE. 4.73x faster on test262 wall time, 1.92x JetStream geometric mean, half the cost of building the engine in the first place.

Exciting work by Jesse bridging TypeScript with Formal Verification via Lean. 👀

Jesse Alama@jessealama.net

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. Thales is a bridge for TS programmers into Lean's program verification toolset. Check out github.com/jessealama/t... to get started.

🧵 My best ideas seem to come to me while I am running. Time and time again I have great ideas while running, then I get back home and pufff... gone! As if I had been in a dream-state all along.

View full thread

A system that allows me dump these ideas _while_ I am running. They are summarized, categorized and when I have time `/grill-me` is used on them to create implementation plans.

The first step of recording while running seems to be the most painful one. Any suggestions? And if you're a builder and create something, I will be your first customer. That's it... and if you get anything anything out of reading this is that you should be running more! :)

🧵 My best ideas seem to come to me while I am running. Time and time again I have great ideas while running, then I get back home and pufff... gone! As if I had been in a dream-state all along.

Lately I get home and I run to my phone and try to dump as much I as can using Google Recorder. It's working fine but... it's not perfect. Here's what I need...

Heading this week to AI Engineer in London. If you happen to be there and want to grab a coffee and talk AI, let me know! @aiDotEngineer #AI #London

Paulo Matos reposted

Tomorrow at Embedded World! Hall 4, Booth 4-443. Demoing Moonforge — live OTA updates on RPi5 via RAUC — plus a Zephyr BLE app built entirely on upstream code, and WPE WebKit on embedded hardware. Talks: Tue 14:45 Yocto best practices, Thu 15:00 web engines for embedded. #EmbeddedWorld #ew26

Paulo Matos reposted

We're live at #EmbeddedWorld! Hall 4, Booth 4-443 — demos running all day.

Paulo Matos reposted

LLMs write code fast, but how do you trust it? Unit tests only cover paths you think to test. Bounded model checking exhaustively explores all paths and gives mathematical proofs when it finds bugs. 🧵

I built a Claude Code plugin for ESBMC (esbmc.github.io) — bringing formal verification into your agentic coding workflow. Ask Claude to check your code, ESBMC runs under the hood, and you get concrete counterexample traces when it finds bugs.

Paulo Matos reposted

Absolutely awesome to see CCC side by side with the other oldies but goodies compilers. I am pretty confident GCC and Clang were the last breed of popular C compilers written by humans!

Matt Godbolt@matt.godbolt.org

We just added CCC to @compiler-explorer.com - Claude's C Compiler. And what fitting way but to have gotten Claude to added itself to CE... @anthropic.com - added a build to our builder, added it to our daily builds, added the installation, the configuration, and tested it in staging. Nice!

Paulo Matos reposted

The EC is putting together an initiative to develop their strategy for open digital ecosystems. Given its potential to push forward the development and funding of open-source software in Europe and beyond, Igalia submitted a response with some suggestions. Read more: www.igalia.com/2026/02/03/I...

igalia.comIgalia's Response to the European Commission on the Open Digital Ecosystem Strategy | IgaliaIgalia is an open source consultancy specialised in the development of innovative projects and solutions. Our engineers have expertise in a wide range of technological areas, including browsers and cl...

If you are in Nuremberg or surroundings, consider joining our meetup group to discuss the implications of AI in the marketplace. No matter your profession - lets get together, chat and have some fun! #nuremberg #meetup #vibe Join us at www.meetup.com/vipers-vibe-...

meetup.comVipers Meetup Nuremberg — Vibe Engineering & Agentic AI | MeetupWhere professionals explore vibe coding, agentic AI, and the new wave of AI-augmented work. Bimonthly in Nuremberg.The way we build software is changing fast. Entire applications are being vibe-coded ...

Paulo Matos reposted

Paulo Matos reposted

Paulo Matos reposted

Really wishing that somebody would hire my company (@igalia.com) to standardize/implement support for import maps in web workers. I already have a draft spec PR ready and there is interest from the community, which company wants to be the hero funding pushing it forward? :)

github.comSupport import maps in workers by nicolo-ribaudo · Pull Request #10858 · whatwg/htmlThis patch started as a conversation with @guybedford. I tried writing some spec for one of the potential approaches discussed in WICG/import-maps#2. This PR is not actually ready as I have not fin...

Paulo Matos reposted

Claude Code helps me so much with the household chores. The dishes get washed more frequently, the apartment is appreciably tidier, the vacuum cleaner spends an above-average amount of time turned on, the trash gets taken out more quickly.

Paulo Matos reposted

Incredible results with #lean and Gemini Deep Think by Tao in the Erdős Problem. It feels like a lot of doors in the formalization space, whether that's math or hardware/software verification, are opening quickly. mathstodon.xyz/@tao/1155914...

mathstodon.xyzTerence Tao (@tao@mathstodon.xyz)Over at the Erdos problem website, AI assistance is now becoming routine. Here is what happened recently regarding Erdos problem #367 https://www.erdosproblems.com/367 : 1. On Nov 20, Wouter van…

Paulo Matos reposted

Valve’s announcements last week about their new hardware were particularly welcome here at Igalia: a lot of our work will be in those machines. From translation layers to better frame rates and longer battery life, we’ve helped @valvesoftware.com push gaming forward. www.igalia.com/2025/11/help...

igalia.comHelping Valve to Power Up Steam Devices | IgaliaIgalia is an open source consultancy specialised in the development of innovative projects and solutions. Our engineers have expertise in a wide range of technological areas, including browsers and cl...