The Frontier

Remix explains formal verification as mathematically specifying a program's behavior and then mechanically proving the code matches that specification using a proof assistant like Coq. This ensures correctness for all possible inputs, unlike testing or fuzzing.

Remix's OpenSats-funded project formally verified `libsecp`'s 300-line modular scalar multiplication function, requiring 6,000 lines of proof code. This process guarantees memory safety and prevents integer overflows or division by zero.

Formal verification typically demands 20 lines of proof code for every line of C code and involves significant refactoring, such as converting macros to inline functions. Remix spent five weeks on the scalar multiplication proof after months of toolchain learning.

Luis introduces Utreexo, a UTXO set compression method allowing lightweight nodes like phones to run on Bitcoin, overcoming the limitations of Bitcoin Core's large UTXO set. This system relies on bridge nodes creating Merkle proofs for blocks.

Utreexod 0.5 is mainnet compatible, implementing BIPs 181, 182, and 183. It incorporates SwiftSync, which reduces initial block download (IBD) bandwidth for compact state nodes (CSNs) by 75% by only requiring proofs from the last 16 blocks.

Luis explains that Utreexod is a BTCD fork implementing bridge nodes, while Floresta is a from-scratch compact state node (CSN) implementation using the Kernel consensus engine. Floresta, running on Luis's router, consumes about 200MB of RAM and minimal storage.

The Utreexo model enhances wallet privacy by removing the need for third-party APIs like Electrum, which leak user addresses and IP. Compact state nodes instead act as normal Bitcoin nodes on the network.

Z-Man proposed "towards a K of N Lightning Network node" on Delving Bitcoin, aiming for multi-sig self-custodial Lightning wallets. This concept allows K-of-N signing for one channel side, using nested Musig2 and FROST.

Enabling K-of-N Lightning channels requires modifying the Bolt specification to make the "sha-chain" (revocation key handling) optional. This is due to derivation challenges with distributed key material in multi-signature setups.

Merch notes that Z-Man's Lightning proposals often involve complex, interactive designs. This approach circumvents the need for ANYPREVOUT or other covenant proposals, which Z-Man believes are unlikely to be adopted.

Coldcard 6.5.0 adds support for signing Musig2 UTXOs, BIP322 signed messages for Miniscript and Musig2 proof of reserves, Miniscript/Minitapscript, Taproot multisig up to eight leaves, and BIP-129 for secure multisig setup.

Frigate 1.4.0 now uses an "ultra-fast SecP256K1 library" for silent payment scanning, achieving a 14x speed improvement alongside GPU computation. Merch observes this re-implementation of `libsecp` is fast due to LLM-assisted improvements but less vetted.

Bitcoin Core #34401 extends the `libbitcoin_kernel` API to serialize block headers into standard byte encoding. This enables external programs to compute block hashes directly without needing separate serialization code.

Bitcoin Core #35032 prevents the `private broadcast` option (using short-lived Tor/I2P connections for transactions) from storing learned peer addresses in the address manager. This enhances privacy by isolating connection information.

Core Lightning's 26.04 release has removed splicing from experimental status, making it a default and production-ready feature. This marks a significant upgrade in Core Lightning's implementation of the splicing protocol.

Core Lightning #9046 fixes KeySend interoperability with LDK by increasing the final CLTV expiry value (safety margin) from 22 to 42. This matches LDK's expectation for receiving KeySend payments.

LDK has promoted zero-fee commitment channels from experimental to production status. This feature replaces two anchor outputs with one shared `pay-to-anchor` output, offering more flexibility for future fee conditions.

LDK #4558 extends receiver-side timeout, previously for multi-path payments, to KeySend payments. This allows receivers to fail back stuck HTLCs and free up slots without waiting for a full CLTV expiry.

LND #9985 promotes simple Taproot channels to production status. It incorporates `OP_CHECKSIGVERIFY` for Tapscripts and improved map-based nonce handling linked to funding transaction IDs, serving as groundwork for future splicing.

BTCPay Server #7250 adds support for LNURL `withdrawRequest` (LUD-21), an unauthenticated endpoint. This allows external services to verify if a Bolt11 invoice, created via LNURL-pay, has been settled.

BIPs repository #20.9.89 publishes BIP 376, defining new input fields for PSBTv2. These fields carry BIP 350 tweak data necessary to sign and spend silent payment outputs, complementing BIP 375 for output creation.

Gustavo mentions other silent payments BIPs: BIP 252 (defining silent payments), BIP 274 (discrete log equivalency proofs), and BIP 392 (descriptor format). Merch concludes these BIPs provide a complete picture for implementing silent payments, including multi-user transactions.