vLLM 0.32 scherpt serving en security aan; Lean laat bewijzen door meerdere kernels narekenen

vLLM 0.32.0 is een grote serving-upgrade met securityfixes, snellere opstartpaden en een paar wijzigingen die bestaande deployments kunnen breken. Lean 4.35.0 maakt het intussen mogelijk een development door meerdere, losstaande kernels te laten hercontroleren — een extra controlelaag, geen magische garantie.

vLLM 0.32.0 verandert defaults voor serving én hardening

vLLM 0.32.0 is uit. Voor inference-operators springen drie soorten wijzigingen eruit: de release repareert drie security-advisories, beperkt CORS voortaan standaard tot geen origins en laat onbetrouwbare beelden alleen nog toe in een rasterformaat-allowlist. Ook krijgen gedeelde-memoryhandles voor multimodale caches volgens de releasenotes een HMAC-handtekening en weigert de server JSON-schema’s die dieper dan 64 niveaus nesten.

Daarmee is dit meer dan een modelondersteuningsrelease. Wie een browserclient voor een OpenAI-compatibele vLLM-server heeft, moet na de upgrade expliciet --allowed-origins configureren; het vroegere impliciete * verdwijnt. Controleer tegelijk of eigen clients afhankelijk zijn van hernoemde reasoning-stream-events of van het oude gedrag waarin max_tokens alvast ruimte in het contextvenster reserveerde.

Er zijn ook praktische performance- en runtimewijzigingen. vllm download-kernels kan vooraf gecompileerde FlashInfer-kernels installeren en vllm preload --preload-autotune bewaart een autotune-tabel over herstarts. Bij meer dan één API-worker verdeelt de server verbindingen volgens de release naar de minst belaste worker; vLLM meldt daarvoor 43–85% meer requests per seconde bij korte requests. Dat zijn projectmetingen, geen voorspelling voor lange prompts, eigen modellen of een volledige agentworkflow.

De upgrade vraagt bovendien om een dependencycheck: Python 3.10 valt af, met Python 3.11 als nieuwe ondergrens; ook transformers en tokenizers krijgen hogere minimaversies. Dit is een concrete vervolgontwikkeling na de namiddagupdate van vrijdag 16 oktober, die vLLM nog behandelde als runtimepad voor Reflection-Beam. Test deze release daarom in staging op browsertoegang, clients, images, eigen parsers en de gebruikte Python-versie — niet alleen op tok/s. vLLM 0.32.0: volledige release notes

Lean 4.35.0 voegt paranoia-modus voor proof checking toe

Lean 4.35.0 levert lake check: een commando dat een development exporteert en opnieuw laat controleren door leanchecker, de afgeslankte officiële kernel, binnen een sandbox. Met lake check --paranoid komen daar vier aanvullende kernels bij: nanoda, lean4lean, con-leche en con-ron. De release gebruikt in die modus ook een officiële kernelvariant met geharde geheugenallocator, die geheugencorruptie volgens de makers in een gecontroleerde abort moet veranderen in plaats van een stil verkeerd resultaat.

De interessantste extra checker is con-leche: geschreven in Lean en voorzien van een consistentiebewijs. De makers omschrijven dat zorgvuldig: iedere door con-leche geaccepteerde omgeving heeft, onder een aanname over de consistentie van de gebruikte verzamelingenleer, een model in die theorie. Dat sluit programmeerfouten in juist deze kernelimplementatie als foutklasse uit, maar bewijst niet dat de compiler, runtime of de funderende aanname foutloos zijn.

Daarom is er ook con-ron: een naar Rust vertaalde checker waarvoor Aeneas volgens de aankondiging een verfijning naar het algoritme van con-leche bewijst. Twee uiteenlopende toolchains die hetzelfde bewijs accepteren, verlagen plausibel het risico op één gedeelde implementatiefout; ze maken formele verificatie niet absoluut. De maker noemt bovendien schaalbaarheid nog open werk: externe kernels moeten volgens hem beter met binaire exports en incrementele checking omgaan bij zeer grote ontwikkelingen.

Voor Lean-projecten is dit vooral een nieuwe, concrete supply-chain- en regressiecontrole: voer lake check --paranoid eens uit op eigen proofs en onderzoek afwijkende uitkomsten. De HN-discussie benadrukt terecht dat Lean vooral formaliseert en controleert; het verzint niet vanzelf de wiskundige ideeën die gecontroleerd moeten worden. Lean over kernels, aannames en lake check · HN-discussie

Sphinx maakt begrip van agentdiff een push-gate

Sphinx is een FOSS Git-hook voor agentondersteunde ontwikkeling. Bij een push op een beschermde branch leest de tool volgens de projectpagina de diff en stelt hij een vraag over het gewijzigde gedrag, inclusief een foutpad. Pas na een goed antwoord gaat de push door; overslaan kan met sphinx yolo en wordt gelogd. Het kan een bestaand coding-agentendpoint, OpenRouter of een OpenAI-compatibele API gebruiken.

Dit is een interessante, smalle reactie op een praktisch agentprobleem: testgroen of een plausibele diff betekent niet noodzakelijk dat degene die deployt de retries, state-overgangen of foutafhandeling begrijpt. De tool zegt .env-bestanden en sleutels niet te openen en antwoorden niet naar de coding agent te sturen. Dat zijn projectclaims; ze vervangen geen inspectie van hook, configuratie, modelendpoint en repositoryrechten.

De beperking zit ook in de interactie zelf. In de HN-discussie noemen deelnemers confirmation fatigue en het risico dat teams een verplichte quiz als hinderlijk ervaren of uiteindelijk laten automatiseren. Behandel Sphinx daarom als een experimentele reviewprikkel voor kleine, risicovolle branches — en meet of vragen daadwerkelijk relevante fouten vangen zonder de pushstroom tot ritueel te maken. Sphinx: werkwijze en installatie · HN-discussie

Verder nog

• Furigana in een font blijft contextgevoelig: een HN-discussie over Furifont, een project dat Japanse furigana via een font wil tonen, maakt een harde grens zichtbaar: dezelfde kanji kan afhankelijk van woord en context anders worden gelezen. Dat maakt het hooguit een hulpmiddel voor voorbereide tekst of leerinterfaces, niet een universele omzetter voor willekeurige Japanse inhoud. De opgeslagen projectpagina bood geen leesbare technische uitleg; deze nuance komt uit de discussie, niet uit een onafhankelijke evaluatie. HN-discussie