GPT-OSS-context, formele agentchecks en nieuwe processtukken zetten controleerbaarheid centraal

Een communityanalyse meldt dat een afgeleide GPT-OSS-chattemplate bij meerturngesprekken eerdere antwoorden kan verliezen zodra een assistant-bericht zowel reasoning als content bevat. Los daarvan maakt een nieuw TLA+-overzicht scherp waarom een modelcheck geen bewijs voor de bijbehorende implementatie is — juist relevant nu agents steeds meer stateful code produceren.

Controleer GPT-OSS-templates bij bewaarde reasoning

Een gebruiker meldt een fout in een aangepaste GPT-OSS-Jinja-template die op Unsloths versie zou zijn gebaseerd. Bij het renderen van een historische assistant-turn met zowel thinking als content kiest de getoonde elif-tak alleen de reasoningtekst; het zichtbare antwoord zelf valt dan weg. Dat kan een volgende beurt context geven die wel de redenering, maar niet de eerdere conclusie bevat — een plausibele oorzaak van ontsporende meerturnsessies.

De post bevat ook een aangepaste template met preserve_thinking. Dat kan prefix-caching gunstiger maken, maar vergroot tegelijk de context en tokenkosten. Het is geen upstream security-advisory of bevestigde fix: de bevinding komt van één gebruiker en de beschikbare context bevat geen reactie van Unsloth of OpenAI. Toch is de controle praktisch: test een transcript waarin eerdere turns beide velden hebben, inspecteer de werkelijk gerenderde prompt en vergelijk die met de referentietemplate voordat je een template-fork voor agentwerk uitrolt. Analyse en aangepaste template

TLA+ is nuttig vóór code, maar verifieert die code niet vanzelf

Een nieuw overzicht van Reasonable gebruikt een eenvoudige leader-election om het onderscheid zichtbaar te maken: een TLA+-model beschrijft mogelijke toestanden en overgangen, waarna eigenschappen als ‘nooit twee leiders’ worden gecontroleerd. Voor een eindig model kan TLC alle bereikbare toestanden aflopen en bij een schending een concrete counterexample teruggeven. Maar dat bewijst alleen iets over het model met die eindige parameters — niet automatisch over elke schaal of over de implementatie die een agent daarna schrijft.

De auteur is daar expliciet over: voor algemene eigenschappen is een bewijs nodig, en een los TLA+-model kan van de echte code afdrijven. Als mogelijke brug beschrijft Reasonable een pijplijn die TLA+-specificaties naar Verus vertaalt, met een prover-reviewer-opzet en controles tegen triviale ‘bewijzen’. De gemelde aantallen — meer dan 3.000 machine-gecheckte bewijzen uit 16.459 specificatie/property-paren — zijn eigen resultaten die nog in vervolgposts moeten worden toegelicht.

De bruikbare ontwerpregel voor agentteams is bescheidener: laat een agent eerst invarianten, foutpaden en liveness-aannames expliciteren voor je hem transacties, retries of distributed state laat implementeren. Maar houd vervolgens tests en code-review: TLA+ alleen toont geen refinement tussen model en programmacode. Een HN-gebruiker meldt dat modelleren met Quint transactiefouten blootlegde, maar wijst tegelijk op de extra complexiteit van externe resources en de state-spacekosten. Artikel · HN-discussie

Nieuwe stukken in auteurszaak leggen beschuldigingen over trainingsdata neer

De Authors Guild publiceert een samenvatting van nieuwe, vrijgegeven stukken in de lopende zaak Alter v. OpenAI and Microsoft. Volgens de organisatie stellen de eisers onder meer dat interne berichten kennis tonen van LibGen-gebruik, reputatierisico’s en het later verwijderen van LibGen-bestanden. De Guild koppelt citaten aan een memorandum voor gedeeltelijk summary judgment en een feitenoverzicht van de eisers; een hoorzitting wordt volgens de pagina pas begin 2027 verwacht.

Dit is juridisch relevant voor de herkomst- en licentiediscussie rond modeltraining, maar geen vaststelling van de rechter. Het artikel komt van een belangenorganisatie die partij kiest in het geschil; OpenAI en Microsofts inhoudelijke verweer staat niet in de opgeslagen bron. Ook de HN-discussie laat zien dat gevolgclaims over marktschade worden betwist. Lees de publicatie daarom als een verslag van processtellingen en nieuw openbaar geworden documenten, niet als bewezen opzet of een uitspraak over aansprakelijkheid. Samenvatting van de Authors Guild · HN-discussie

Verder nog

• Toolkitversie is niet hetzelfde als binarydekking: een communityoverzicht zet voor oude NVIDIA- en AMD-kaarten de laatste genoemde CUDA- of ROCm-generatie op een rij en raadt voor onder meer Pascal en Volta CUDA 12.9 aan. Een reactie corrigeert de MI50-grens en wijst op experimentele nieuwere builds. De stevige les blijft: controleer naast toolkitversie ook of precies jouw PyTorch-, vLLM- of llama.cpp-binary voor de GPU-architectuur is gebouwd. Het overzicht en de correcties zijn communitywerk; verifieer ze bij de leveranciersreleasenotes. Overzicht en discussie
• Rust: maak een gevalideerde eigenschap een type: een technische uitwerking van ‘parse, don’t validate’ laat zien hoe NonEmpty, NonZero en verfijnde padtypes herhaalde runtimechecks kunnen vervangen. Bijvoorbeeld: geef een parser na controle een NonEmpty terug in plaats van een Vec, zodat callers niet opnieuw op leegte hoeven te testen. Let bij pad-refinement wel op de trade-off: Utf8PathBuf sluit geldige niet-UTF-8-bestandsnamen uit. Artikel · Lobsters-discussie
• Another World op een ZX Spectrum 48K: antirez toont een realtime Z80-VM en polygonendemo die volgens hem op echte Spectrum-hardware draait. Hij zegt dat er circa 512 bytes overbleven en kondigt een release met Z80-broncode aan; die code is nog niet beschikbaar, dus dit is vooralsnog een demonstratie en geen reproduceerbaar project. Aankondiging