MiniMax M3.1 wordt lokaal inzetbaar; OpenShell 0.1 en formele proofs scherpen agentbeveiliging aan

De weights van MiniMax M3.1 Flash zijn nu openbaar en vLLM meldt ondersteuning vanaf dag één. Dat verandert het model van een loutere API-optie in een kandidaat voor eigen inference, al blijven de indrukwekkende prestatiecijfers leveranciersclaims.

Voor agenten valt daarnaast OpenShell 0.1 op als een concrete nieuwe release van NVIDIAs isolatielaag. Anthropic en Theorem laten tegelijk zien dat LLM-gegenereerde formele proofs op forse schaal kunnen werken, maar nog binnen zeer specifieke uitvoeringsaannames.

MiniMax M3.1 Flash krijgt publieke weights en een vLLM-pad

MiniMax heeft de weights van M3.1 Flash gepubliceerd; vLLM zegt het model meteen te ondersteunen. De runtime noemt native NVFP4 voor KV-cache en MoE-weights, plus DSpark speculative decoding. Daarmee is er nu naast de API een route voor eigen serving en — afhankelijk van beschikbare quantisaties en hardware — lokale experimenten.

Dat is een concrete verandering sinds de ochtendupdate van dinsdag, waarin M3.1 Flash nog expliciet geen open model was. De nieuwe mogelijkheid is vooral relevant voor teams die model, latency, datastroom en servingstack zelf willen beheersen, in plaats van alleen een provider-API te evalueren.

De gepresenteerde cijfers vragen wel om terughoudendheid. vLLM meldt onder meer geheugenbesparing door NVFP4 en throughput op NVIDIA Vera Rubin; MiniMax noemt benchmarks voor agentwerk. Dat zijn metingen van respectievelijk runtimeproject en modelmaker, op specifieke hardware en instellingen. Vergelijk daarom op eigen prompts niet alleen decode-snelheid, maar ook prefill, lange context, gelijktijdigheid, toolfouten en de kwaliteit van de gebruikte weights of quant.

vLLM over M3.1 Flash en de servingpaden · MiniMax over de publieke weights

OpenShell 0.1 voegt policycontrole dichter bij de runtime toe

NVIDIA brengt OpenShell 0.1 uit, een open runtime voor autonome agents met isolatie, policy en een gateway voor credentials. Volgens de projectdocumentatie controleert de runtime bestands-, syscall- en netwerktoegang op kernelniveau. Credentials worden niet rechtstreeks aan de agent gegeven, maar alleen toegevoegd aan requests naar goedgekeurde endpoints. Policywijzigingen worden vooraf formeel gecontroleerd op nieuw bereik, bijvoorbeeld een extra host met credentials, voordat menselijke review nodig is.

Dit is een echte vervolgontwikkeling op de ochtendupdate van dinsdag 29 september: waar OpenShell toen onderdeel was van NVIDIAs bredere agentcontainment-platform, brengt de 0.1-reeks volgens het project een stabiele releasecadans, nieuwe isolatieprimitieven, uitbreidingspunten en API’s. Er zijn SDK’s voor Python, TypeScript, Go en Rust; Kubernetes-deployments gebruiken een gateway en vereisen dat de CNI NetworkPolicy daadwerkelijk handhaaft.

Dit is geen bewijs dat een agentomgeving daarmee veilig is. De HN-discussie benadrukt terecht dat een model met toegang tot gevoelige code of data nog steeds informatie kan proberen uit te voeren via toegestane verbindingen. Policy, sandbox en endpoint-gebonden credentials zijn dus lagen die je moet combineren met minimale rechten, beperkte egress, gescheiden secrets en eigen aanvalstests.

OpenShell 0.1: architectuur, SDK’s en supportmatrix · HN-discussie

Claude genereert formele no-crash-proofs, maar alleen binnen een expliciete scope

Anthropic en Theorem beschrijven een workflow waarin Claude formele proofs schrijft voor bestaande fuzz-tests. Volgens het onderzoek zijn voor 239 entry points in 123 OSS-Fuzz-libraries proofs gemaakt dat de onderzochte binaire code onder de vastgelegde voorwaarden niet crasht voor invoer tot 64 MB. De proofs worden door de Rocq-kernel gecontroleerd; de auteurs publiceren een deel ervan, samen met de gebruikte RISC-V- en Linux-semantiek.

De praktische vernieuwing is niet dat een model simpelweg meer fuzzing uitvoert: een fuzz-test wordt vertaald naar een formele eigenschap over gecompileerde RISC-V-code. Tijdens het bewijzen konden volgens de auteurs ook bugs worden gevonden en gepatcht. Voor securitykritische opensourceprojecten is dat een interessante richting om bestaande testharnassen als startpunt voor sterkere garanties te gebruiken.

De garantie is scherp begrensd. De bewezen binaries zijn single-threaded en statisch, met vaste geheugenlimiet, een RISC-V-CPU en gemodelleerd Linux-gedrag; bovendien bewijst een no-crash-eigenschap niet alle gewenste functionele correctheid. Ook in de HN-discussie wordt terecht gewezen op de nog open vraag of de zeer uitvoerige proofstijl naar complexere software schaalt. Zie dit daarom als een veelbelovende aanvulling op fuzzing en review, niet als een algemene verklaring dat libraries bugvrij zijn.

Anthropic en Theorem: methode, scope en gepubliceerde artifacts · HN-discussie over schaalbaarheid en toepassingsgrenzen

Verder nog

• UUIDv7 vraagt om bescheiden aannames: een technische analyse laat zien dat RFC-conforme generators geen strikte creatietijd of wereldwijde monotone volgorde garanderen. Bij een klok die terugloopt kan Pythons uuid.uuid7() zijn ingebedde tijd vooruit laten lopen; tussen processen of machines is strikte ordening al helemaal geen eigenschap van het formaat. Gebruik UUIDv7 gerust voor unieke, grof sorteerbare sleutels, maar bewaar een echte tijdstempel en gebruik een expliciet orderingsprotocol wanneer die garanties nodig zijn. Analyse met RFC- en Python-voorbeeld · Lobsters-discussie
• Nix als afhankelijkheidslaag voor losse scripts: een praktische uitwerking laat zien hoe writePython3Bin een Python-script met vastgepinde Python- én systeemafhankelijkheden verpakt, inclusief een wrapper voor PATH; dezelfde writers-route bestaat voor meer talen. Dat is nuttig voor scripts die anders op een willekeurige combinatie van pip en systeemtools rusten. De uitgewerkte aplay-demo ondersteunt alleen Linux, dus neem platformondersteuning expliciet op in de flake. Voorbeeld en Nix-constructies · Lobsters-discussie