Projekt KERN nabízí ověřovací vrstvu mezi programovacím AI agentem a repozitářem. Místo samotného výsledku testů rozlišuje prokázané tvrzení, nalezený protipříklad, chybějící důkaz a rozpor mezi podklady. Pro kontrolu formálních kontraktů využívá nástroj Z3. Pokud řešič není dostupný nebo výsledek zůstane neznámý, brána se neotevře jen na základě slovního ujištění agenta.
Ukázka pracuje s chybou ve výběru peněz, kterou běžný test bez ověřovací podmínky přehlédne. KERN zároveň dokumentuje omezení: statická kontrola sama neopravuje logiku programu a nenahrazuje důkazy z jeho vykonání. Dostupné rozhraní umožňuje začlenění přes knihovnu nebo HTTP bránu. Kód je veřejně čitelný, nejde ale o open-source licenci podle OSI: komerční použití včetně interního firemního CI vyžaduje samostatnou licenci.
