Η &Truth συγκεντρώνει 70 εκατ. δολάρια σε αρχική χρηματοδότηση για την κατασκευή καθολικής μηχανής επαλήθευσης κώδικα

Η &Truth, εταιρεία κοινωφελούς σκοπού που αναπτύσσει τεχνολογία για να αποδεικνύει μαθηματικά ότι το λογισμικό είναι ασφαλές, βγήκε από τη μυστικότητα στις 29 Οκτωβρίου 2026, γνωστοποιώντας ότι συγκέντρωσε 70 εκατομμύρια δολάρια σε αρχική χρηματοδότηση και ότι σχεδιάζει να κατασκευάσει αυτό που αποκαλεί καθολική μηχανή επαλήθευσης κώδικα.

Στην ανακοίνωση της ίδρυσής της, η εταιρεία ανέφερε ότι ιδρύθηκε στις αρχές του 2026 και χρηματοδοτήθηκε με 70 εκατομμύρια δολάρια αρχικού κεφαλαίου από μια ομάδα που περιέγραψε ως πρωτοπόρους στον τομέα της ασφάλειας της τεχνητής νοημοσύνης και των επιχειρηματικών κεφαλαίων. Η εταιρεία δήλωσε ότι κατασκευάζει τη μηχανή επαλήθευσης ώστε να διαβάζει κώδικα σε οποιαδήποτε γλώσσα προγραμματισμού και να αποδεικνύει μαθηματικά ότι είναι ασφαλής, προστατευμένος και ορθός, με αποδείξεις που μπορεί να ελέγξει ανεξάρτητα οποιοσδήποτε.

Αυτοματοποίηση αποδείξεων με βάση το Lean

Η τυπική επαλήθευση υπάρχει εδώ και δεκαετίες, αλλά μέχρι πρότινος ήταν απρόσιτη και δαπανηρή, ανέφερε η ανακοίνωση, καθώς οι ειδικοί έπρεπε να διατυπώνουν τις αποδείξεις με το χέρι, περιορίζοντας την εφαρμογή της σε λίγα κρίσιμα συστήματα. Η εταιρεία δήλωσε ότι η τεχνητή νοημοσύνη επιταχύνει πλέον την εργασία για την τυπική απόδειξη κατά 100 φορές ή περισσότερο και ότι η τεχνολογία αυτοματοποίησης αποδείξεων που διαθέτει επιταχύνει τη διαδικασία κατά επιπλέον 100 φορές, μειώνοντας τον χρόνο παραγωγής αποδείξεων από χρόνια ή μήνες σε ώρες ή λεπτά.

Η εταιρεία περιέγραψε επίσης την τεχνολογία που αποκαλεί «εργοστάσιο προδιαγραφών», η οποία, όπως ανέφερε, επιτρέπει σε επιχειρήσεις και προγραμματιστές να μετατρέπουν σε μεγάλη κλίμακα την ανθρώπινη πρόθεση και τις επιχειρηματικές απαιτήσεις σε ακριβείς τυπικές προδιαγραφές, παρέχοντας εγγυήσεις που μπορούν να ελεγχθούν ανεξάρτητα, αντί να βασίζονται σε δοκιμές ή στους ισχυρισμούς των προμηθευτών.

Η &Truth βασίζεται στο Lean, ένα σύστημα αποδείξεων ανοικτού κώδικα, και στο Mathlib, μια βιβλιοθήκη με περισσότερες από δύο εκατομμύρια γραμμές μαθηματικών ορισμών και θεωρημάτων, καθώς και σε τεχνολογίες ανοικτού κώδικα, όπως το CSLib. Σύμφωνα με την εταιρεία, στόχος είναι να δημιουργηθεί ένα καθολικό τυπικό λεξιλόγιο για το λογισμικό: μαθηματικά μοντέλα γλωσσών προγραμματισμού και συστημάτων, τεχνικές απόδειξης και ακριβείς προδιαγραφές που επιτρέπουν την αυτοματοποιημένη επαλήθευση σε όλες τις γλώσσες. Η &Truth δήλωσε ότι συνεργάζεται με τον Lean Focused Research Organization και σκοπεύει να διαθέσει τις θεμελιώδεις βιβλιοθήκες της ως λογισμικό ανοικτού κώδικα.

Ο συνιδρυτής και συνδιευθύνων σύμβουλος Clark Barrett δήλωσε ότι τα Lean και Mathlib προσέφεραν στην τεχνητή νοημοσύνη μια ακριβή γλώσσα για μαθηματικούς συλλογισμούς, ενώ το λογισμικό δεν διέθετε αντίστοιχο θεμέλιο. Ο συνιδρυτής και επικεφαλής επιστημονικός υπεύθυνος Ilya Sergey δήλωσε ότι η εμπιστοσύνη στο λογισμικό θα πρέπει να βασίζεται σε αποδείξεις που μπορούν να ελεγχθούν ανεξάρτητα και όχι στον λόγο οποιασδήποτε εταιρείας.

Ιδρυτές και δύο έδρες

Ο Barrett είναι καθηγητής Επιστήμης Υπολογιστών Corbel στο Stanford University, ιδρυτικός συνεκτελεστικός διευθυντής του Stanford Center for AI Safety, διευθυντής του Stanford Center for Automated Reasoning, συνδημιουργός του CSLib και επικεφαλής του έργου για τη μηχανή αυτοματοποιημένου συλλογισμού cvc5. Ο Sergey ίδρυσε το VERSE Lab στο National University of Singapore και συνδημιούργησε τα εργαλεία επαλήθευσης ανοικτού κώδικα Veil και Velvet. Ο συνιδρυτής, συνδιευθύνων σύμβουλος και εκτελεστικός πρόεδρος Chris Hsu είναι μέλος του Lean FRO Strategic Advisory Board και πρόεδρος του Infinitude Foundation, ενώ στο παρελθόν διετέλεσε διευθύνων σύμβουλος της Kilometre Capital και διευθύνων σύμβουλος της Citadel Investment Group.

Η ανακοίνωση ανέφερε επίσης τον Gregory Malecha, ο οποίος είχε προηγουμένως ηγηθεί του τομέα τυπικών μεθόδων στην BlueRock Security και υπήρξε βασικός αρχιτέκτονας του πλαισίου επαλήθευσης BRiCk· τον Sebastian Ullrich, συν-αρχιτέκτονα του Lean 4 και συνιδρυτή του Lean Focused Research Organization· τον Linus Lee, πρώην διευθύνοντα εταίρο της Kilometre Capital· και τον Drew Harman, πρώην επικεφαλής εμπορικό διευθυντή της Fastino Labs και λειτουργικό εταίρο στις Insight Partners και Shasta Ventures. Η &Truth δήλωσε ότι αξιοποιεί δεκαετίες έρευνας στην τυπική επαλήθευση και τον αυτοματοποιημένο συλλογισμό στο Stanford University και στο National University of Singapore.

Η έδρα της &Truth στις ΗΠΑ βρίσκεται στο Πάλο Άλτο και η διεθνής έδρα της στη Σιγκαπούρη, όπου, σύμφωνα με την εταιρεία, το γραφείο της θα επεκταθεί σημαντικά στους τομείς της έρευνας, της μηχανικής, των προϊόντων και της εμπορικής ανάπτυξης. Ο Low Jin Yong, ανώτερος αντιπρόεδρος και συνεπικεφαλής του Digital Industry Singapore, δήλωσε στην ανακοίνωση ότι η έδρα θα ενισχύσει τις δυνατότητες της Σιγκαπούρης στον τομέα της εμπιστοσύνης και της ασφάλειας και θα ενδυναμώσει τη θέση της χώρας ως βάσης για εταιρείες που αναπτύσσουν αξιόπιστη τεχνητή νοημοσύνη.

Στον ιστότοπο της εταιρείας παρουσιάζεται επίσης μια συζήτηση στρογγυλής τραπέζης με τον Leonardo de Moura, εφευρέτη του Lean και αντιπρόεδρο και διακεκριμένο επιστήμονα στην AWS, και τον Simone Severini, μέλος του Lean FRO Strategic Advisory Board και διακεκριμένο μηχανικό στην Google.

Συνοδευτικά δοκίμια εξηγούν το σκεπτικό της εταιρείας

Σε συνοδευτικό δοκίμιο με ημερομηνία 29 Οκτωβρίου 2026, ο Hsu ανέλυσε τις τάσεις που, σύμφωνα με την εταιρεία, καθιστούν επείγουσα την επαλήθευση, παραθέτοντας δηλώσεις του διευθύνοντος συμβούλου της Google, Sundar Pichai, ότι το 75% του νέου κώδικα στην Google παράγεται πλέον από τεχνητή νοημοσύνη και εγκρίνεται από μηχανικούς, καθώς και τις δοκιμές της Veracode για το 2026, σύμφωνα με τις οποίες τα μοντέλα τεχνητής νοημοσύνης απέτυχαν σχεδόν στις μισές εργασίες προγραμματισμού όπου είχε σημασία η ασφάλεια. Το δοκίμιο αναφέρεται επίσης σε εκστρατεία του Σεπτεμβρίου 2026, κατά την οποία ένας εισβολέας χρησιμοποίησε εκατοντάδες πράκτορες τεχνητής νοημοσύνης για να παραβιάσει 395 οργανισμούς σε 48 χώρες, εκμεταλλευόμενος αδυναμίες σε ευρέως χρησιμοποιούμενο λογισμικό διαχείρισης εκτυπώσεων, καθώς και στον αριθμό-ρεκόρ των 14.959 ευπαθειών λογισμικού που δημοσιεύτηκαν τον Σεπτέμβριο του 2026, μέγεθος που, όπως αναφέρει, είναι 3,5 φορές μεγαλύτερο από τον αριθμό που είχε δημοσιευτεί έναν χρόνο νωρίτερα.

Το δοκίμιο αναφέρεται σε παλαιότερα ορόσημα της τυπικής επαλήθευσης: η αρχική απόδειξη για τον μικροπυρήνα seL4 απαιτούσε περίπου 20 ανθρωποέτη εξειδικευμένης εργασίας για περίπου 8.700 γραμμές κώδικα· το 2015, στο πλαίσιο του προγράμματος HACMS της DARPA, το seL4 ενσωματώθηκε στο ελικόπτερο Unmanned Little Bird της Boeing, τα συστήματα ελέγχου πτήσης του οποίου δεν μπόρεσε να παραβιάσει μια επαγγελματική ομάδα red team, παρότι είχε πρόσβαση επί εβδομάδες· και τον Σεπτέμβριο του 2026, ένα μοντέλο τεχνητής νοημοσύνης που ανέπτυξε η Anthropic τυποποίησε στο Lean, μέσα σε 11 ημέρες, την πλήρη απόδειξη του Τελευταίου Θεωρήματος του Φερμά. Σημειώνει επίσης ότι νωρίτερα το 2026, ο Kim Morrison, ανώτερος μηχανικός ερευνητικού λογισμικού στο Lean FRO, χρησιμοποίησε το Claude της Anthropic με ελάχιστη ανθρώπινη καθοδήγηση για να δημιουργήσει μια έκδοση της βιβλιοθήκης συμπίεσης zlib σε Lean και να αποδείξει ότι αυτή επαναφέρει πάντοτε ακριβώς τα δεδομένα που συμπίεσε.

Το δοκίμιο παραθέτει τα λόγια του δημιουργού του Lean, Leonardo de Moura: «Οι δοκιμές προσφέρουν εμπιστοσύνη. Η απόδειξη παρέχει εγγύηση».

Σε ένα δεύτερο δοκίμιο που δημοσιεύτηκε στις 29 Οκτωβρίου 2026, ο Sergey εξηγεί πώς λειτουργεί η επαλήθευση προγραμμάτων, ξεκινώντας από την εργασία του Alan Turing του 1949 με τίτλο «Έλεγχος μιας μεγάλης ρουτίνας», η οποία πρότεινε οι προγραμματιστές να συνοδεύουν τον κώδικά τους με ακριβείς ισχυρισμούς που ένας ελεγκτής θα μπορούσε να επαληθεύει μεμονωμένα. Το δοκίμιο περιγράφει τις προδιαγραφές, τις αναλλοίωτες συνθήκες των βρόχων και τις αποδείξεις που ελέγχονται στο Lean, και αναφέρει ότι στόχος της &Truth είναι οι προγραμματιστές να μπορούν να αποκτούν ανεξάρτητα επαληθεύσιμα τεκμήρια, όπως μια τυπική απόδειξη στο Lean, με κόστος που καθιστά την επαλήθευση τακτικό μέρος της ανάπτυξης.

Η &Truth περιγράφει το μακροπρόθεσμο όραμά της ως μετάβαση από τον «προγραμματισμό με το ένστικτο» στον «επαληθεύσιμο προγραμματισμό», όπου ο κώδικας που δημιουργείται από τεχνητή νοημοσύνη επαληθεύεται μαθηματικά πριν από την ανάπτυξή του, οι πράκτορες τεχνητής νοημοσύνης λειτουργούν σε περιβάλλοντα με αποδεδειγμένα περιορισμένα όρια, το παλαιό λογισμικό εκσυγχρονίζεται με ασφάλεια και οι κρίσιμες υποδομές προστατεύονται από μαθηματικές εγγυήσεις που μπορούν να ελεγχθούν ανεξάρτητα.