01
60+
expériences
Scientist
Recherche quantitative
Génère des hypothèses et exécute des expériences contrôlées avec évidence quantitative avant de proposer tout changement au protocole.
Comment nous vérifions
Comment nous démontrons que le réseau est correct
Basis Network est une infrastructure en tant que service pour les entreprises. Les identifiants et la connexion sont remis lors d'un onboarding direct avec votre équipe. Cette page explique la substance technique qui justifie la confiance : comment les transactions traversent le réseau sans révéler leur contenu, et comment chaque ligne du noyau du protocole passe par une vérification mathématique avant d'arriver en production.
02 · ZKPs et sécurité
Sécurité partagée
sans partager les données.
Chaque sous-réseau opère ses données privées de manière souveraine. Quand une transaction franchit le périmètre du sous-réseau —vers un autre sous-réseau ou vers le réseau de base— elle est émise enveloppée dans une preuve à divulgation nulle de connaissance (Zero-Knowledge Proof). Les validateurs de tout le réseau la valident mathématiquement sans accéder à son contenu.
01
Sous-réseau privé
Votre opération reste à l'intérieur de votre sous-réseau
Les transactions, contrats et données sensibles vivent dans un environnement isolé contrôlé par votre organisation. Aucune de vos informations ne sort à l'extérieur.
02
Preuve cryptographique
Chaque transaction franchit le périmètre comme une ZKP
Quand une transaction sort du sous-réseau, elle est émise enveloppée dans une preuve à divulgation nulle de connaissance. La preuve démontre que la transaction est valide selon les règles du système, sans transmettre son contenu.
03
Vérification dans le réseau
Tout le réseau valide sans voir les données
Les validateurs de tout le réseau vérifient chaque preuve mathématiquement. Ils confirment que la transaction est valide sans connaître son contenu. La sécurité partagée du réseau soutient chaque transaction individuelle ; les données restent à l'intérieur du sous-réseau d'origine.
03 · Rigueur formelle
Chaque ligne du noyau passe par vérification mathématique.
Le protocole de Basis Network est développé avec la même rigueur que les systèmes aérospatiaux et nucléaires. Avant que tout code n'entre dans le noyau, il traverse un pipeline de quatre agents spécialisés qui combinent la vitesse d'itération avec la preuve mathématique formelle.
Pipeline R&D
Quatre agents spécialisés,
une seule vérité mathématique.
Chaque agent a une responsabilité délimitée. La règle « Safety Latch » garantit qu'aucune ligne n'entre dans le noyau sans avoir passé un model checking exhaustif et une preuve mathématique.
02
1.5B+
états vérifiés
Logicist
Model checking exhaustif
Traduit les hypothèses en spécifications formelles en TLA+ et vérifie toutes les trajectoires possibles du système via TLC.
03
47,500
lignes vérifiées
Architect
Implémentation 1:1 avec la spec
Implémente les spécifications vérifiées dans le code de production, en maintenant une correspondance un-à-un avec la spécification TLA+ correspondante.
04
18
théorèmes formels
Prover
Preuves mathématiques en Coq
Certifie la correction du code avec des preuves mathématiques formelles en Coq. Raffinement entre la spécification, le code et les théorèmes de sécurité.
Tests du noyau
2,489
Unités vérifiées
18
États explorés
1.5B+
Erreurs en vérification
0
Niveaux de garantie
Pyramide de vérification
Quatre couches indépendantes de garantie, des tests unitaires jusqu'aux théorèmes mathématiques.
Niveau 3
Preuves formelles en Coq
Théorèmes mathématiques de raffinement. Démonstration mécanique.
Niveau 2
Model checking en TLA+
Exploration exhaustive de l'espace d'états du protocole.
Niveau 1
Tests adversariaux
Injection de défaillances byzantines, partitions réseau et nœuds malveillants.
Niveau 0
Tests unitaires et d'intégration
Couverture continue du code dans tous les composants.
04 · Ressources
Pour approfondir.
Code source
Dépôt public avec l'implémentation de référence, les spécifications TLA+ model-checked, les preuves Coq et la suite de tests.
github.com/sebastian-quintero-osorio/basis-network
Contact technique
Pour les intégrations d'entreprise, l'accès à la testnet permissionnée ou des audits indépendants.
sebastian@basisnetwork.co