We're building a new computing stack with formally verified data, memory, and resource isolation between executions for instant, truly elastic global compute. This includes designing and building a production language in a way that's never been done before, with complete, mechanized formal specifications and a certifying compiler from the start. Our immediate goals include an alternative to eBPF and building the world's first serverless networking infrastructure.

We are VC funded with runway for multiple years. The team is composed of PhDs from Stanford, UW, OSU, and Brown, advised by professors from MIT and UWaterloo.

We are currently hiring for the following positions:

- [1] Staff Software Engineer: Compilers, Programming Languages, and Verification ($175k - $250k + ≥ 0.4%)

- [2] Formal Verification Engineer: Formal Methods and Programming Languages ($120k - $200k + ≥ 0.2%)

- [3] Software Engineer: Compilers and Programming Languages ($100k - $175k + ≥ 0.1%)

- [4] Formal Methods PhD Intern: Formal Methods and Programming Languages ($10k / month)

Please see [5] for general information. Apply via our job board [6].

[0] https://formalstack.com

[1] https://formalstack.com/jobs/05-2026/staff-software-engineer...

[2] https://formalstack.com/jobs/05-2026/formal-verification-eng...

[3] https://formalstack.com/jobs/05-2026/software-engineer-v.pdf

[4] https://formalstack.com/jobs/05-2026/formal-methods-phd-inte...

[5] https://formalstack.com/jobs/info.pdf

[6] https://jobs.gem.com/formal

We’re [0] rethinking serverless from scratch, building a new computing stack for instant, globally available, truly elastic, soundly isolated execution. We leverage formal methods and languages to build OS interfaces with low overhead, formally verified isolation without containers or VMs. Our immediate goal is a new programming language to replace eBPF and build the world's first serverless networking infrastructure.

We are a 5-person, VC-funded team with PhDs from Stanford, UW, OSU, and Brown, advised by professors from MIT and UWaterloo. We are currently hiring for the following four positions:

- [1] Staff Software Engineer: Compilers, Programming Languages, and Verification ($175k - $250k + ≥ 0.4%)

- [2] Formal Verification Engineer: Formal Methods and Programming Languages ($120k - $200k + ≥ 0.2%)

- [3] Software Engineer: Compilers and Programming Languages ($100k - $175k + ≥ 0.1%)

- [4] Formal Methods PhD Intern: Formal Methods and Programming Languages ($10k / month)

Please see [5] for general information. Apply via our job board [6].

[0]: https://formalstack.com [1]: https://formalstack.com/jobs/12-2025/staff-software-engineer... [2]: https://formalstack.com/jobs/12-2025/formal-verification-eng... [3]: https://formalstack.com/jobs/12-2025/software-engineer-v.pdf [4]: https://formalstack.com/jobs/12-2025/formal-methods-phd-inte... [5]: https://formalstack.com/jobs/info.pdf [6]: https://jobs.gem.com/formal

At Formal [0], we’re rethinking serverless from scratch: we’re building a new computing stack for instant, globally available, truly elastic, soundly isolated execution. We leverage formal methods and languages to build OS interfaces with low overhead, formally verified isolation without containers or VMs. Our immediate goal is to write a new programming language to replace eBPF and build the world's first serverless networking infrastructure.

We are a 5-person, VC-funded team with PhDs from Stanford, UW, OSU, and Brown, advised by professors from MIT and UWaterloo. We are currently hiring for the following four positions:

- [1] Staff Software Engineer: Compilers, Programming Languages, and Verification (≥ $200k + ≥ 0.5%)

- [2] Formal Verification Engineer: Formal Methods and Programming Languages ($120k - $200k + ≥ 0.25%)

- [3] Software Engineer: Compilers and Programming Languages ($100k - $175k + ≥ 0.2%)

- [4] Formal Methods PhD Intern: Formal Methods and Programming Languages (≥ $5k / month)

Please see [5] for general information. To apply, email us at (work at formalstack dot com) and let us know how your experiences fit the role and its requirements.

[0]: https://formalstack.com [1]: https://formalstack.com/jobs/09-2025/staff-software-engineer... [2]: https://formalstack.com/jobs/09-2025/formal-verification-eng... [3]: https://formalstack.com/jobs/09-2025/software-engineer-v.pdf [4]: https://formalstack.com/jobs/09-2025/formal-methods-phd-inte... [5]: https://formalstack.com/jobs/09-2025/info.pdf

We're building a new computing stack for instant, globally available, truly elastic, soundly isolated execution. We’re building low overhead, formally verified isolation primitives, without containers or VMs. We're taking all of this to the network with new a programming language to replace eBPF and enable truly serverless networking infrastructure.

We are a 5-person, VC-funded team with PhDs from Stanford, UW, OSU, and Brown, advised by professors from MIT and UWaterloo. We are looking for a formal verification engineer [1] with deep and practical experience with Rocq.

Please email us at (work at formalstack dot com) and let us know how you fit the role [1].

[0]: https://formalstack.com [1]: https://formalstack.com/jobs/05-2025/verification.pdf

2. Yes!

We're rethinking the computing stack from the ground up for truly elastic, soundly isolated, instantly and globally available execution. We’re building OS interfaces and compilers for low overhead, formally verified isolation without containers or VMs. We're starting with the network: a programming language to replace eBPF and enable globally programmable networking as a service.

We are a 4-person, VC-funded team with PhDs from Stanford, UW, and OSU, advised by professors from MIT and UWaterloo. We are hiring founding-level software engineers [1] in compilers, programming languages, & verification.

Please email us at (work at formalstack dot com) and let us know how you fit the role [1]. While we are only able to move forward with strictly qualifying applicants at this time, we welcome conversations with anyone interested.

[0]: https://formalstack.com [1]: https://formalstack.com/jobs/01-2025/compilers.pdf

We're rethinking the computing stack from the ground up for truly elastic, soundly isolated, instantly and globally available execution. We’re building OS interfaces and compilers for low overhead, formally verified isolation without containers or VMs. We're starting with the network: a programming language to replace eBPF and enable globally programmable networking as a service.

We are VC-funded ($700k pre-seed), advised by professors from MIT and UWaterloo, and founded by ex-Stanford PhDs. There are two official roles, but we welcome conversations with anyone interested in joining the team.

- Compilers & Programming Languages - https://formalstack.com/jobs/09-2024/compilers.pdf

- Kernel Networking - https://formalstack.com/jobs/09-2024/networking.pdf

Please email us at (work at formalstack dot com) or (sergio at the same domain).

[0]: https://formalstack.com

Comments URL: https://news.ycombinator.com/item?id=38306540

Points: 162

# Comments: 56

Comments URL: https://news.ycombinator.com/item?id=18636113

Points: 395

# Comments: 83

  on_request => |request, _| {
      if request.uri().path().ends_with('/') {
          let new_path = request.uri().path()[..-1];
          request.set_uri(URI::new(new_path));
      }
  }

  on_response => |request, response| {
      if response.status() == Status::NotFound && request.uri().path().ends_with('/') {
          response.set_status(Status::Found);
          response.set_header(Location(request.uri().path()[..-1]));
          response.take_body();
      }
  }

[0]: https://rocket.rs/guide/fairings/

[1]: https://api.rocket.rs/rocket/fairing/trait.Fairing.html

[0]: https://api.rocket.rs/rocket_contrib/index.html

[1]: https://rocket.rs/guide/introduction/#foreword

Comments URL: https://news.ycombinator.com/item?id=14772185

Points: 165

# Comments: 74

Managed state is a feature specifically designed to help with this kind of thing. That being said, I still think Rocket can do more to abstract away database connections. I'm tracking improvements on this front in GitHub issue #167 [2].

[0]: https://github.com/SergioBenitez/Rocket/tree/master/examples...

[1]: https://github.com/SergioBenitez/Rocket/blob/master/examples...

[2]: https://github.com/SergioBenitez/Rocket/issues/167

Comments URL: https://news.ycombinator.com/item?id=13581420

Points: 152

# Comments: 60

  error: 'id' is declared as an argument...
   --> src/main.rs:8:9
    |
  8 | #[get("/")]
    |         ^^^^

  error: ...but isn't in the function signature.
    --> src/main.rs:9:1
     |
  9  |   fn hello() -> &'static str {
     |  _^ starting here...
  10 | |     "Hello, world!"
  11 | | }
     | |_^ ...ending here

Comments URL: https://news.ycombinator.com/item?id=13245475

Points: 484

# Comments: 114