Repository navigation

Releases

v1.0.0 — Formally Verified Post-Quantum WAN Mesh Latest

Latest

KELLERBABG released this 09 Nov 10:08

v1.0.0

0f3936d

Vantablack 1.0.0 — Formally Verified Production Release

I am proud to announce the 1.0.0 milestone of Vantablack. This release marks the transition of Vantablack from an experimental architecture into a production-grade, zero-panic, post-quantum WAN mesh routing node and high-assurance TUN VPN.

Formally Verified Security & Mathematical Guarantees (Keller & ProVerif)

Rather than relying solely on traditional unit testing, I subjected the entire Vantablack core to formal verification and SMT solver analysis:

Keller SMT Verification Platform: Evaluated over 2,500 functions and 1,290+ proof obligations across the workspace using the Z3 SMT solver.
0 Remaining Counterexamples: Formally resolved all 104 SMT counterexample FAIL obligations (integer overflow/underflow, slice boundary violations, division hazards, and remainder anomalies) across 23 core modules.
Symbolic Secrecy Proofs (ProVerif 2.05): Formally proved injective agreement, payload secrecy, and forward secrecy against active Dolev-Yao network adversaries (formal/ghost_session.pv & formal/shardsec_space_time.pv).
Absence of Panic Paths: Completely eliminated unmodelled .unwrap() / .expect() panics across untrusted packet ingest, PDU framing, and reassembly rings. Malformed or malicious network payloads are rejected deterministically without crashing the node.

Cryptography, Onion Routing & Hardening

PEN-2 Sphinx Shard Onion Security: Resolved fixed-nonce keystream reuse in SphinxShardOnion. Every hop (Guard, Middle, Exit) now utilizes cryptographically fresh 96-bit ephemeral nonces directly within the 576-byte fixed-size onion frame.
GTFv2 High-Entropy Wire Framing: Eliminated slack-padding null runs; PRF stream masking guarantees Shannon entropy $> 7.92\text{ bits/byte}$ across all packet sizes, preventing Deep Packet Inspection (DPI) fingerprinting.
Post-Quantum Hybrid Core: NIST FIPS 203 ML-KEM-768 + X25519 key encapsulation, ML-DSA-65 identity signatures, and constant-time SessionGuard sliding-window replay protection (>31 Mpps).
Reed-Solomon RS(2,1) Fast-Path: Monotone ring-buffer reassembly with zero-copy erasure reconstruction at $> 20\text{ GiB/s}$.

Keller-Verify Debut

With this milestone, I am also debuting Keller-Verify, an open-source formal verification engine for Rust.

Alongside v1.0, I am introducing Keller-Verify: a formal verification tool designed to mathematically prove that Rust code is free from panics, out-of-bounds access, and arithmetic overflows using SMT-LIB solving directly on the compiler's MIR.

If you are intrigued about Keller-Verify, check it out at either of these two links:
https://veritas.kellersystems.dev
https://github.com/KELLERBABG/Keller-Verify.com

Assets 12

v0.8.21

github-actions released this 03 Nov 11:25

v0.8.21

9183ac0

Full Changelog: v0.8.20...v0.8.21

Assets 10

v0.8.20

github-actions released this 18 Oct 21:21

v0.8.20

65b8087

Full Changelog: v0.8.19...v0.8.20

Assets 10

v0.8.19

github-actions released this 18 Oct 20:53

v0.8.19

b811dbe

Full Changelog: v0.8.18...v0.8.19

Assets 10

v0.8.18

github-actions released this 18 Oct 20:21

v0.8.18

03bb587

Full Changelog: v0.8.17...v0.8.18

Assets 10

v0.8.17

github-actions released this 18 Oct 18:53

v0.8.17

361756e

Full Changelog: v0.8.16...v0.8.17

Assets 10

v0.8.16

github-actions released this 18 Oct 17:06

v0.8.16

cc753d3

Full Changelog: v0.8.15...v0.8.16

Assets 10

v0.8.15

github-actions released this 18 Oct 16:41

v0.8.15

4588756

Full Changelog: v0.8.14...v0.8.15

Assets 10

v0.8.14

github-actions released this 18 Oct 16:23

v0.8.14

7ad1882

Full Changelog: v0.8.13...v0.8.14

Assets 10

v0.8.13

github-actions released this 18 Oct 16:04

v0.8.13

1066c30

Full Changelog: v0.8.12...v0.8.13

Assets 11

v1.0.0 — Formally Verified Post-Quantum WAN Mesh

Vantablack 1.0.0 — Formally Verified Production Release

Formally Verified Security & Mathematical Guarantees (Keller & ProVerif)

Cryptography, Onion Routing & Hardening

Keller-Verify Debut

Uh oh!

v0.8.21

Uh oh!

v0.8.20

Uh oh!

v0.8.19

Uh oh!

v0.8.18

Uh oh!

v0.8.17

Uh oh!

v0.8.16

Uh oh!

v0.8.15

Uh oh!

v0.8.14

Uh oh!

v0.8.13

Uh oh!