Security Council Nomination: Everett Hildenbrandt (Runtime Verification)

Season 6 Security Council Nomination Template - Cohort A

Please paste your completed nomination here, following the instructions at the top.

Security Council Member Self-Nomination Template

Please keep your answers as concise as possible while conveying all relevant information.
All nominations will require 8 Top 100 delegate approvals.

Please indicate if you are running to be the Council Lead or a Council Member:

Council Member

Does this nomination represent an individual or organization:

Organization

Candidate country of residence (or, if an entity, incorporation and principle place of business):

USA

Have you previously served on Optimism’s Security Council:

No

Have you previously served on any other Council or Board in the Collective:

No

Are you a representative of OP Labs:

No

Are you a representative of another OP Chain:

No

If you are a delegate, please provide the link to your delegate profile:

No

If you are a member of the Citizens’ House, please link to your most recent attestation here:

No

Please outline your contributions, and their impact, to the Optimism ecosystem to date:

We have worked with the OP Labs team on integrating Kontrol —our formal verification tool for Solidity and EVM smart contracts—into their CI. Within the course of our most recent engagement, we verified the pausability mechanism (Improving Superchain Incident Response Capabilities) of Optimism L1 contracts. Being a part of Optimism’s CI, Kontrol continuously proves that the pausability mechanism works correctly as code evolves.

Kontrol proofs and a detailed description of the project can be found in the Optimism monorepo: optimism/packages/contracts-bedrock/test/kontrol at develop · ethereum-optimism/optimism · GitHub,

and our blogpost: Kontrol Integrated Verification of the Optimism Pausability Mechanism.

Please demonstrate any non-Optimism experience you believe is relevant to this role:

Runtime Verification specializes in formal verification of software systems, providing the highest level of assurance for the correctness and security of smart contracts and other critical software. Our mission is to deliver open-source formal verification and developer tooling to reduce the costs of auditing and enable continuous formal verification and testing on each commit.

Since 2018, we have provided formal verification and security services to numerous blockchain foundations and dApps, such as EigenLayer, Uniswap, Ethereum Foundation, Lido, Gnosis, Morpho, Polkadot, and many others.

Here you can find a complete list of our previous engagements.

Please elaborate on your technical background, including your github handle (this will be used to calculate your github expertise score and will be added to your nomination before it goes to a vote by the Foundation):

Our technical expertise is rooted in the development and maintenance of industry-leading tools such as the K Framework, Kontrol, Simbolik, and KEVM. These tools are central to our formal verification processes, which have been applied to a wide range of blockchain ecosystems.

Our GitHub Organization hosts all of Runtime Verification’s open-source tools and projects, designed to improve the security and reliability of blockchain and software systems through formal verification.

We are currently building and maintaining the following projects:

  1. K Framework: A rewrite-based executable semantic framework that allows formal definition of programming languages and VMs.
  2. Kontrol: Combines KEVM and Foundry to enable developers to perform formal verification without learning new languages or tools.
  3. Simbolik: VSCode-compatible Solidity debugger with built-in symbolic execution engine designed to assist in debugging and verifying smart contracts.
  4. KEVM: An executable formal specification of the Ethereum Virtual Machine (EVM) in the K framework.
  5. KWasm: A formal semantics of WebAssembly in the K framework, allowing formal analysis and verification of WebAssembly programs.
  6. KMIR: A formal semantics of the Rust MIR (Mid-level Intermediate Representation) in the K framework.
  7. Kasmer: A formal verification tool for WebAssembly, based on KWasm.
  8. KaaS: CI Integrated Cloud-Based Symbolic Execution.

You can learn more about our tools from Runtime Verification docs.

Please elaborate on your experience with relevant member (or Lead) requirements:

RV brings a unique combination of formal verification expertise, deep technical security knowledge, and a strong track record of contributing to high-profile blockchain ecosystems. Our team is well-versed in secure key management, governance processes, and the operational aspects of blockchain security. We have successfully integrated formal verification and security tools into CI pipelines of several projects, demonstrating our ability to manage complex security requirements and deliver robust, secure solutions. Our alignment with the Optimistism vision and our technical competency make us a strong candidate for the Security Council.

Please describe your philosophy on what makes a good Security Council member:

A good Security Council member should embody technical expertise, a commitment to transparency, and a strong ethical foundation. At Runtime Verification, we believe that members must possess deep knowledge in cybersecurity, especially web3 security, enabling them to make decisions that safeguard the network’s integrity. Our previous contributions to the Optimism ecosystem, particularly our work with OP Labs, have given us a deep understanding of the ecosystem’s ethos, which we fully share and support. Collaboration, accountability, and a focus on security are essential to our philosophy, ensuring that decisions reflect the community’s best interests while advancing the goals of decentralization within the Optimism ecosystem.

Please disclose any anticipated conflicts of interest:

Runtime Verification does not anticipate any conflicts of interest in serving on the Optimism Security Council. If any potential conflicts arise, we are committed to full transparency and will take measures to address them on the Optimism forum or under this post.

Please verify that you understand you may be removed from this role via the Representative Removal proposal type in the Operating Manual:

Yes, understood.

Please verify that you understand that election is subject to successful completion of a Foundation screen which may include KYC/AML, sanctions screening, and a requirement to sign a standard contract:

Yes

Please verify that you are able to commit ~5 active hours / month to fulfill the Member Responsibilities. Please note that there is an “on-call” aspect to this role that is not fully encompassed in the active hours estimate:

Yes

We are impressed with the experience and contributions to the Optimism technical foundation and other ecosystems.

We are an Optimism delegate with sufficient voting power and believe this candidate is ready to move to an election.

1 Like

Who would be the point person from RV for this role? Regardless, I think this organization has sufficient technical background to allow the collective to vote. I would, however, like to see this organization have a larger presence within the optimism community, lending their technical expertise to relevant discussions.

On behalf of Blockchain@USC:
We are an Optimism delegate with sufficient voting power and we believe this proposal is ready to move to a vote.

1 Like

Main point person would be myself, Everett Hildenbrandt, CEO.

Next point person would be Gregory Makodzeba, Developer Relations.

Let us know how we can get more involved. I’m happy to do technical review of grants/proposals, offer general advice, and will start attending relevant calls (eg. DAG).

1 Like

I am an Optimism Delegate with sufficient voting power and I believe this proposal with experience on integrating Kontrol is ready to move to a vote.

1 Like

gm, Gregory is here, I’ll be the next point of contact after Everett. Let me know if you have any questions.

I am an Optimism delegate with sufficient voting power and I believe this proposal is ready to move to a vote.

I am an Optimism delegate with sufficient voting power and I believe this proposal is ready to move to a vote.

1 Like

The SEED Latam delegation, as we’ve communicated here, with @Joxes being an Optimism delegate with sufficient voting power we believe this proposal is ready to move towards a vote.