Vad Mistral öppnade
Den 2 juli 2026 släppte det franska AI-labbet Mistral Leanstral 1.5 under en Apache-2.0-licens, med öppna vikter på Hugging Face och en gratis API-slutpunkt. Enligt Mistrals eget tillkännagivande är det en mixture-of-experts-modell, 119B parametrar totalt med omkring 6B aktiva och en kontext på 256k tokens, specialiserad på formell teorembevisning i Lean 4 och autoformalisering. Enkelt uttryckt innebär bevisning i Lean 4 att ett påstående om din programvara omvandlas till en sats som en maskin kontrollerar rad för rad, så att korrekthet visas i stället för att antas.
Benchmarkresultaten närmar sig mättnad: 100 procent på miniF2F validerings- och testuppsättningar, 587 av 672 PutnamBench-problem lösta, 87 procent på FATE-H och 34 procent på FATE-X, med stark skalning under beräkning, från 44 problem vid en liten budget upp till 587 vid en stor. Mer talande för en ägare avslöjade modellen i test 5 tidigare okända buggar i 57 kodförråd, bland dem ett kritiskt överflöde i ett zigzag-avkodningsbibliotek som konventionella test vanligtvis missar.
Att skriva kod var den lätta halvan
Att få en AI att skriva kod är i stort sett löst. Att bevisa att koden är korrekt är det inte, och det är den halva som räknas för allt du inte har råd att få fel. När modeller genererar mer av din programvara överstiger mängden kod den mänskliga granskningsförmågan, och verifieringslagret blir tyst flaskhalsen och den egentliga tryggheten.
Därför väger en bevismotor som Leanstral tyngre än ännu en kodgenerator. För kritisk och reglerad programvara flyttar bevisbar korrekthet från akademisk lyx mot ett realistiskt upphandlingskrav, där ett påvisat bevis väger det ingen godkänd testsvit kan matcha. Ägaren som kan styrka att en komponent är bevisad, och inte bara testad, förhandlar från ett starkare läge mot tillsynsmyndigheter, försäkringsbolag och kunder.
Att äga kontrolleraren
Suveränitetspoängen här är inte ännu en chattbot. Det är verifieraren. Eftersom Leanstral levereras som europeiska öppna vikter under Apache-2.0 kan du köra kontrollagret internt, se exakt vad det gör och behålla det, i stället för att anropa ett amerikanskt API och lita på en svart låda du varken ser eller bevarar.
Så förblir förtroendelagret i din programvarukedja granskningsbart och under din kontroll. När maskiner skriver koden är den avgörande frågan vem som äger maskinen som kontrollerar maskinen. En bevismotor du själv kör besvarar den frågan till din fördel, utan att tvinga dig att lämna över din känsligaste kod till en extern tjänst.
Läs vidare: Din Microsoft-förnyelse är en hävstång · Suveränt moln kommer nu med ett betyg
