PRIVACY is a God Given Right

This video examines the amount of location information carried by inaudible background sounds, using the Doppler effect to locate a reference recording within ~100m, and only needing (in some cases) less 1-min of audio. This video raises awareness of these capabilities and closes by discussing preventative measures one could take.

Methodology:
Aircraft position, altitude, and velocity data were sourced from ADS-B data and filtered in Python using ICAO type-code classification for propeller vs jet types. For each candidate location on a 200m grid, the closest point of approach (CPA) and sound propagation delay were computed from 3D slant distance, using a digital elevation model (DEM).

Doppler curve spectrogram measurements constrained each event's velocity and CPA slant distance. Candidates were then filtered by the 920-second offset between two flyovers, plus a silence constraint. The exact Doppler curve each candidate would hear was modelled, using emission-time radial velocity from interpolated ADS-B data.

Modelled doppler curves were scored against the observed spectrogram using a locked two-event scoring method. This corrected for measurement error on CPA time & fundamental frequency, while preserving the purely physics-derived temporal offset between the two events.

The pipeline was repeated again for a single 1-min clip of known time, US-wide search, and again, successfully scored the true location 1st.

Lastly, preventative measures were assessed, including rationale behind why common signal processing fixes fail (high-pass filtering, drowning out, and phone call compression/noise reduction).

This video is an educational demonstration of acoustics, signal processing, and data analysis using publicly available data. No code or tools are being released.

Hi Laura / Hi Cybe.

Agreed. Many people (who should know better?) are still on Windows! The appropriate analogy would be that remaining on Windows is like handing over the key to your house to a thief. A thief may break in no matter what one does, but putting the key in their hand ( using a Windows OS) is downright negligence.

On November 10, 2026, Google DeepMind announced that it had used frontier LLM agents to mathematically verify important security properties of Signal's actual cryptographic implementation.

The project is called AlphaProof Code. It represents a significant advance in AI-assisted formal verification, not merely conventional security auditing.

RESULTS REPORTED NOVEMBER 10, 2026

6.5M

Lines of machine-checked proof

4 weeks

Research effort

Lean

Formal proof checker

What they actually proved

The researchers verified properties of Signal's libsignal implementation, including:

  • Forward secrecy: Compromising keys later should not reveal previously protected messages.
  • Post-compromise security: The protocol can regain certain security guarantees after a temporary compromise.
  • Authentication: Protections against impersonation under the specified threat model.
  • Handshake secrecy: Protection of key-establishment secrets, including a modeled post-quantum property.

The crucial distinction is that the AI produced formal proofs checked by the Lean theorem prover. The researchers did not simply ask an LLM whether Signal was secure and accept its opinion.

But they did not prove that the entire Signal application is secure. Their proofs cover specified properties of compiled cryptographic code under explicit assumptions, not every application feature, operating system interaction, or possible attack.

google-deepmind.github.io+1

Which frontier models?

The technical paper identifies two:

  • Gemini 4 Carbon: Generated the formal proofs using teams of autonomous agents.
  • Claude Opus 5.5 and Gemini 4 Carbon: Helped develop and cross-review the mathematical specifications, with human researchers approving them.

The work also uncovered problems in earlier published formal analyses of the protocol.

google-deepmind.github.io

The important limitations

The research used libsignal v0.105.4 and SPQR v1.6.0, compiled for AArch64 Linux. It did not verify the complete Signal apps, and notably did not establish post-quantum recovery after compromise, a protection the protocol is designed to provide. The proofs also depend on trusted specifications, cryptographic assumptions, and models of the execution environment.

google-deepmind.github.io

Original research

Assessment — high confidence in the reported achievement, pending independent reproduction. The more consequential development isn't that AI declared Signal secure. It's that frontier LLM agents generated millions of lines of mathematical proof, checked by a separate formal verification system, in approximately one month. This could substantially change how production software is verified.

1 Like

That series of people with firstnamesirname and another one with something like NameSomething82934 were a set of simple spambots with some AI that someone is letting lose everywhere.

They find an appropriate thread, analyse it a bit and write a convincing looking reply. Then after a few they then drop the payload, a message with a link.

There were quite a few....They've been locked out for now...

I still remember fondly the first time I tried Linux, over 30 years ago...

2 Likes

I can relate to that fondness. :slightly_smiling_face:

Massive Microsoft 365 outage disrupts Outlook, Teams, Copilot worldwide

Microsoft is investigating a widespread outage affecting multiple Microsoft 365 services, including Outlook, Microsoft Teams, and Copilot, as users report connectivity problems worldwide.