-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
Have you seen https://github.com/FStarLang/fstar-vscode-assistant? Copilot & F* works pretty nicely.
We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el
Have you seen https://github.com/FStarLang/fstar-vscode-assistant? Copilot & F* works pretty nicely.
We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el
F* existed before Project Everest, but Everest did power a lot of its development.
We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/
Some of it is deployed in production systems:
* Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...
* Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star
Related posts
-
How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
-
One step forward, an easier interoperability between Rust and Haskell | IOG Engineering
-
Awesome Rust Cryptography list compiled by the Rust Cryptography Interest Group (RCIG)
-
A Memory Safe TLS Module for the Apache HTTP Server
-
Translation of the Rust's core and alloc crates to Coq for formal verification