Also I noticed something in the libsignal repo:
>attest: Functionality for remote attestation of SGX enclaves and server-side HSMs
https://github.com/signalapp/libsignal
How trusted are Intel's (SGX) and AMD's hardware level security features?
Cloudflare runs their edge network in random ISP datacenters and in shady jurisdictions and promise AMD's TSME is enough to keep things secure.
Use s real password with the signal account thing.
> The resolution (decompression) of such backreferences in an imperative context is trivial, but uses lots of invariants that make it hard to prove correct. In a purely functional context, it is non-trivial to find data structures that are fast enough. We decided to stick with purely functional algorithms, as they can be verified directly using Coq, and optimization of purely functional programs is interesting for its own sake. In our current verified implementation, this is the slowest part. The benchmarks in Appendix 0.A support this claim. We already have figured out an algorithm with better performance, but we are not yet done proving it formally correct; we will not get deeper into this algorithm in this paper.
There are many ways verify programs; the authors of your linked paper just chose a method that resulted in a slow binary. Alternatively, one can build a model of an imperative language (C) and prove that an imperative programs meets some specification.
Not sure if this is precise. At least it sounds somewhat odd. I think what they really wanted to say here is "multi-agent system" (which usually, but not necessarily, implies the use of multiple LLMs).