Pinboard (jm)

Lean proved this program was correct; then I found a bug

jm — 2026-04-14T13:08:07+00:00

This is IMO very exciting. Formal verification and formally-proven correctness in code using Lean, which was in turn exercised heavily using Claude, which managed to turn up a totally unexpected runtime bug:

The positive result here is actually the remarkable one. Across 105 million executions, the application code (that is, excluding the runtime) had zero heap buffer overflows, zero use-after-free, zero stack buffer overflows, zero undefined behaviour (UBSan clean), and zero out-of-bounds array reads in the Lean-generated C code. [...] The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct (and now has a PR addressing). Overall verification resulted in a remarkably robust and rigorous codebase. AFL and Claude had a really hard time finding errors. But they did still find issues. Verification is only as strong as the questions you think to ask and the foundations you choose to trust.

Zip bombs to frustrate AI crawlers

jm — 2025-03-25T10:08:23+00:00

Nifty trick; redirecting abusive AI crawlers to a gzipped file containing 100GB of zeros with a few lines of nginx config:

set $redir_to_gz 1;
if ($host = gz.niko.lgbt) {
    set $redir_to_gz 0;
}
if ($http_user_agent !~* (claudebot|ZoominfoBot|GPTBot|SeznamBot|DotBot|Amazonbot|DataForSeoBot|2ip|paloaltonetworks.com|SummalyBot|incestoma)) {
    set $redir_to_gz 0;
}
if ($redir_to_gz) {
    return 301 https://gz.niko.lgbt/;
}

as for the actual stuff behind gz.niko.lgbt

server {
    # SSL and listen -- snipped

    # static files
    root /var/www/gz.niko.lgbt;
    location / {
        add_header Content-Encoding gzip;
        try_files /42.gz =404;
        gunzip off;
        types { text/html gz; }
    }

    # gunzip off is very important because if the client doesn't support gzip encoding nginx will blow its foot off without that
    # 42.gz is generated with dd if=/dev/zero bs=1M count=102400 | gzip -c - > 42.gz

    # additional config -- snipped
}

Nice one @niko, I'm definitely going to use that :)

research!rsc: Zip Files All The Way Down

jm — 2016-02-05T15:26:51+00:00

quine.zip, quine.gz, and quine.tar.gz. Here's what happens when you mail it through bad AV software: https://twitter.com/FioraAeterna/status/694655296707297281

Compress data more densely with Zopfli - Google Developers Blog

jm — 2013-03-02T23:10:18+00:00

New compressor from Google, gzip/zip-compatible, slower but slightly smaller results

Making Really Executable Jars

jm — 2013-03-01T22:36:52+00:00

Who knew? you can make a runnable JAR file!

There has long been a hack known in some circles, but not widely known, to make jars really executable, in the chmod +x sense. The hack takes advantage of the fact that jar files are zip files, and zip files allow arbitrary cruft to be prepended to the zip file itself (this is how self-extracting zip files work).

lrzip

jm — 2012-02-07T17:31:53+00:00

'Lrzip uses an extended version of rzip which does a first pass long distance redundancy reduction. The lrzip modifications make it scale according to memory size. [...] The unique feature of lrzip is that it tries to make the most of the available ram in your system at all times for maximum benefit. It does this by default, choosing the largest sized window possible without running out of memory.'

pigz

jm — 2009-10-21T10:09:18+00:00

'A parallel implementation of gzip for modern multi-processor, multi-core machines', by Mark Adler, no less