Diego Kingston🟩

To acquaintances: given recent impersonators, I remind you that I will never write to you unless I met you in real life (and generally, I don't write to people often), and will never ask you to download any software or execute commands, or anything of the sort. I have several skills, but Chinese is not among them. I also don't send any files, photos or things of the sort. Beware of scammers. If you bump into someone saying it's me, it´s definitely not me

Our friends at @mathematics_inc forked Hermes Agent to build an incredible autoformalization agent harness

Amazing work!

Updates from @class_lambda lambdaworks: - 1190: pairing optimization for BLS12-381 - 1192: GLV/GLS endomorphism for scalar multiplication - 1195: added hash to curve using RFC9380 for BLS12-381 We are also working towards adding Spartan and IPA to add more IOP and PCS

@fede_intern It’s a great plan. I always liked the part of large deformation theory, it has some weird stuff

Tuesday night, here I am talking with Claude about shells and structural engineering.

@class_lambda Link to lambdaworks: github.com/lambdaclass/la…

Updates from @class_lambda lambdaworks: - PR #1188 (Univariate LogUp-GKR): Implements univariate LogUp-GKR infrastructure with FRI polynomial commitment scheme, univariate sumcheck, and comprehensive examples for ROM check and range check. Includes security hardening - PR #1182 (Metal GPU Poseidon2): Adds Metal GPU-accelerated Poseidon2 Merkle tree backend with compute shaders and fuzzing tests. Includes GPU-accelerated internal Merkle tree levels. - PR #1186 (Circular transition constraint LogUp ): Improves logup

Lambda @class_lambda is helping push @leanEthereum foward!

Lambda @class_lambda brings together engineers from every discipline, chemical, structural, civil, mechanical, industrial, with computer scientists, mathematicians, physicists, and experienced software engineers. We're using that depth, plus LLMs, to ship free alternatives to the tools that have charged $5k to $50k/seat to the engineering profession for decades. Pull request by pull request.

Some updates from @class_lambda lambdaworks: - We added all the abstractions for lookups using logup #1159 and #1186 - We added the RPX hash function #1185 - Poseidon 2 for Goldilocks #1181 - LogUp GKR #1183

Telling people vibe coding VMs is a skill issue when you haven't shipped code to production with real money and security in years is peak Dunning Kruger.

@fede_intern @VitalikButerin @alexhooketh Yes, sometimes it gets the protocol wrong, adds soundness bugs or lacks basic cryptography intuition. It also tends to bloat the codebase

AI is great and we are already using it to accelerate ethrex and lambda risc-v zkvm but I highly recommend to be cautious too. We need to accelerate Ethereum roadmap development for sure but we also need to check all the code being generated. Particularly in cryptography the code being generated has too many bugs and mistakes. @mauro_aligned and @diego_aligned I would love you guys sharing your perspective.

This is quite an impressive experiment. Vibe-coding the entire 2030 roadmap within weeks. Obviously such a thing built in two weeks without even having the EIPs has massive caveats: almost certainly lots of critical bugs, and probably in some cases "stub" versions of a thing where the AI did not even try making the full version. But six months ago, even this was far outside the realm of possibility, and what matters is where the trend is going. AI is massively accelerating coding (yesterday, I tried agentic-coding an equivalent of my blog software, and finished within an hour, and that was using gpt-oss:20b running on my laptop (!!!!), kimi-2.5 would have probably just one-shotted it). But probably, the right way to use it, is to take half the gains from AI in speed, and half the gains in security: generate more test-cases, formally verify everything, make more multi-implementations of things. A collaborator of the @leanethereum effort managed to AI-code a machine-verifiable proof of one of the most complex theorems that STARKs rely on for security. A core tenet of @leanethereum is to formally verify everything, and AI is greatly accelerating our ability to do that. Aside from formal verification, simply being able to generate a much larger body of test cases is also important. Do not assume that you'll be able to put in a single prompt and get a highly-secure version out anytime soon; there WILL be lots of wrestling with bugs and inconsistencies between implementations. But even that wrestling can happen 5x faster and 10x more thoroughly. People should be open to the possibility (not certainty! possibility) that the Ethereum roadmap will finish much faster than people expect, at a much higher standard of security than people expect. On the security side, I personally am excited about the possibility that bug-free code, long considered an idealistic delusion, will finally become first possible and then a basic expectation. If we care about trustlessness, this is a necessary piece of the puzzle. Total security is impossible because ultimately total security means exact correspondence between lines of code and contents of your mind, which is many terabytes (see firefly.social/post/x/2025653… ). But there are many specific cases, where specific security claims can be made and verified, that cut out >99% of the negative consequences that might come from the code being broken.

Link to lambdaworks: github.com/lambdaclass/la…

Updates from lambdaworks: - #1097 | Plonk DSL -- typed variables, CircuitBuilder API, composable gadgets - #1169 | FFT early fusion -- fused stages, merged bit-reverse permutation - #1168 | Metal profiling harness for Apple Silicon GPU kernels - #1160 | GLS endomorphism scalar multiplication for BLS12-381 G2 - #1143 | Plonk prover batch inversions and direct evaluations for enhanced performance - #1171 | Improved CPU FFT based on Plonky3 - #1172 | Consolidate Goldilocks hybrid field into canonical implementation - #1178 | Iterator chains, pre-allocation, and idiomatic patterns across provers - #1177 | Improve examples folder with better rust patterns - #1176 | Improve code quality crypto crate

Lambda @class_lambda has been hiring mathematicians the last years. We're quickly becoming a formal verification powerhouse. Check the AMO-Lean bogpost. AMO-Lean: what if every compiler optimization came with a machine-checked proof? Compiler optimization bugs are not hypothetical. They're well documented. For most software this is fine. For crypto, aerospace, or finance, a silent miscompilation can be catastrophic. AMO-Lean is an optimization pass where every transformation is a theorem formally verified in Lean 4. You write a spec, the system: 1. It explores all equivalent programs simultaneously via equality saturation 2. Picks the fastest variant 3. Emits optimized C or Rust 4. Proves the output is semantically equivalent to the spec Each rewrite rule is a proven theorem, automatically converted into optimizer rules via metaprogramming. There are no manual translation step where correctness silently breaks. The only unverified component is the cost model. If it picks wrong, you get slower but correct code. Normal compilers give you silently wrong code. Way better failure mode. This is particularly relevant for crypto, where optimization bugs are a known class of real vulnerabilities. Provable equivalence between spec and optimized output kills this attack surface. We will be writing a paper about it and we will continue developing it. We already have a proof of concept on matrix computations today, but the architecture generalizes.

A follow-up to our post on building a post-quantum Ethereum client. Here we detail @ethlambda_lean's minimalist architecture.

In life there are two tragedies: one is not getting what one wants, the other is getting it. It seems mankind will find the curse of easily having everything

A few weeks ago I said there was a seismic change in Ethereum's social layer about to happen. It's happening. Multiple big infrastructure players that most users don't know about are starting to collaborate and build together, doubling down on ETH and the Ethereum network. Follow @blockspaceforum to keep up with it. The biggest block builder (@titanbuilderxyz), the biggest relay (@ultrasoundmoney), @ETHGasOfficial, @Commit_Boost (38% network adoption), @QuasarBuilder, @primev_xyz, @nuconstruct, @blocknative, @fabric_ethereum, researchers from the @ethereumfndn, and many others are all coordinating. Many of us realized that they had to team up and work closely together to make our opinions stronger and speed up our ability to deliver. In the last 5 years @class_lambda built many of the most relevant zkVMs and Ethereum L2s. Last year we went all in on @ethereum L1. In a year we built @ethrex_client, one of the fastest production ready execution clients at about 60k lines of code. We're coordinating with big stakers and the MEV pipeline to grow its adoption while also shipping multiple products around it. We're building a new RISC-V zkVM with @alignedlayer and @3miLabs that I think will become a standard for L1 proving and @eth_proofs in the short term. We're working on @leanEthereum by building our own @ethlambda_lean client. We helped develop the @Commit_Boost sidecar that standardizes communication between validators and third party protocols. We're happy to have helped build a critical piece of software that is now running on 38% of the Ethereum network. We also started collaborating with @titanbuilderxyz on different things under @kubimensah's lead. Hopefully soon we'll be working closely with @alextes and @ultrasoundrelay too! There's more I want to share but can't yet. For now I can say that @class_lambda is part of the @blockspaceforum process and I'm very excited about what's coming. Keep an eye on what we will be doing, I promise it's gonna get interesting.

@realjuanruocco @421Net Buenos encantamientos y hechizos. Rancor siempre fue de mis favoritas

cómo no encontraba una aplicación sencilla para llevar la cuenta de mi colección de magic, tuve que armar una con claude. mtg.421.news

Some updates from @class_lambda lambdaworks: *GPU Backends: metal-accelerated MSM, Merkle trees, and sumcheck. CUDA support for FFT with goldilocks field. (1137, 1133, 1134) * Sumcheck improvements (1144, 1145) * Performance: faster EC scalar mul on BLS12-381 (1149) * Code Quality & Correctness: bug fixes, removing dead code, improving Groth16 verification (1151, 1147, 1148, 1150, 1141)