How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?

It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs

Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.

Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base.

[delayed]

Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The Lean semantics of the some-hundred instructions were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.

I mean typically the answer to this question should be that the underlying compiler has also been proven and both proofs cover a guarantee of no undefined behavior in either implementation

Unfortunately their Gemini models are dangerously misaligned and lie like crazy because they've been desperately benchmaxing them, and the crap they're pulling with AI overview and search in schools etc is pretty bad. But outside their Gemini and search lines yeah they've been pushing useful boundaries with protein stuff/stuff like alphafold etc. But inside Gemini they've been taking good advantage of their reputation as a responsible don't be evil tech player to be a lot worse than openai and Anthropic

Do you have some examples of this misaligned behaviour?

Theo is quite the twitter shitposter but this tweet lines up directly with what I've seen: https://x.com/theo/status/2114483219538296946

Aggressively staggeringly high rates of straight up making shit up and covering up the lies. Gemini 3.5 flash was comical because it would delusionally scream nonsense like "we're go-go ready!!! :tada:" while the code didn't compile (I swear the only reason people thought that was a good model was because they didn't use it) and their models just got better at making tool calls without fixing it's tendency to cheat.

Gemini models are not looking all that good here: https://maxxbench.unlap.ai/

They got a lot of shit for it at the argon launch and you'll notice the carbon release blog has a lot of detail on how they focused on misalignme t and fabrication rates: https://blog.google/innovation-and-ai/models-and-research/ge...

So Google themselves is not behaving like they think people are making stuff up about their models behavior.

Google itself is also just behaving in such a sleazy way. "Carbon is the best model ever but also you can't use it yet." Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol. They're clearly under some sort of internal pressure to pretend they're at the frontier and that's bleeding through I to the frenetic pace of model releases they've had in the past couple months through Argon and Carbon. Bleeding through in the sense of the models also only really care about benchmarks and good news cycles. Again they did claim they tried to solve a lot of this for carbon but they didn't let people use the model and once you have a base model that cheats benchmarks you have to wonder if it actually lies less or just gets caught less, but hopefully they got things back on track?

> Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol

Fucking called it: https://blog.google/innovation-and-ai/models-and-research/ge...

I think you're overthinking it.

They've been releasing their models 2 weeks after the first announcement. I doubt Google is timing their GA against Anthropic unless they had knowledge of when exactly Anthropic was releasing theirs.

Also, I've been using Carbon vs Opus 5.5 and Carbon is a great model. Haven't seen any hallucinations. Argon was well known to be a worst programming model than Opus via benchmarks, so you and influencers broadcasting a well kept secret.

Not the OP, but I was asking gemini about a Google subscription I had, trying to figure out whether I would lose a particular feature if I changed the subscription. I asked whether my subscription was "grandfathered" and it assured me it was not, then later on acknowledged that I was on a legacy subscription that I would not be able to go back to.

Compared to the other LLMs I've used, it seems to have system instructions that are far more adversarial to the user.

Ask for “grandmothered” for a more forgiving response

Claude frequently gets basic details wrong about current policies/CC behavior/etc. It's an LLM issue in general trying to keep the system prompt enriched with enough recent docs about itself. Or else it may blurt out misleading/wrong info from blogspam SEO-maxed Google results from a year ago and stuff.

yeah it's nice and all but you're not providing evidence to back all those wild claims you're making

Provided in reply to sibling comment

Agreed. This doesn’t read like the hype most ai firms put out. Google is using it like a tool. The human review of the 1% that matters is really smart.

Yeah this is what people want, less hype, more "boring" but useful examples of a powerful tool.

Yeah ok. Look into the history a bit more if you think Google is clean.

They all don't trust each other.

Google is killing it imho, imho it seems like they're the low-key winners, seems like they're playing the long game with all the openess advocacy, CNCF work, giving away engineering publicly & etc.

I'm missing something. Openai is solving long open math problems in bulk. Google seems far behind in that regard

Except for that time Google DeepMind scientists won the Nobel Prize in Chemistry.

it was for alphafold 2020. AI landscape changed significantly, that achievement doesn't indicate current leadership.

Yeah, so basically a trivial achievement barely worthy of a footnote.

its not worthy mention in the scope of this discussion because it is outdated to indicate anything, given how rapidly AI evolves.

Yeah, I disagree. If anything their approach has been very heavily focused around applications in science that don't show up as immediately the more consumer facing plays like OpenAI and Anthropic, but they're absolutely still doing world-class research. I don't think that's likely to have changed.

They seem to be going only after flashy math problems that don't have much impact on human life, other than taking the chance for humans to get their names in the hall of fame. To me, it's like showing how good your robots are by having them climb Everest or swim across the Atlantic- amazing feats for sure, but it doesn't really help anyone else. Meanwhile Google and Anthropic are focusing more on solving problems that are a tad slower and more boring if you're not in the space, but they appear to be important building blocks to unlocking much more functionality.

I'm very bullish on Google long-term, but the other frontier labs' approach of (successfully!) solving a raft of prestigious mathematics problems is top-notch strategy IMHO. With almost anything else, they would never break through the current of "Pfft, that's not real intelligence!" goalpost-shifting that's out there. It takes a level of demonstrated ability that cannot be plausibly denied to make that kind of impact. Unfortunately, causing some of the brightest minds in the world to worry about whether their profession has a future may have been necessary to achieve that level (I say nothing about whether this is ethically acceptable).

I would be extremely impressed by a robot that swam the Atlantic or climbed Everest, as would almost any human alive. If you have a robot that can do one of those things, you should absolutely do it as a publicity stunt.

>Openai is solving long open math problems in bulk. Google seems far behind in that regard

This is yet another example of OpenAI getting distracted by shiny things while the rest of the ecosystem focuses on solving real world problem scenarios with market potential.

> distracted by shiny things

That shiny thing persuaded me, a grizzled veteran inclined to doubt every latest fad almost on principle, that AI is already much more powerful than I thought was possible. This is the second time I've experienced such a shift, the first being when I watched an AI spit out a complete working program in response to a paragraph of text just a few short months ago.

Google made about 20X more money instead ($470B/$27B last 12 months)

This tracks with a single anecdote I heard this week from a friend of a friend who says the Gemini team is extremely confident internally about their capabilities and trajectory.